src/FOLP/ex/Nat.thy

--- a/src/FOLP/ex/Nat.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Nat.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -44,7 +44,7 @@
 
 subsection {* Proofs about the natural numbers *}
 
-lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
+schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
 apply (rule_tac n = k in induct)
 apply (rule notI)
 apply (erule Suc_neq_0)
@@ -53,7 +53,7 @@
 apply (erule Suc_inject)
 done
 
-lemma "?p : (k+m)+n = k+(m+n)"
+schematic_lemma "?p : (k+m)+n = k+(m+n)"
 apply (rule induct)
 back
 back
@@ -63,23 +63,23 @@
 back
 oops
 
-lemma add_0 [simp]: "?p : 0+n = n"
+schematic_lemma add_0 [simp]: "?p : 0+n = n"
 apply (unfold add_def)
 apply (rule rec_0)
 done
 
-lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
+schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
 apply (unfold add_def)
 apply (rule rec_Suc)
 done
 
 
-lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
+schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
   apply (erule subst)
   apply (rule refl)
   done
 
-lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
+schematic_lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
   apply (erule subst, erule subst, rule refl)
   done
 
@@ -89,19 +89,19 @@
   val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
 *}
 
-lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
+schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
 apply (rule_tac n = k in induct)
 apply (tactic {* SIMP_TAC add_ss 1 *})
 apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
 done
 
-lemma add_0_right: "?p : m+0 = m"
+schematic_lemma add_0_right: "?p : m+0 = m"
 apply (rule_tac n = m in induct)
 apply (tactic {* SIMP_TAC add_ss 1 *})
 apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
 done
 
-lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
+schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
 apply (rule_tac n = m in induct)
 apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
 done