src/Sequents/LK/Nat.thy
author paulson <lp15@cam.ac.uk>
Mon Jun 11 14:34:17 2018 +0100 (15 months ago)
changeset 68424 02e5a44ffe7d
parent 61386 0a29a984a91b
permissions -rw-r--r--
the last of the infinite product proofs
wenzelm@17481
     1
(*  Title:      Sequents/LK/Nat.thy
paulson@7091
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7095
     3
    Copyright   1999  University of Cambridge
paulson@7091
     4
*)
paulson@7091
     5
wenzelm@60770
     6
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
wenzelm@17481
     7
wenzelm@17481
     8
theory Nat
wenzelm@55229
     9
imports "../LK"
wenzelm@17481
    10
begin
wenzelm@17481
    11
wenzelm@17481
    12
typedecl nat
wenzelm@55380
    13
instance nat :: "term" ..
paulson@7091
    14
wenzelm@51309
    15
axiomatization
wenzelm@51309
    16
  Zero :: nat      ("0") and
wenzelm@61385
    17
  Suc :: "nat \<Rightarrow> nat" and
wenzelm@61385
    18
  rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a"
wenzelm@51309
    19
where
wenzelm@61386
    20
  induct:  "\<lbrakk>$H \<turnstile> $E, P(0), $F;
wenzelm@61386
    21
             \<And>x. $H, P(x) \<turnstile> $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P(n), $F" and
paulson@7095
    22
wenzelm@61386
    23
  Suc_inject:  "\<turnstile> Suc(m) = Suc(n) \<longrightarrow> m = n" and
wenzelm@61386
    24
  Suc_neq_0:   "\<turnstile> Suc(m) \<noteq> 0" and
wenzelm@61386
    25
  rec_0:       "\<turnstile> rec(0,a,f) = a" and
wenzelm@61386
    26
  rec_Suc:     "\<turnstile> rec(Suc(m), a, f) = f(m, rec(m,a,f))"
wenzelm@51309
    27
wenzelm@61385
    28
definition add :: "[nat, nat] \<Rightarrow> nat"  (infixl "+" 60)
wenzelm@61385
    29
  where "m + n == rec(m, n, \<lambda>x y. Suc(y))"
wenzelm@17481
    30
wenzelm@21426
    31
wenzelm@21426
    32
declare Suc_neq_0 [simp]
wenzelm@21426
    33
wenzelm@61386
    34
lemma Suc_inject_rule: "$H, $G, m = n \<turnstile> $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G \<turnstile> $E"
wenzelm@21426
    35
  by (rule L_of_imp [OF Suc_inject])
wenzelm@21426
    36
wenzelm@61386
    37
lemma Suc_n_not_n: "\<turnstile> Suc(k) \<noteq> k"
wenzelm@21426
    38
  apply (rule_tac n = k in induct)
wenzelm@55230
    39
  apply simp
wenzelm@55228
    40
  apply (fast add!: Suc_inject_rule)
wenzelm@21426
    41
  done
wenzelm@21426
    42
wenzelm@61386
    43
lemma add_0: "\<turnstile> 0 + n = n"
wenzelm@21426
    44
  apply (unfold add_def)
wenzelm@21426
    45
  apply (rule rec_0)
wenzelm@21426
    46
  done
wenzelm@21426
    47
wenzelm@61386
    48
lemma add_Suc: "\<turnstile> Suc(m) + n = Suc(m + n)"
wenzelm@21426
    49
  apply (unfold add_def)
wenzelm@21426
    50
  apply (rule rec_Suc)
wenzelm@21426
    51
  done
wenzelm@21426
    52
wenzelm@21426
    53
declare add_0 [simp] add_Suc [simp]
wenzelm@21426
    54
wenzelm@61386
    55
lemma add_assoc: "\<turnstile> (k + m) + n = k + (m + n)"
wenzelm@21426
    56
  apply (rule_tac n = "k" in induct)
wenzelm@55230
    57
  apply simp_all
wenzelm@21426
    58
  done
wenzelm@21426
    59
wenzelm@61386
    60
lemma add_0_right: "\<turnstile> m + 0 = m"
wenzelm@21426
    61
  apply (rule_tac n = "m" in induct)
wenzelm@55230
    62
  apply simp_all
wenzelm@21426
    63
  done
wenzelm@21426
    64
wenzelm@61386
    65
lemma add_Suc_right: "\<turnstile> m + Suc(n) = Suc(m + n)"
wenzelm@21426
    66
  apply (rule_tac n = "m" in induct)
wenzelm@55230
    67
  apply simp_all
wenzelm@21426
    68
  done
wenzelm@21426
    69
wenzelm@61386
    70
lemma "(\<And>n. \<turnstile> f(Suc(n)) = Suc(f(n))) \<Longrightarrow> \<turnstile> f(i + j) = i + f(j)"
wenzelm@21426
    71
  apply (rule_tac n = "i" in induct)
wenzelm@55230
    72
  apply simp_all
wenzelm@21426
    73
  done
wenzelm@17481
    74
paulson@7091
    75
end