doc-src/TutorialI/Rules/Basic.thy

-(* ID:         $Id$ *)
 theory Basic imports Main begin
 
 lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)"
 apply (rule conjI)
  apply assumption

 *};
 
 
 lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R"
 apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (intro impI)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 by (erule notE)
 
 text {*
 @{thm[display] disjCI}
 \rulename{disjCI}
 *};
 
 lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R"
 apply (intro disjCI conjI)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 
 apply (elim conjE disjE)
  apply assumption
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 
 by (erule contrapos_np, rule conjI)
 text{*
 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{6}}\isanewline
 \isanewline

 by (drule mp)
 
 text{*rename_tac*}
 lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)"
 apply (intro allI)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rename_tac v w)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
 
 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))"
 apply (frule spec)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (drule mp, assumption)
 apply (drule spec)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 by (drule mp)
 
 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))"
 by blast
 

 text{*
 instantiating quantifiers explicitly by rule_tac and erule_tac*}
 
 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))"
 apply (frule spec)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (drule mp, assumption)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (drule_tac x = "h a" in spec)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 by (drule mp)
 
 text {*
 @{thm[display]"dvd_def"}
 \rulename{dvd_def}
 *};
 
 lemma mult_dvd_mono: "\<lbrakk>i dvd m; j dvd n\<rbrakk> \<Longrightarrow> i*j dvd (m*n :: nat)"
 apply (simp add: dvd_def)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (erule exE) 
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (erule exE) 
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rename_tac l)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rule_tac x="k*l" in exI) 
-	--{* @{subgoals[display,indent=0,margin=65]} *}
+        --{* @{subgoals[display,indent=0,margin=65]} *}
 apply simp
 done
 
 text{*
 Hilbert-epsilon theorems*}