src/FOLP/ex/Nat.thy
author paulson
Thu, 14 Jun 2018 14:23:48 +0100
changeset 68446 92ddca1edc43
parent 61337 4645502c3c64
child 69593 3dda49e08b9d
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41777
1f7cbe39d425 more precise headers;
wenzelm
parents: 41310
diff changeset
     1
(*  Title:      FOLP/ex/Nat.thy
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
     6
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     7
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     8
theory Nat
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     9
imports FOLP
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    10
begin
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    11
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    12
typedecl nat
55380
4de48353034e prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents: 51306
diff changeset
    13
instance nat :: "term" ..
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    14
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    15
axiomatization
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    16
  Zero :: nat    ("0") and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    17
  Suc :: "nat => nat" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    18
  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  (*Proof terms*)
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    21
  nrec :: "[nat, p, [nat, p] => p] => p" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    22
  ninj :: "p => p" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    23
  nneq :: "p => p" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    24
  rec0 :: "p" and
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    25
  recSuc :: "p"
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    26
where
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    27
  induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    28
              |] ==> nrec(n,b,c):P(n)" and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    30
  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    31
  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    32
  rec_0:      "rec0 : rec(0,a,f) = a" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    33
  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    34
  nrecB0:     "b: A ==> nrec(0,b,c) = b : A" and
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    35
  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    36
51306
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    37
definition add :: "[nat, nat] => nat"    (infixl "+" 60)
f0e5af7aa68b eliminated legacy 'axioms';
wenzelm
parents: 41777
diff changeset
    38
  where "m + n == rec(m, n, %x y. Suc(y))"
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    39
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    40
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    41
subsection \<open>Proofs about the natural numbers\<close>
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    42
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    43
schematic_goal Suc_n_not_n: "?p : ~ (Suc(k) = k)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    44
apply (rule_tac n = k in induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    45
apply (rule notI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    46
apply (erule Suc_neq_0)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    47
apply (rule notI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    48
apply (erule notE)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    49
apply (erule Suc_inject)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    50
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    51
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    52
schematic_goal "?p : (k+m)+n = k+(m+n)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    53
apply (rule induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    54
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    55
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    56
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    57
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    58
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    59
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    60
oops
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    61
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    62
schematic_goal add_0 [simp]: "?p : 0+n = n"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    63
apply (unfold add_def)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    64
apply (rule rec_0)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    65
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    66
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    67
schematic_goal add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    68
apply (unfold add_def)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    69
apply (rule rec_Suc)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    70
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    71
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    72
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    73
schematic_goal Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    74
  apply (erule subst)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    75
  apply (rule refl)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    76
  done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    77
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    78
schematic_goal Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    79
  apply (erule subst, erule subst, rule refl)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    80
  done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    81
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    82
lemmas nat_congs = Suc_cong Plus_cong
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    83
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    84
ML \<open>
60644
4af8b9c2b52f clarified context;
wenzelm
parents: 58889
diff changeset
    85
  val add_ss =
4af8b9c2b52f clarified context;
wenzelm
parents: 58889
diff changeset
    86
    FOLP_ss addcongs @{thms nat_congs}
4af8b9c2b52f clarified context;
wenzelm
parents: 58889
diff changeset
    87
    |> fold (addrew @{context}) @{thms add_0 add_Suc}
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    88
\<close>
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    89
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    90
schematic_goal add_assoc: "?p : (k+m)+n = k+(m+n)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    91
apply (rule_tac n = k in induct)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    92
apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>)
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    93
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    94
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    95
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    96
schematic_goal add_0_right: "?p : m+0 = m"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    97
apply (rule_tac n = m in induct)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    98
apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>)
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
    99
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   100
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   101
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   102
schematic_goal add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   103
apply (rule_tac n = m in induct)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60646
diff changeset
   104
apply (tactic \<open>ALLGOALS (ASM_SIMP_TAC @{context} add_ss)\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   105
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   106
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   107
(*mk_typed_congs appears not to work with FOLP's version of subst*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
   108
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
end