src/Sequents/LK/Nat.thy
 author wenzelm Sat Feb 01 18:00:28 2014 +0100 (2014-02-01) changeset 55229 08f2ebb65078 parent 55228 901a6696cdd8 child 55230 cb5ef74b32f9 permissions -rw-r--r--
simplified sessions;
```     1 (*  Title:      Sequents/LK/Nat.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1999  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
```
```     7
```
```     8 theory Nat
```
```     9 imports "../LK"
```
```    10 begin
```
```    11
```
```    12 typedecl nat
```
```    13 arities nat :: "term"
```
```    14
```
```    15 axiomatization
```
```    16   Zero :: nat      ("0") and
```
```    17   Suc :: "nat=>nat" and
```
```    18   rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
```
```    19 where
```
```    20   induct:  "[| \$H |- \$E, P(0), \$F;
```
```    21               !!x. \$H, P(x) |- \$E, P(Suc(x)), \$F |] ==> \$H |- \$E, P(n), \$F" and
```
```    22
```
```    23   Suc_inject:  "|- Suc(m)=Suc(n) --> m=n" and
```
```    24   Suc_neq_0:   "|- Suc(m) ~= 0" and
```
```    25   rec_0:       "|- rec(0,a,f) = a" and
```
```    26   rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
```
```    27
```
```    28 definition add :: "[nat, nat] => nat"  (infixl "+" 60)
```
```    29   where "m + n == rec(m, n, %x y. Suc(y))"
```
```    30
```
```    31
```
```    32 declare Suc_neq_0 [simp]
```
```    33
```
```    34 lemma Suc_inject_rule: "\$H, \$G, m = n |- \$E \<Longrightarrow> \$H, Suc(m) = Suc(n), \$G |- \$E"
```
```    35   by (rule L_of_imp [OF Suc_inject])
```
```    36
```
```    37 lemma Suc_n_not_n: "|- Suc(k) ~= k"
```
```    38   apply (rule_tac n = k in induct)
```
```    39   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *})
```
```    40   apply (fast add!: Suc_inject_rule)
```
```    41   done
```
```    42
```
```    43 lemma add_0: "|- 0+n = n"
```
```    44   apply (unfold add_def)
```
```    45   apply (rule rec_0)
```
```    46   done
```
```    47
```
```    48 lemma add_Suc: "|- Suc(m)+n = Suc(m+n)"
```
```    49   apply (unfold add_def)
```
```    50   apply (rule rec_Suc)
```
```    51   done
```
```    52
```
```    53 declare add_0 [simp] add_Suc [simp]
```
```    54
```
```    55 lemma add_assoc: "|- (k+m)+n = k+(m+n)"
```
```    56   apply (rule_tac n = "k" in induct)
```
```    57   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
```
```    58   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
```
```    59   done
```
```    60
```
```    61 lemma add_0_right: "|- m+0 = m"
```
```    62   apply (rule_tac n = "m" in induct)
```
```    63   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
```
```    64   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
```
```    65   done
```
```    66
```
```    67 lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
```
```    68   apply (rule_tac n = "m" in induct)
```
```    69   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
```
```    70   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
```
```    71   done
```
```    72
```
```    73 lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
```
```    74   apply (rule_tac n = "i" in induct)
```
```    75   apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
```
```    76   apply (tactic {* asm_simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
```
```    77   done
```
```    78
```
```    79 end
```