src/FOL/ex/NatClass.thy
 author haftmann Tue, 10 Jul 2007 17:30:50 +0200 changeset 23709 fd31da8f752a parent 21404 eb85850d3eb7 child 29751 e2756594c414 permissions -rw-r--r--
moved lfp_induct2 here

(*  Title:      FOL/ex/NatClass.thy
ID:         $Id$
Author:     Markus Wenzel, TU Muenchen
*)

theory NatClass
imports FOL
begin

text {*
This is an abstract version of theory @{text "Nat"}. Instead of
axiomatizing a single type @{text nat} we define the class of all
these types (up to isomorphism).

because class axioms may not contain more than one type variable.
*}

consts
0 :: 'a    ("0")
Suc :: "'a => 'a"
rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"

axclass
nat < "term"
induct:        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
Suc_inject:    "Suc(m) = Suc(n) ==> m = n"
Suc_neq_0:     "Suc(m) = 0 ==> R"
rec_0:         "rec(0, a, f) = a"
rec_Suc:       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"

definition
add :: "['a::nat, 'a] => 'a"  (infixl "+" 60) where
"m + n = rec(m, n, %x y. Suc(y))"

lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
apply (rule_tac n = k in induct)
apply (rule notI)
apply (erule Suc_neq_0)
apply (rule notI)
apply (erule notE)
apply (erule Suc_inject)
done

lemma "(k+m)+n = k+(m+n)"
apply (rule induct)
back
back
back
back
back
back
oops

lemma add_0 [simp]: "0+n = n"
apply (rule rec_0)
done

lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
apply (rule rec_Suc)
done

apply (rule_tac n = k in induct)
apply simp
apply simp
done

apply (rule_tac n = m in induct)
apply simp
apply simp
done

apply (rule_tac n = m in induct)
apply simp_all
done

lemma
assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
shows "f(i+j) = i+f(j)"
apply (rule_tac n = i in induct)
apply simp