# Isabelle/HOL Support Wiki

### Site Tools

reference:rule_method

# Differences

This shows you the differences between two versions of the page.

 reference:rule_method [2011/06/22 11:59]131.246.161.187 reference:rule_method [2011/06/22 12:27] (current)131.246.161.187 [Example] Both sides previous revision Previous revision 2011/06/22 12:27 [Example] 2011/06/22 12:19 2011/06/22 11:59 2011/06/13 22:01 created Next revision Previous revision 2011/06/22 12:27 [Example] 2011/06/22 12:19 2011/06/22 11:59 2011/06/13 22:01 created Line 16: Line 16: ==== Example ==== ==== Example ==== + Assume we have a goal + + $\quad[|\ A |] \Longrightarrow A \vee B$ + + Applying ''​apply (rule disjI1)''​ yields the new subgoal + + $\quad [|\ A\ |] \Longrightarrow A$ + + which can obviously be solved by one application of ''​[[assumption]]''​. Note that ''​apply (rule(1) disjI)''​ is a shortcut for this and immediately solves the goal. + ==== Non-Example ==== ==== Non-Example ==== Line 24: Line 34: apply (rule_tac ident1="​expr1"​ and ident2="​expr1"​ and ... in rule) apply (rule_tac ident1="​expr1"​ and ident2="​expr1"​ and ... in rule) This means that the variable ''?​ident1''​ is replaced by expression ''​expr1''​ and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''​thm rule''​. This means that the variable ''?​ident1''​ is replaced by expression ''​expr1''​ and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''​thm rule''​. + + === rule(k) === + Oftentimes, a rule application results in several subgoals that can directly be solved by ''​[[assumption]]'';​ see [[#​Example|above]] for an example. Instead of applying ''​assumption''​ by hand, you can apply ''​rule(k)''​ which forces Isabelle to apply ''​assumption''​ $k$ times after the rule application. ==== Relatives ==== ==== Relatives ====