src/FOLP/ex/Nat.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 41310 65631ca437c9
     1.1 --- a/src/FOLP/ex/Nat.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOLP/ex/Nat.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  subsection {* Proofs about the natural numbers *}
     1.6  
     1.7 -lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
     1.8 +schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
     1.9  apply (rule_tac n = k in induct)
    1.10  apply (rule notI)
    1.11  apply (erule Suc_neq_0)
    1.12 @@ -53,7 +53,7 @@
    1.13  apply (erule Suc_inject)
    1.14  done
    1.15  
    1.16 -lemma "?p : (k+m)+n = k+(m+n)"
    1.17 +schematic_lemma "?p : (k+m)+n = k+(m+n)"
    1.18  apply (rule induct)
    1.19  back
    1.20  back
    1.21 @@ -63,23 +63,23 @@
    1.22  back
    1.23  oops
    1.24  
    1.25 -lemma add_0 [simp]: "?p : 0+n = n"
    1.26 +schematic_lemma add_0 [simp]: "?p : 0+n = n"
    1.27  apply (unfold add_def)
    1.28  apply (rule rec_0)
    1.29  done
    1.30  
    1.31 -lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
    1.32 +schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
    1.33  apply (unfold add_def)
    1.34  apply (rule rec_Suc)
    1.35  done
    1.36  
    1.37  
    1.38 -lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
    1.39 +schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
    1.40    apply (erule subst)
    1.41    apply (rule refl)
    1.42    done
    1.43  
    1.44 -lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
    1.45 +schematic_lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
    1.46    apply (erule subst, erule subst, rule refl)
    1.47    done
    1.48  
    1.49 @@ -89,19 +89,19 @@
    1.50    val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
    1.51  *}
    1.52  
    1.53 -lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
    1.54 +schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
    1.55  apply (rule_tac n = k in induct)
    1.56  apply (tactic {* SIMP_TAC add_ss 1 *})
    1.57  apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
    1.58  done
    1.59  
    1.60 -lemma add_0_right: "?p : m+0 = m"
    1.61 +schematic_lemma add_0_right: "?p : m+0 = m"
    1.62  apply (rule_tac n = m in induct)
    1.63  apply (tactic {* SIMP_TAC add_ss 1 *})
    1.64  apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
    1.65  done
    1.66  
    1.67 -lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
    1.68 +schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
    1.69  apply (rule_tac n = m in induct)
    1.70  apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
    1.71  done