doc-src/TutorialI/Rules/Basic.thy

 apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply intro
 	--{* @{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
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 

 *}
 
 
 text{*Quantifiers*}
 
+
+text {*
+@{thm[display] allI}
+\rulename{allI}
+
+@{thm[display] allE}
+\rulename{allE}
+
+@{thm[display] spec}
+\rulename{spec}
+*};
+
 lemma "\<forall>x. P x \<longrightarrow> P x"
 apply (rule allI)
 by (rule impI)
 
 lemma "(\<forall>x. P \<longrightarrow> Q x) \<Longrightarrow> P \<longrightarrow> (\<forall>x. Q x)"
 apply (rule impI, rule allI)
 apply (drule spec)
 by (drule mp)
 
-text{*NEW: rename_tac*}
+text{*rename_tac*}
 lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)"
 apply intro
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rename_tac v w)
 	--{* @{subgoals[display,indent=0,margin=65]} *}

 \rulename{someI}
 
 @{thm[display] someI2[no_vars]}
 \rulename{someI2}
 
+@{thm[display] someI_ex[no_vars]}
+\rulename{someI_ex}
+
 needed for examples
 
 @{thm[display] inv_def[no_vars]}
 \rulename{inv_def}
 

 @{thm[display] order_antisym[no_vars]}
 \rulename{order_antisym}
 *}
 
 
-lemma "inv Suc (Suc x) = x"
+lemma "inv Suc (Suc n) = n"
 by (simp add: inv_def)
 
 text{*but we know nothing about inv Suc 0*}
 
 theorem Least_equality:

 *};
 by (auto intro: order_antisym)
 
 
 theorem axiom_of_choice:
-     "(\<forall>x. \<exists> y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
+     "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
 apply (rule exI, rule allI)
 
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 

 (*both can be done by blast, which however hasn't been introduced yet*)
 lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k";
 apply (simp add: Least_def)
 by (blast intro: some_equality order_antisym);
 
-theorem axiom_of_choice: "(\<forall>x. \<exists> y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
+theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
 apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])
 by (blast intro: someI);
 
 text{*end of Epsilon section*}
 

 apply (rule exI)
 apply (rule conjI)
  apply assumption
 oops
 
-lemma "\<forall> z. R z z \<Longrightarrow> \<exists>x. \<forall> y. R x y"
-apply (rule exI)
-apply (rule allI)
-apply (drule spec)
+lemma "\<forall> y. R y y \<Longrightarrow> \<exists>x. \<forall> y. R x y"
+apply (rule exI) 
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule allI) 
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (drule spec) 
+  --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
 lemma "\<forall>x. \<exists> y. x=y"
 apply (rule allI)
 apply (rule exI)