src/FOLP/ex/Nat.thy
author wenzelm
Sun, 27 Jan 2008 20:04:32 +0100
changeset 25991 31b38a39e589
parent 17480 fd19f77dcf60
child 35762 af3ff2ba4c54
permissions -rw-r--r--
eliminated some legacy ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
     1
(*  Title:      FOLP/ex/nat.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     7
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     8
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
     9
theory Nat
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    10
imports FOLP
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    11
begin
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    12
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    13
typedecl nat
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    14
arities nat :: "term"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    15
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    16
consts
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    17
  0 :: nat    ("0")
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    18
  Suc :: "nat => nat"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    19
  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    20
  add :: "[nat, nat] => nat"    (infixl "+" 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  (*Proof terms*)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    23
  nrec :: "[nat, p, [nat, p] => p] => p"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    24
  ninj :: "p => p"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    25
  nneq :: "p => p"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    26
  rec0 :: "p"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    27
  recSuc :: "p"
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    28
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    29
axioms
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    30
  induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    31
              |] ==> nrec(n,b,c):P(n)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    33
  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    34
  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    35
  rec_0:      "rec0 : rec(0,a,f) = a"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    36
  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    37
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    38
defs
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    39
  add_def:    "m+n == rec(m, n, %x y. Suc(y))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    41
axioms
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    42
  nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    43
  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 1477
diff changeset
    44
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    45
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    46
subsection {* Proofs about the natural numbers *}
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    47
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    48
lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    49
apply (rule_tac n = k in induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    50
apply (rule notI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    51
apply (erule Suc_neq_0)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    52
apply (rule notI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    53
apply (erule notE)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    54
apply (erule Suc_inject)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    55
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    56
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    57
lemma "?p : (k+m)+n = k+(m+n)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    58
apply (rule induct)
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
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    61
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    62
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    63
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    64
back
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    65
oops
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    66
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    67
lemma add_0 [simp]: "?p : 0+n = n"
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_0)
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
lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    73
apply (unfold add_def)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    74
apply (rule rec_Suc)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    75
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    76
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    77
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    78
lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    79
  apply (erule subst)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    80
  apply (rule refl)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    81
  done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    82
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    83
lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    84
  apply (erule subst, erule subst, rule refl)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    85
  done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    86
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    87
lemmas nat_congs = Suc_cong Plus_cong
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    88
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    89
ML {*
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    90
  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    91
*}
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    92
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    93
lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    94
apply (rule_tac n = k in induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    95
apply (tactic {* SIMP_TAC add_ss 1 *})
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    96
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    97
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    98
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
    99
lemma add_0_right: "?p : m+0 = m"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   100
apply (rule_tac n = m in induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   101
apply (tactic {* SIMP_TAC add_ss 1 *})
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   102
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   103
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   104
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   105
lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   106
apply (rule_tac n = m in induct)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   107
apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   108
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   109
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 17480
diff changeset
   110
(*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
   111
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
end