Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.
(* Title: HOL/Nat.thy
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Definition of types ind and nat.
Type nat is defined as a set Nat over type ind.
*)
Nat = WF +
(** type ind **)
types
ind
arities
ind :: term
consts
Zero_Rep :: ind
Suc_Rep :: ind => ind
rules
(*the axiom of infinity in 2 parts*)
inj_Suc_Rep "inj(Suc_Rep)"
Suc_Rep_not_Zero_Rep "Suc_Rep(x) ~= Zero_Rep"
(** type nat **)
(* type definition *)
typedef (Nat)
nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def)
instance
nat :: ord
(* abstract constants and syntax *)
consts
"0" :: nat ("0")
Suc :: nat => nat
nat_case :: ['a, nat => 'a, nat] => 'a
pred_nat :: "(nat * nat) set"
nat_rec :: [nat, 'a, [nat, 'a] => 'a] => 'a
translations
"case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
defs
Zero_def "0 == Abs_Nat(Zero_Rep)"
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
(*nat operations and recursion*)
nat_case_def "nat_case a f n == @z. (n=0 --> z=a)
& (!x. n=Suc(x) --> z=f(x))"
pred_nat_def "pred_nat == {p. ? n. p = (n, Suc(n))}"
less_def "m<n == (m,n):trancl(pred_nat)"
le_def "m<=(n::nat) == ~(n<m)"
nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
end