src/Sequents/LK/Nat.thy
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 35762 af3ff2ba4c54
child 41310 65631ca437c9
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
     1
(*  Title:      Sequents/LK/Nat.thy
7091
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
7095
cfc11af6174a fixed the comments...
paulson
parents: 7091
diff changeset
     3
    Copyright   1999  University of Cambridge
7091
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
     4
*)
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
     5
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
     6
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
     7
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
     8
theory Nat
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
     9
imports LK
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    10
begin
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    11
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    12
typedecl nat
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    13
arities nat :: "term"
7091
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
    14
consts  "0" :: nat      ("0")
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    15
        Suc :: "nat=>nat"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    16
        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    17
        add :: "[nat, nat] => nat"                (infixl "+" 60)
7091
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
    18
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    19
axioms
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    20
  induct:  "[| $H |- $E, P(0), $F;
7123
4ab38de3fd20 congruence rule for |-, etc.
paulson
parents: 7095
diff changeset
    21
              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
7095
cfc11af6174a fixed the comments...
paulson
parents: 7091
diff changeset
    22
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    23
  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    24
  Suc_neq_0:   "|- Suc(m) ~= 0"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    25
  rec_0:       "|- rec(0,a,f) = a"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    26
  rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    27
  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    28
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    29
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    30
declare Suc_neq_0 [simp]
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    31
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    32
lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    33
  by (rule L_of_imp [OF Suc_inject])
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    34
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    35
lemma Suc_n_not_n: "|- Suc(k) ~= k"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    36
  apply (rule_tac n = k in induct)
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    37
  apply (tactic {* simp_tac (LK_ss addsimps @{thms Suc_neq_0}) 1 *})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    38
  apply (tactic {* fast_tac (LK_pack add_safes @{thms Suc_inject_rule}) 1 *})
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    39
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    40
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    41
lemma add_0: "|- 0+n = n"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    42
  apply (unfold add_def)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    43
  apply (rule rec_0)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    44
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    45
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    46
lemma add_Suc: "|- Suc(m)+n = Suc(m+n)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    47
  apply (unfold add_def)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    48
  apply (rule rec_Suc)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    49
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    50
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    51
declare add_0 [simp] add_Suc [simp]
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    52
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    53
lemma add_assoc: "|- (k+m)+n = k+(m+n)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    54
  apply (rule_tac n = "k" in induct)
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    55
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    56
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    57
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    58
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    59
lemma add_0_right: "|- m+0 = m"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    60
  apply (rule_tac n = "m" in induct)
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    61
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    62
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    63
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    64
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    65
lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    66
  apply (rule_tac n = "m" in induct)
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    67
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    68
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    69
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    70
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    71
lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    72
  apply (rule_tac n = "i" in induct)
22896
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    73
  apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})
1c2abcabea61 tuned ML setup;
wenzelm
parents: 21426
diff changeset
    74
  apply (tactic {* asm_simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
    75
  done
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 7123
diff changeset
    76
7091
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
diff changeset
    77
end