--- a/src/ZF/Coind/ECR.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Coind/ECR.thy Sat Dec 29 18:36:12 2001 +0100
@@ -46,8 +46,9 @@
(* Specialised elimination rules *)
-inductive_cases htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
-inductive_cases htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel"
+inductive_cases
+ htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
+ and htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel"
(* Properties of the pointwise extension to environments *)
--- a/src/ZF/Coind/Static.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Coind/Static.thy Sat Dec 29 18:36:12 2001 +0100
@@ -54,11 +54,12 @@
type_intros te_appI Exp.intros Ty.intros
-inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
-inductive_cases elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
-inductive_cases elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
-inductive_cases elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
-inductive_cases elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
+inductive_cases
+ elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
+ and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
+ and elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
+ and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
+ and elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
declare ElabRel.dom_subset [THEN subsetD, dest]
--- a/src/ZF/IMP/Com.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/IMP/Com.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,160 +1,139 @@
(* Title: ZF/IMP/Com.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
+*)
-Arithmetic expressions, Boolean expressions, Commands
-
-And their Operational semantics
-*)
+header {* Arithmetic expressions, boolean expressions, commands *}
theory Com = Main:
-(** Arithmetic expressions **)
-consts loc :: i
- aexp :: i
+
+subsection {* Arithmetic expressions *}
-datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
- "aexp" = N ("n \<in> nat")
- | X ("x \<in> loc")
- | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
- | Op2 ("f \<in> (nat*nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
+consts
+ loc :: i
+ aexp :: i
+
+datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> nat) -> nat))"
+ aexp = N ("n \<in> nat")
+ | X ("x \<in> loc")
+ | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
+ | Op2 ("f \<in> (nat \<times> nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
-(** Evaluation of arithmetic expressions **)
-consts evala :: "i"
- "-a->" :: "[i,i] => o" (infixl 50)
-translations
- "p -a-> n" == "<p,n> \<in> evala"
+consts evala :: i
+syntax "_evala" :: "[i, i] => o" (infixl "-a->" 50)
+translations "p -a-> n" == "<p,n> \<in> evala"
+
inductive
- domains "evala" <= "(aexp * (loc -> nat)) * nat"
- intros
+ domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
+ intros
N: "[| n \<in> nat; sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n"
X: "[| x \<in> loc; sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
- Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat*nat) -> nat |]
+ Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat\<times>nat) -> nat |]
==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
type_intros aexp.intros apply_funtype
-(** Boolean expressions **)
-consts bexp :: i
+subsection {* Boolean expressions *}
+
+consts bexp :: i
-datatype <= "univ(aexp Un ((nat*nat)->bool) )"
- "bexp" = true
- | false
- | ROp ("f \<in> (nat*nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
- | noti ("b \<in> bexp")
- | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
- | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
+datatype \<subseteq> "univ(aexp \<union> ((nat \<times> nat)->bool))"
+ bexp = true
+ | false
+ | ROp ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
+ | noti ("b \<in> bexp")
+ | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
+ | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
-(** Evaluation of boolean expressions **)
-consts evalb :: "i"
- "-b->" :: "[i,i] => o" (infixl 50)
-
-translations
- "p -b-> b" == "<p,b> \<in> evalb"
+consts evalb :: i
+syntax "_evalb" :: "[i,i] => o" (infixl "-b->" 50)
+translations "p -b-> b" == "<p,b> \<in> evalb"
inductive
- domains "evalb" <= "(bexp * (loc -> nat)) * bool"
- intros (*avoid clash with ML constructors true, false*)
- tru: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
- fls: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
- ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |]
+ domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
+ intros
+ true: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
+ false: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
+ ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |]
==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
noti: "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
- andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
==> <b0 andi b1,sigma> -b-> (w0 and w1)"
- ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
==> <b0 ori b1,sigma> -b-> (w0 or w1)"
- type_intros bexp.intros
+ type_intros bexp.intros
apply_funtype and_type or_type bool_1I bool_0I not_type
type_elims evala.dom_subset [THEN subsetD, elim_format]
-(** Commands **)
-consts com :: i
-
-datatype
- "com" = skip
- | asgt ("x \<in> loc", "a \<in> aexp") (infixl 60)
- | semic("c0 \<in> com", "c1 \<in> com") ("_; _" [60, 60] 10)
- | while("b \<in> bexp", "c \<in> com") ("while _ do _" 60)
- | ifc ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("ifc _ then _ else _" 60)
+subsection {* Commands *}
-(*Constructor ";" has low precedence to avoid syntactic ambiguities
- with [| m \<in> nat; x \<in> loc; ... |] ==> ... It usually will need parentheses.*)
+consts com :: i
+datatype com =
+ skip ("\<SKIP>" [])
+ | assignment ("x \<in> loc", "a \<in> aexp") (infixl "\<ASSN>" 60)
+ | semicolon ("c0 \<in> com", "c1 \<in> com") ("_\<SEQ> _" [60, 60] 10)
+ | while ("b \<in> bexp", "c \<in> com") ("\<WHILE> _ \<DO> _" 60)
+ | if ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
-(** Execution of commands **)
-consts evalc :: "i"
- "-c->" :: "[i,i] => o" (infixl 50)
-translations
- "p -c-> s" == "<p,s> \<in> evalc"
+consts evalc :: i
+syntax "_evalc" :: "[i, i] => o" (infixl "-c->" 50)
+translations "p -c-> s" == "<p,s> \<in> evalc"
inductive
- domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
+ domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
intros
- skip: "[| sigma \<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
+ skip: "[| sigma \<in> loc -> nat |] ==> <\<SKIP>,sigma> -c-> sigma"
- assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |]
- ==> <x asgt a,sigma> -c-> sigma(x:=m)"
+ assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |]
+ ==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)"
- semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |]
- ==> <c0 ; c1, sigma> -c-> sigma1"
+ semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |]
+ ==> <c0\<SEQ> c1, sigma> -c-> sigma1"
- ifc1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;
- <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
- ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
+ if1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;
+ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
+ ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
- ifc0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;
- <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
- ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
+ if0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;
+ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
+ ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
- while0: "[| c \<in> com; <b, sigma> -b-> 0 |]
- ==> <while b do c,sigma> -c-> sigma"
+ while0: "[| c \<in> com; <b, sigma> -b-> 0 |]
+ ==> <\<WHILE> b \<DO> c,sigma> -c-> sigma"
- while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
- <while b do c, sigma2> -c-> sigma1 |]
- ==> <while b do c, sigma> -c-> sigma1"
+ while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
+ <\<WHILE> b \<DO> c, sigma2> -c-> sigma1 |]
+ ==> <\<WHILE> b \<DO> c, sigma> -c-> sigma1"
type_intros com.intros update_type
type_elims evala.dom_subset [THEN subsetD, elim_format]
evalb.dom_subset [THEN subsetD, elim_format]
-(*** type_intros for evala ***)
+subsection {* Misc lemmas *}
-lemmas evala_1 [simp] =
- evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
-lemmas evala_2 [simp] =
- evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
-lemmas evala_3 [simp] =
- evala.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+ and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+ and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2]
-
-(*** type_intros for evalb ***)
+lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+ and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+ and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2]
-lemmas evalb_1 [simp] =
- evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
-lemmas evalb_2 [simp] =
- evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
-lemmas evalb_3 [simp] =
- evalb.dom_subset [THEN subsetD, THEN SigmaD2]
-
-(*** type_intros for evalc ***)
+lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+ and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+ and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2]
-lemmas evalc_1 [simp] =
- evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
-lemmas evalc_2 [simp] =
- evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
-lemmas evalc_3 [simp] =
- evalc.dom_subset [THEN subsetD, THEN SigmaD2]
-
-inductive_cases evala_N_E [elim!]: "<N(n),sigma> -a-> i"
-inductive_cases evala_X_E [elim!]: "<X(x),sigma> -a-> i"
-inductive_cases evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
-inductive_cases evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i"
+inductive_cases
+ evala_N_E [elim!]: "<N(n),sigma> -a-> i"
+ and evala_X_E [elim!]: "<X(x),sigma> -a-> i"
+ and evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
+ and evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i"
end
--- a/src/ZF/IMP/Denotation.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/IMP/Denotation.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,13 +1,13 @@
(* Title: ZF/IMP/Denotation.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
+*)
-Denotational semantics of expressions & commands
-*)
+header {* Denotational semantics of expressions and commands *}
theory Denotation = Com:
+subsection {* Definitions *}
consts
A :: "i => i => i"
@@ -15,73 +15,59 @@
C :: "i => i"
constdefs
- Gamma :: "[i,i,i] => i"
- "Gamma(b,cden) == (%phi.{io \<in> (phi O cden). B(b,fst(io))=1} Un
- {io \<in> id(loc->nat). B(b,fst(io))=0})"
+ Gamma :: "[i,i,i] => i" ("\<Gamma>")
+ "\<Gamma>(b,cden) ==
+ (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>
+ {io \<in> id(loc->nat). B(b,fst(io))=0})"
primrec
- "A(N(n), sigma) = n"
- "A(X(x), sigma) = sigma`x"
- "A(Op1(f,a), sigma) = f`A(a,sigma)"
- "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
-
-
-primrec
- "B(true, sigma) = 1"
- "B(false, sigma) = 0"
- "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
- "B(noti(b), sigma) = not(B(b,sigma))"
- "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
- "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
-
+ "A(N(n), sigma) = n"
+ "A(X(x), sigma) = sigma`x"
+ "A(Op1(f,a), sigma) = f`A(a,sigma)"
+ "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
primrec
- "C(skip) = id(loc->nat)"
-
- "C(x asgt a) = {io:(loc->nat)*(loc->nat).
- snd(io) = fst(io)(x := A(a,fst(io)))}"
+ "B(true, sigma) = 1"
+ "B(false, sigma) = 0"
+ "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
+ "B(noti(b), sigma) = not(B(b,sigma))"
+ "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
+ "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
- "C(c0 ; c1) = C(c1) O C(c0)"
-
- "C(ifc b then c0 else c1) = {io \<in> C(c0). B(b,fst(io))=1} Un
- {io \<in> C(c1). B(b,fst(io))=0}"
-
- "C(while b do c) = lfp((loc->nat)*(loc->nat), Gamma(b,C(c)))"
+primrec
+ "C(\<SKIP>) = id(loc->nat)"
+ "C(x \<ASSN> a) =
+ {io \<in> (loc->nat) \<times> (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}"
+ "C(c0\<SEQ> c1) = C(c1) O C(c0)"
+ "C(\<IF> b \<THEN> c0 \<ELSE> c1) =
+ {io \<in> C(c0). B(b,fst(io)) = 1} \<union> {io \<in> C(c1). B(b,fst(io)) = 0}"
+ "C(\<WHILE> b \<DO> c) = lfp((loc->nat) \<times> (loc->nat), \<Gamma>(b,C(c)))"
-(** Type_intr for A **)
+subsection {* Misc lemmas *}
lemma A_type [TC]: "[|a \<in> aexp; sigma \<in> loc->nat|] ==> A(a,sigma) \<in> nat"
-by (erule aexp.induct, simp_all)
-
-
-(** Type_intr for B **)
+ by (erule aexp.induct) simp_all
lemma B_type [TC]: "[|b \<in> bexp; sigma \<in> loc->nat|] ==> B(b,sigma) \<in> bool"
by (erule bexp.induct, simp_all)
-(** C_subset **)
-
-lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat)*(loc->nat)"
-apply (erule com.induct)
-apply simp_all
-apply (blast dest: lfp_subset [THEN subsetD])+
-done
-
-(** Type_elims for C **)
+lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat) \<times> (loc->nat)"
+ apply (erule com.induct)
+ apply simp_all
+ apply (blast dest: lfp_subset [THEN subsetD])+
+ done
lemma C_type_D [dest]:
- "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
-by (blast dest: C_subset [THEN subsetD])
+ "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
+ by (blast dest: C_subset [THEN subsetD])
lemma C_type_fst [dest]: "[| x \<in> C(c); c \<in> com |] ==> fst(x) \<in> loc->nat"
-by (auto dest!: C_subset [THEN subsetD])
-
-(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
+ by (auto dest!: C_subset [THEN subsetD])
-lemma Gamma_bnd_mono:
- "cden <= (loc->nat)*(loc->nat)
- ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,cden))"
-by (unfold bnd_mono_def Gamma_def, blast)
+lemma Gamma_bnd_mono:
+ "cden \<subseteq> (loc->nat) \<times> (loc->nat)
+ ==> bnd_mono ((loc->nat) \<times> (loc->nat), \<Gamma>(b,cden))"
+ by (unfold bnd_mono_def Gamma_def) blast
end
--- a/src/ZF/IMP/Equiv.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/IMP/Equiv.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,87 +1,87 @@
(* Title: ZF/IMP/Equiv.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
+ Author: Heiko Loetzbeyer and Robert Sandner, TU München
*)
+header {* Equivalence *}
+
theory Equiv = Denotation + Com:
lemma aexp_iff [rule_format]:
- "[| a \<in> aexp; sigma: loc -> nat |]
- ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
-apply (erule aexp.induct)
-apply (force intro!: evala.intros)+
-done
+ "[| a \<in> aexp; sigma: loc -> nat |]
+ ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
+ apply (erule aexp.induct)
+ apply (force intro!: evala.intros)+
+ done
declare aexp_iff [THEN iffD1, simp]
aexp_iff [THEN iffD2, intro!]
-inductive_cases [elim!]: "<true,sigma> -b-> x"
-inductive_cases [elim!]: "<false,sigma> -b-> x"
-inductive_cases [elim!]: "<ROp(f,a0,a1),sigma> -b-> x"
-inductive_cases [elim!]: "<noti(b),sigma> -b-> x"
-inductive_cases [elim!]: "<b0 andi b1,sigma> -b-> x"
-inductive_cases [elim!]: "<b0 ori b1,sigma> -b-> x"
+inductive_cases [elim!]:
+ "<true,sigma> -b-> x"
+ "<false,sigma> -b-> x"
+ "<ROp(f,a0,a1),sigma> -b-> x"
+ "<noti(b),sigma> -b-> x"
+ "<b0 andi b1,sigma> -b-> x"
+ "<b0 ori b1,sigma> -b-> x"
lemma bexp_iff [rule_format]:
- "[| b \<in> bexp; sigma: loc -> nat |]
- ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
-apply (erule bexp.induct)
-apply (auto intro!: evalb.intros)
-done
+ "[| b \<in> bexp; sigma: loc -> nat |]
+ ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
+ apply (erule bexp.induct)
+ apply (auto intro!: evalb.intros)
+ done
declare bexp_iff [THEN iffD1, simp]
bexp_iff [THEN iffD2, intro!]
lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
-apply (erule evalc.induct)
-apply simp_all
-(* skip *)
-apply fast
-(* assign *)
-apply (simp add: update_type)
-(* comp *)
-apply fast
-(* while *)
-apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
-apply (simp add: Gamma_def)
-apply (force )
-(* recursive case of while *)
-apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
-apply (simp add: Gamma_def)
-apply auto
-done
-
+ apply (erule evalc.induct)
+ apply simp_all
+ txt {* @{text skip} *}
+ apply fast
+ txt {* @{text assign} *}
+ apply (simp add: update_type)
+ txt {* @{text comp} *}
+ apply fast
+ txt {* @{text while} *}
+ apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+ apply (simp add: Gamma_def)
+ apply force
+ txt {* recursive case of @{text while} *}
+ apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+ apply (auto simp add: Gamma_def)
+ done
declare B_type [intro!] A_type [intro!]
declare evalc.intros [intro]
lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
-apply (erule com.induct)
-(* skip *)
-apply force
-(* assign *)
-apply force
-(* comp *)
-apply force
-(* while *)
-apply safe
-apply simp_all
-apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
-apply (unfold Gamma_def)
-apply force
-(* if *)
-apply auto
-done
+ apply (erule com.induct)
+ txt {* @{text skip} *}
+ apply force
+ txt {* @{text assign} *}
+ apply force
+ txt {* @{text comp} *}
+ apply force
+ txt {* @{text while} *}
+ apply safe
+ apply simp_all
+ apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
+ apply (unfold Gamma_def)
+ apply force
+ txt {* @{text if} *}
+ apply auto
+ done
-(**** Proof of Equivalence ****)
+subsection {* Main theorem *}
-lemma com_equivalence:
- "\<forall>c \<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"
-by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
+theorem com_equivalence:
+ "c \<in> com ==> C(c) = {io \<in> (loc->nat) \<times> (loc->nat). <c,fst(io)> -c-> snd(io)}"
+ by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/document/root.bib Sat Dec 29 18:36:12 2001 +0100
@@ -0,0 +1,3 @@
+
+@book{Winskel,author={Glynn Winskel},
+title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/document/root.tex Sat Dec 29 18:36:12 2001 +0100
@@ -0,0 +1,49 @@
+
+\documentclass[a4wide]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\renewcommand{\isachardoublequote}{}
+
+% pretty printing for the Com language
+%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
+\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
+\newcommand{\isasymSKIP}{\CMD{skip}}
+\newcommand{\isasymASSN}{\CMD{:=}}
+\newcommand{\isasymSEQ}{\CMD{;}}
+\newcommand{\isasymIF}{\CMD{if}}
+\newcommand{\isasymTHEN}{\CMD{then}}
+\newcommand{\isasymELSE}{\CMD{else}}
+\newcommand{\isasymWHILE}{\CMD{while}}
+\newcommand{\isasymDO}{\CMD{do}}
+
+\addtolength{\hoffset}{-1cm}
+\addtolength{\textwidth}{2cm}
+
+
+\begin{document}
+
+\title{IMP --- A {\tt WHILE}-language and two semantics}
+\author{Heiko Loetzbeyer and Robert Sandner}
+\maketitle
+
+\parindent 0pt\parskip 0.5ex
+
+\begin{abstract}\noindent
+ The formalization of the denotational and operational semantics of a simple
+ while-language together with an equivalence proof between the two semantics.
+ The whole development essentially formalizes/transcribes chapters 2 and 5 of
+ \cite{Winskel}. A much extended version of this development is found in
+ HOL/IMP of the Isabelle distribution.
+\end{abstract}
+
+\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
--- a/src/ZF/Induct/Acc.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Acc.thy Sat Dec 29 18:36:12 2001 +0100
@@ -2,59 +2,61 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-
-Inductive definition of acc(r)
+*)
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon. Dec 1992.
-*)
+header {* The accessible part of a relation *}
theory Acc = Main:
+text {*
+ Inductive definition of @{text "acc(r)"}; see \cite{paulin-tlca}.
+*}
+
consts
- acc :: "i=>i"
+ acc :: "i => i"
inductive
- domains "acc(r)" <= "field(r)"
+ domains "acc(r)" \<subseteq> "field(r)"
intros
vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
monos Pow_mono
-
-(*The introduction rule must require a \<in> field(r)
- Otherwise acc(r) would be a proper class! *)
+text {*
+ The introduction rule must require @{prop "a \<in> field(r)"},
+ otherwise @{text "acc(r)"} would be a proper class!
-(*The intended introduction rule*)
+ \medskip
+ The intended introduction rule:
+*}
+
lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r); a \<in> field(r) |] ==> a \<in> acc(r)"
-by (blast intro: acc.intros)
+ by (blast intro: acc.intros)
lemma acc_downward: "[| b \<in> acc(r); <a,b>: r |] ==> a \<in> acc(r)"
-by (erule acc.cases, blast)
+ by (erule acc.cases) blast
-lemma acc_induct:
- "[| a \<in> acc(r);
- !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
+lemma acc_induct [induct set: acc]:
+ "[| a \<in> acc(r);
+ !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
|] ==> P(a)"
-apply (erule acc.induct)
-apply (blast intro: acc.intros)
-done
+ by (erule acc.induct) (blast intro: acc.intros)
lemma wf_on_acc: "wf[acc(r)](r)"
-apply (rule wf_onI2)
-apply (erule acc_induct)
-apply fast
-done
+ apply (rule wf_onI2)
+ apply (erule acc_induct)
+ apply fast
+ done
-(* field(r) \<subseteq> acc(r) ==> wf(r) *)
-lemmas acc_wfI = wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf]
+lemma acc_wfI: "field(r) \<subseteq> acc(r) \<Longrightarrow> wf(r)"
+ by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf])
lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)"
-apply (rule subsetI)
-apply (erule wf_induct2, assumption)
-apply (blast intro: accI)+
-done
+ apply (rule subsetI)
+ apply (erule wf_induct2, assumption)
+ apply (blast intro: accI)+
+ done
lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
-by (rule iffI, erule acc_wfD, erule acc_wfI)
+ by (rule iffI, erule acc_wfD, erule acc_wfI)
end
--- a/src/ZF/Induct/Brouwer.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Brouwer.thy Sat Dec 29 18:36:12 2001 +0100
@@ -13,8 +13,8 @@
consts
brouwer :: i
-datatype \\<subseteq> "Vfrom(0, csucc(nat))"
- "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
+datatype \<subseteq> "Vfrom(0, csucc(nat))"
+ "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
monos Pi_mono
type_intros inf_datatype_intrs
@@ -23,16 +23,16 @@
elim: brouwer.cases [unfolded brouwer.con_defs])
lemma brouwer_induct2:
- "[| b \\<in> brouwer;
+ "[| b \<in> brouwer;
P(Zero);
- !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b));
- !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i)
+ !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b));
+ !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i)
|] ==> P(Lim(h))
|] ==> P(b)"
-- {* A nicer induction rule than the standard one. *}
proof -
case rule_context
- assume "b \\<in> brouwer"
+ assume "b \<in> brouwer"
thus ?thesis
apply induct
apply (assumption | rule rule_context)+
@@ -47,26 +47,26 @@
consts
Well :: "[i, i => i] => i"
-datatype \\<subseteq> "Vfrom(A \\<union> (\\<Union>x \\<in> A. B(x)), csucc(nat \\<union> |\\<Union>x \\<in> A. B(x)|))"
+datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
-- {* The union with @{text nat} ensures that the cardinal is infinite. *}
- "Well(A, B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A, B)")
+ "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
monos Pi_mono
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs
-lemma Well_unfold: "Well(A, B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A, B))"
+lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
by (fast intro!: Well.intros [unfolded Well.con_defs]
elim: Well.cases [unfolded Well.con_defs])
lemma Well_induct2:
- "[| w \\<in> Well(A, B);
- !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y)
+ "[| w \<in> Well(A, B);
+ !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y)
|] ==> P(Sup(a,f))
|] ==> P(w)"
-- {* A nicer induction rule than the standard one. *}
proof -
case rule_context
- assume "w \\<in> Well(A, B)"
+ assume "w \<in> Well(A, B)"
thus ?thesis
apply induct
apply (assumption | rule rule_context)+
@@ -75,7 +75,7 @@
done
qed
-lemma Well_bool_unfold: "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))"
+lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
-- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
-- {* for @{text Well} to prove this. *}
apply (rule Well_unfold [THEN trans])
--- a/src/ZF/Induct/Comb.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Comb.thy Sat Dec 29 18:36:12 2001 +0100
@@ -2,269 +2,279 @@
ID: $Id$
Author: Lawrence C Paulson
Copyright 1994 University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
- J. Camilleri and T. F. Melham.
- Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
- Report 265, University of Cambridge Computer Laboratory, 1992.
-
-HOL system proofs may be found in
-/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
*)
+header {* Combinatory Logic example: the Church-Rosser Theorem *}
theory Comb = Main:
-(** Datatype definition of combinators S and K, with infixed application **)
-consts comb :: i
-datatype
- "comb" = K
- | S
- | "#" ("p \<in> comb", "q \<in> comb") (infixl 90)
+text {*
+ Curiously, combinators do not include free variables.
+
+ Example taken from \cite{camilleri-melham}.
+*}
+
+subsection {* Definitions *}
+
+text {* Datatype definition of combinators @{text S} and @{text K}. *}
-(** Inductive definition of contractions, -1->
- and (multi-step) reductions, --->
-**)
+consts comb :: i
+datatype comb =
+ K
+ | S
+ | app ("p \<in> comb", "q \<in> comb") (infixl "#" 90)
+
+text {*
+ Inductive definition of contractions, @{text "-1->"} and
+ (multi-step) reductions, @{text "--->"}.
+*}
+
consts
- contract :: "i"
- "-1->" :: "[i,i] => o" (infixl 50)
- "--->" :: "[i,i] => o" (infixl 50)
-
+ contract :: i
+syntax
+ "_contract" :: "[i,i] => o" (infixl "-1->" 50)
+ "_contract_multi" :: "[i,i] => o" (infixl "--->" 50)
translations
"p -1-> q" == "<p,q> \<in> contract"
"p ---> q" == "<p,q> \<in> contract^*"
inductive
- domains "contract" <= "comb*comb"
+ domains "contract" \<subseteq> "comb \<times> comb"
intros
- K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q -1-> p"
- S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
- Ap1: "[| p-1->q; r \<in> comb |] ==> p#r -1-> q#r"
- Ap2: "[| p-1->q; r \<in> comb |] ==> r#p -1-> r#q"
- type_intros "comb.intros"
-
+ K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q -1-> p"
+ S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+ Ap1: "[| p-1->q; r \<in> comb |] ==> p#r -1-> q#r"
+ Ap2: "[| p-1->q; r \<in> comb |] ==> r#p -1-> r#q"
+ type_intros comb.intros
-(** Inductive definition of parallel contractions, =1=>
- and (multi-step) parallel reductions, ===>
-**)
+text {*
+ Inductive definition of parallel contractions, @{text "=1=>"} and
+ (multi-step) parallel reductions, @{text "===>"}.
+*}
+
consts
- parcontract :: "i"
- "=1=>" :: "[i,i] => o" (infixl 50)
- "===>" :: "[i,i] => o" (infixl 50)
-
+ parcontract :: i
+syntax
+ "_parcontract" :: "[i,i] => o" (infixl "=1=>" 50)
+ "_parcontract_multi" :: "[i,i] => o" (infixl "===>" 50)
translations
"p =1=> q" == "<p,q> \<in> parcontract"
"p ===> q" == "<p,q> \<in> parcontract^+"
inductive
- domains "parcontract" <= "comb*comb"
+ domains "parcontract" \<subseteq> "comb \<times> comb"
intros
- refl: "[| p \<in> comb |] ==> p =1=> p"
- K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q =1=> p"
- S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
- Ap: "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"
- type_intros "comb.intros"
+ refl: "[| p \<in> comb |] ==> p =1=> p"
+ K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q =1=> p"
+ S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+ Ap: "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"
+ type_intros comb.intros
+text {*
+ Misc definitions.
+*}
-(*Misc definitions*)
constdefs
I :: i
"I == S#K#K"
diamond :: "i => o"
- "diamond(r) == \<forall>x y. <x,y>\<in>r -->
- (\<forall>y'. <x,y'>\<in>r -->
- (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
+ "diamond(r) ==
+ \<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
-
-(*** Transitive closure preserves the Church-Rosser property ***)
+subsection {* Transitive closure preserves the Church-Rosser property *}
lemma diamond_strip_lemmaD [rule_format]:
- "[| diamond(r); <x,y>:r^+ |] ==>
- \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
-apply (unfold diamond_def)
-apply (erule trancl_induct)
-apply (blast intro: r_into_trancl)
-apply clarify
-apply (drule spec [THEN mp], assumption)
-apply (blast intro: r_into_trancl trans_trancl [THEN transD])
-done
-
+ "[| diamond(r); <x,y>:r^+ |] ==>
+ \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
+ apply (unfold diamond_def)
+ apply (erule trancl_induct)
+ apply (blast intro: r_into_trancl)
+ apply clarify
+ apply (drule spec [THEN mp], assumption)
+ apply (blast intro: r_into_trancl trans_trancl [THEN transD])
+ done
lemma diamond_trancl: "diamond(r) ==> diamond(r^+)"
-apply (simp (no_asm_simp) add: diamond_def)
-apply (rule impI [THEN allI, THEN allI])
-apply (erule trancl_induct)
-apply (auto );
-apply (best intro: r_into_trancl trans_trancl [THEN transD]
- dest: diamond_strip_lemmaD)+
-done
-
+ apply (simp (no_asm_simp) add: diamond_def)
+ apply (rule impI [THEN allI, THEN allI])
+ apply (erule trancl_induct)
+ apply auto
+ apply (best intro: r_into_trancl trans_trancl [THEN transD]
+ dest: diamond_strip_lemmaD)+
+ done
inductive_cases Ap_E [elim!]: "p#q \<in> comb"
declare comb.intros [intro!]
-(*** Results about Contraction ***)
+subsection {* Results about Contraction *}
-(*For type checking: replaces a-1->b by a,b \<in> comb *)
+text {*
+ For type checking: replaces @{term "a -1-> b"} by @{text "a, b \<in>
+ comb"}.
+*}
+
lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
-lemmas contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
-lemmas contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]
+ and contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
+ and contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]
lemma field_contract_eq: "field(contract) = comb"
-by (blast intro: contract.K elim!: contract_combE2)
+ by (blast intro: contract.K elim!: contract_combE2)
-lemmas reduction_refl =
- field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]
+lemmas reduction_refl =
+ field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]
-lemmas rtrancl_into_rtrancl2 =
- r_into_rtrancl [THEN trans_rtrancl [THEN transD]]
+lemmas rtrancl_into_rtrancl2 =
+ r_into_rtrancl [THEN trans_rtrancl [THEN transD]]
declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!]
-lemmas reduction_rls = contract.K [THEN rtrancl_into_rtrancl2]
- contract.S [THEN rtrancl_into_rtrancl2]
- contract.Ap1 [THEN rtrancl_into_rtrancl2]
- contract.Ap2 [THEN rtrancl_into_rtrancl2]
+lemmas reduction_rls =
+ contract.K [THEN rtrancl_into_rtrancl2]
+ contract.S [THEN rtrancl_into_rtrancl2]
+ contract.Ap1 [THEN rtrancl_into_rtrancl2]
+ contract.Ap2 [THEN rtrancl_into_rtrancl2]
-(*Example only: not used*)
-lemma reduce_I: "p \<in> comb ==> I#p ---> p"
-by (unfold I_def, blast intro: reduction_rls)
+lemma "p \<in> comb ==> I#p ---> p"
+ -- {* Example only: not used *}
+ by (unfold I_def) (blast intro: reduction_rls)
lemma comb_I: "I \<in> comb"
-by (unfold I_def, blast)
+ by (unfold I_def) blast
-(** Non-contraction results **)
+
+subsection {* Non-contraction results *}
-(*Derive a case for each combinator constructor*)
-inductive_cases K_contractE [elim!]: "K -1-> r"
-inductive_cases S_contractE [elim!]: "S -1-> r"
-inductive_cases Ap_contractE [elim!]: "p#q -1-> r"
+text {* Derive a case for each combinator constructor. *}
+
+inductive_cases
+ K_contractE [elim!]: "K -1-> r"
+ and S_contractE [elim!]: "S -1-> r"
+ and Ap_contractE [elim!]: "p#q -1-> r"
declare contract.Ap1 [intro] contract.Ap2 [intro]
lemma I_contract_E: "I -1-> r ==> P"
-by (auto simp add: I_def)
+ by (auto simp add: I_def)
lemma K1_contractD: "K#p -1-> r ==> (\<exists>q. r = K#q & p -1-> q)"
-by auto
+ by auto
lemma Ap_reduce1: "[| p ---> q; r \<in> comb |] ==> p#r ---> q#r"
-apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
-apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
-apply (erule rtrancl_induct)
-apply (blast intro: reduction_rls)
-apply (erule trans_rtrancl [THEN transD])
-apply (blast intro: contract_combD2 reduction_rls)
-done
+ apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+ apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+ apply (erule rtrancl_induct)
+ apply (blast intro: reduction_rls)
+ apply (erule trans_rtrancl [THEN transD])
+ apply (blast intro: contract_combD2 reduction_rls)
+ done
lemma Ap_reduce2: "[| p ---> q; r \<in> comb |] ==> r#p ---> r#q"
-apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
-apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
-apply (erule rtrancl_induct)
-apply (blast intro: reduction_rls)
-apply (erule trans_rtrancl [THEN transD])
-apply (blast intro: contract_combD2 reduction_rls)
-done
+ apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+ apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+ apply (erule rtrancl_induct)
+ apply (blast intro: reduction_rls)
+ apply (erule trans_rtrancl [THEN transD])
+ apply (blast intro: contract_combD2 reduction_rls)
+ done
-(** Counterexample to the diamond property for -1-> **)
+text {* Counterexample to the diamond property for @{text "-1->"}. *}
lemma KIII_contract1: "K#I#(I#I) -1-> I"
-by (blast intro: comb.intros contract.K comb_I)
+ by (blast intro: comb.intros contract.K comb_I)
lemma KIII_contract2: "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"
-by (unfold I_def, blast intro: comb.intros contract.intros)
-
+ by (unfold I_def) (blast intro: comb.intros contract.intros)
lemma KIII_contract3: "K#I#((K#I)#(K#I)) -1-> I"
-by (blast intro: comb.intros contract.K comb_I)
+ by (blast intro: comb.intros contract.K comb_I)
-lemma not_diamond_contract: "~ diamond(contract)"
-apply (unfold diamond_def)
-apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
- elim!: I_contract_E)
-done
-
+lemma not_diamond_contract: "\<not> diamond(contract)"
+ apply (unfold diamond_def)
+ apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
+ elim!: I_contract_E)
+ done
-(*** Results about Parallel Contraction ***)
+subsection {* Results about Parallel Contraction *}
-(*For type checking: replaces a=1=>b by a,b \<in> comb *)
+text {* For type checking: replaces @{text "a =1=> b"} by @{text "a, b
+ \<in> comb"} *}
lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
-lemmas parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
-lemmas parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
+ and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
+ and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
lemma field_parcontract_eq: "field(parcontract) = comb"
-by (blast intro: parcontract.K elim!: parcontract_combE2)
+ by (blast intro: parcontract.K elim!: parcontract_combE2)
-(*Derive a case for each combinator constructor*)
-inductive_cases K_parcontractE [elim!]: "K =1=> r"
-inductive_cases S_parcontractE [elim!]: "S =1=> r"
-inductive_cases Ap_parcontractE [elim!]: "p#q =1=> r"
+text {* Derive a case for each combinator constructor. *}
+inductive_cases
+ K_parcontractE [elim!]: "K =1=> r"
+ and S_parcontractE [elim!]: "S =1=> r"
+ and Ap_parcontractE [elim!]: "p#q =1=> r"
declare parcontract.intros [intro]
-(*** Basic properties of parallel contraction ***)
+subsection {* Basic properties of parallel contraction *}
-lemma K1_parcontractD [dest!]: "K#p =1=> r ==> (\<exists>p'. r = K#p' & p =1=> p')"
-by auto
+lemma K1_parcontractD [dest!]:
+ "K#p =1=> r ==> (\<exists>p'. r = K#p' & p =1=> p')"
+ by auto
-lemma S1_parcontractD [dest!]: "S#p =1=> r ==> (\<exists>p'. r = S#p' & p =1=> p')"
-by auto
+lemma S1_parcontractD [dest!]:
+ "S#p =1=> r ==> (\<exists>p'. r = S#p' & p =1=> p')"
+ by auto
lemma S2_parcontractD [dest!]:
- "S#p#q =1=> r ==> (\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"
-by auto
+ "S#p#q =1=> r ==> (\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"
+ by auto
-
-(*Church-Rosser property for parallel contraction*)
lemma diamond_parcontract: "diamond(parcontract)"
-apply (unfold diamond_def)
-apply (rule impI [THEN allI, THEN allI])
-apply (erule parcontract.induct)
-apply (blast elim!: comb.free_elims intro: parcontract_combD2)+
-done
+ -- {* Church-Rosser property for parallel contraction *}
+ apply (unfold diamond_def)
+ apply (rule impI [THEN allI, THEN allI])
+ apply (erule parcontract.induct)
+ apply (blast elim!: comb.free_elims intro: parcontract_combD2)+
+ done
-(*** Equivalence of p--->q and p===>q ***)
+text {*
+ \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
+*}
lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
-by (erule contract.induct, auto)
+ by (erule contract.induct) auto
lemma reduce_imp_parreduce: "p--->q ==> p===>q"
-apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
-apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
-apply (erule rtrancl_induct)
- apply (blast intro: r_into_trancl)
-apply (blast intro: contract_imp_parcontract r_into_trancl
- trans_trancl [THEN transD])
-done
-
+ apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+ apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+ apply (erule rtrancl_induct)
+ apply (blast intro: r_into_trancl)
+ apply (blast intro: contract_imp_parcontract r_into_trancl
+ trans_trancl [THEN transD])
+ done
lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
-apply (erule parcontract.induct)
+ apply (erule parcontract.induct)
+ apply (blast intro: reduction_rls)
+ apply (blast intro: reduction_rls)
apply (blast intro: reduction_rls)
- apply (blast intro: reduction_rls)
- apply (blast intro: reduction_rls)
-apply (blast intro: trans_rtrancl [THEN transD]
- Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
-done
+ apply (blast intro: trans_rtrancl [THEN transD]
+ Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
+ done
lemma parreduce_imp_reduce: "p===>q ==> p--->q"
-apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
-apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
-apply (erule trancl_induct, erule parcontract_imp_reduce)
-apply (erule trans_rtrancl [THEN transD])
-apply (erule parcontract_imp_reduce)
-done
+ apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
+ apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
+ apply (erule trancl_induct, erule parcontract_imp_reduce)
+ apply (erule trans_rtrancl [THEN transD])
+ apply (erule parcontract_imp_reduce)
+ done
lemma parreduce_iff_reduce: "p===>q <-> p--->q"
-by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
+ by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
end
--- a/src/ZF/Induct/Datatypes.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Datatypes.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Datatypes.thy
+(* Title: ZF/Induct/Datatypes.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
--- a/src/ZF/Induct/FoldSet.ML Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/FoldSet.ML Sat Dec 29 18:36:12 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/UNITY/FoldSet.thy
+(* Title: ZF/Induct/FoldSet.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
--- a/src/ZF/Induct/FoldSet.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/FoldSet.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/UNITY/FoldSet.thy
+(* Title: ZF/Induct/FoldSet.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
--- a/src/ZF/Induct/ListN.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/ListN.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,58 +1,62 @@
-(* Title: ZF/Induct/ListN
+(* Title: ZF/Induct/ListN.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-
-Inductive definition of lists of n elements
+*)
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon. Dec 1992.
-*)
+header {* Lists of n elements *}
theory ListN = Main:
-consts listn :: "i=>i"
+text {*
+ Inductive definition of lists of @{text n} elements; see
+ \cite{paulin-tlca}.
+*}
+
+consts listn :: "i=>i"
inductive
- domains "listn(A)" <= "nat*list(A)"
+ domains "listn(A)" \<subseteq> "nat \<times> list(A)"
intros
- NilI: "<0,Nil> \<in> listn(A)"
+ NilI: "<0,Nil> \<in> listn(A)"
ConsI: "[| a \<in> A; <n,l> \<in> listn(A) |] ==> <succ(n), Cons(a,l)> \<in> listn(A)"
- type_intros nat_typechecks list.intros
+ type_intros nat_typechecks list.intros
lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
-by (erule list.induct, simp_all add: listn.intros)
+ by (erule list.induct) (simp_all add: listn.intros)
lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
-apply (rule iffI)
-apply (erule listn.induct)
-apply auto
-apply (blast intro: list_into_listn)
-done
+ apply (rule iffI)
+ apply (erule listn.induct)
+ apply auto
+ apply (blast intro: list_into_listn)
+ done
lemma listn_image_eq: "listn(A)``{n} = {l \<in> list(A). length(l)=n}"
-apply (rule equality_iffI)
-apply (simp (no_asm) add: listn_iff separation image_singleton_iff)
-done
+ apply (rule equality_iffI)
+ apply (simp add: listn_iff separation image_singleton_iff)
+ done
lemma listn_mono: "A \<subseteq> B ==> listn(A) \<subseteq> listn(B)"
-apply (unfold listn.defs )
-apply (rule lfp_mono)
-apply (rule listn.bnd_mono)+
-apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
-done
+ apply (unfold listn.defs)
+ apply (rule lfp_mono)
+ apply (rule listn.bnd_mono)+
+ apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
+ done
lemma listn_append:
- "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)"
-apply (erule listn.induct)
-apply (frule listn.dom_subset [THEN subsetD])
-apply (simp_all add: listn.intros)
-done
+ "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)"
+ apply (erule listn.induct)
+ apply (frule listn.dom_subset [THEN subsetD])
+ apply (simp_all add: listn.intros)
+ done
-inductive_cases Nil_listn_case: "<i,Nil> \<in> listn(A)"
-inductive_cases Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)"
+inductive_cases
+ Nil_listn_case: "<i,Nil> \<in> listn(A)"
+ and Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)"
-inductive_cases zero_listn_case: "<0,l> \<in> listn(A)"
-inductive_cases succ_listn_case: "<succ(i),l> \<in> listn(A)"
+inductive_cases
+ zero_listn_case: "<0,l> \<in> listn(A)"
+ and succ_listn_case: "<succ(i),l> \<in> listn(A)"
end
--- a/src/ZF/Induct/Multiset.ML Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Multiset.ML Sat Dec 29 18:36:12 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/UNITY/Multiset.thy
+(* Title: ZF/Induct/Multiset.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
--- a/src/ZF/Induct/Multiset.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Multiset.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/UNITY/Multiset.thy
+(* Title: ZF/Induct/Multiset.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
--- a/src/ZF/Induct/Ntree.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Ntree.thy Sat Dec 29 18:36:12 2001 +0100
@@ -34,11 +34,11 @@
constdefs
ntree_rec :: "[[i, i, i] => i, i] => i"
"ntree_rec(b) ==
- Vrecursor(%pr. ntree_case(%x h. b(x, h, \<lambda>i \<in> domain(h). pr`(h`i))))"
+ Vrecursor(\<lambda>pr. ntree_case(\<lambda>x h. b(x, h, \<lambda>i \<in> domain(h). pr`(h`i))))"
constdefs
ntree_copy :: "i => i"
- "ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)"
+ "ntree_copy(z) == ntree_rec(\<lambda>x h r. Branch(x,r), z)"
text {*
--- a/src/ZF/Induct/Primrec.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Primrec.thy Sat Dec 29 18:36:12 2001 +0100
@@ -2,369 +2,372 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-
-Primitive Recursive Functions: the inductive definition
+*)
-Proof adopted from
-Nora Szasz,
-A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
-In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
-
-See also E. Mendelson, Introduction to Mathematical Logic.
-(Van Nostrand, 1964), page 250, exercise 11.
-*)
+header {* Primitive Recursive Functions: the inductive definition *}
theory Primrec = Main:
+text {*
+ Proof adopted from \cite{szasz}.
+
+ See also \cite[page 250, exercise 11]{mendelson}.
+*}
+
+
+subsection {* Basic definitions *}
+
constdefs
- SC :: "i"
- "SC == \<lambda>l \<in> list(nat). list_case(0, %x xs. succ(x), l)"
-
- CONST :: "i=>i"
- "CONST(k) == \<lambda>l \<in> list(nat). k"
+ SC :: "i"
+ "SC == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. succ(x), l)"
- PROJ :: "i=>i"
- "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
+ CONST :: "i=>i"
+ "CONST(k) == \<lambda>l \<in> list(nat). k"
- COMP :: "[i,i]=>i"
- "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List.map(%f. f`l, fs)"
+ PROJ :: "i=>i"
+ "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. x, drop(i,l))"
- PREC :: "[i,i]=>i"
- (*Note that g is applied first to PREC(f,g)`y and then to y!*)
- "PREC(f,g) ==
- \<lambda>l \<in> list(nat). list_case(0,
- %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+ COMP :: "[i,i]=>i"
+ "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List.map(\<lambda>f. f`l, fs)"
+
+ PREC :: "[i,i]=>i"
+ "PREC(f,g) ==
+ \<lambda>l \<in> list(nat). list_case(0,
+ \<lambda>x xs. rec(x, f`xs, \<lambda>y r. g ` Cons(r, Cons(y, xs))), l)"
+ -- {* Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}! *}
consts
- ACK :: "i=>i"
-
+ ACK :: "i=>i"
primrec
- ACK_0: "ACK(0) = SC"
- ACK_succ: "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
- COMP(ACK(i), [PROJ(0)]))"
+ "ACK(0) = SC"
+ "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
syntax
- ack :: "[i,i]=>i"
-
+ ack :: "[i,i]=>i"
translations
- "ack(x,y)" == "ACK(x) ` [y]"
-
+ "ack(x,y)" == "ACK(x) ` [y]"
-(** Useful special cases of evaluation ***)
+text {*
+ \medskip Useful special cases of evaluation.
+*}
lemma SC: "[| x \<in> nat; l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
-by (simp add: SC_def)
+ by (simp add: SC_def)
lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"
-by (simp add: CONST_def)
+ by (simp add: CONST_def)
lemma PROJ_0: "[| x \<in> nat; l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
-by (simp add: PROJ_def)
+ by (simp add: PROJ_def)
lemma COMP_1: "l \<in> list(nat) ==> COMP(g,[f]) ` l = g` [f`l]"
-by (simp add: COMP_def)
+ by (simp add: COMP_def)
lemma PREC_0: "l \<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"
-by (simp add: PREC_def)
+ by (simp add: PREC_def)
-lemma PREC_succ:
- "[| x \<in> nat; l \<in> list(nat) |]
- ==> PREC(f,g) ` (Cons(succ(x),l)) =
- g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"
-by (simp add: PREC_def)
+lemma PREC_succ:
+ "[| x \<in> nat; l \<in> list(nat) |]
+ ==> PREC(f,g) ` (Cons(succ(x),l)) =
+ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"
+ by (simp add: PREC_def)
+subsection {* Inductive definition of the PR functions *}
+
consts
- prim_rec :: "i"
+ prim_rec :: i
inductive
- domains "prim_rec" <= "list(nat)->nat"
+ domains prim_rec \<subseteq> "list(nat)->nat"
intros
"SC \<in> prim_rec"
"k \<in> nat ==> CONST(k) \<in> prim_rec"
"i \<in> nat ==> PROJ(i) \<in> prim_rec"
- "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs): prim_rec"
- "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g): prim_rec"
- monos list_mono
- con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
- type_intros nat_typechecks list.intros
- lam_type list_case_type drop_type List.map_type
- apply_type rec_type
+ "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs) \<in> prim_rec"
+ "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g) \<in> prim_rec"
+ monos list_mono
+ con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
+ type_intros nat_typechecks list.intros
+ lam_type list_case_type drop_type List.map_type
+ apply_type rec_type
-(*** Inductive definition of the PR functions ***)
+lemma prim_rec_into_fun [TC]: "c \<in> prim_rec ==> c \<in> list(nat) -> nat"
+ by (erule subsetD [OF prim_rec.dom_subset])
-(* c \<in> prim_rec ==> c \<in> list(nat) -> nat *)
-lemmas prim_rec_into_fun [TC] = subsetD [OF prim_rec.dom_subset]
lemmas [TC] = apply_type [OF prim_rec_into_fun]
declare prim_rec.intros [TC]
declare nat_into_Ord [TC]
declare rec_type [TC]
-lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i): prim_rec"
-by (induct_tac "i", simp_all)
-
-lemma ack_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j): nat"
-by auto
+lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i) \<in> prim_rec"
+ by (induct_tac i) simp_all
-(** Ackermann's function cases **)
+lemma ack_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) \<in> nat"
+ by auto
-(*PROPERTY A 1*)
-lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
-by (simp add: SC)
+
+subsection {* Ackermann's function cases *}
-(*PROPERTY A 2*)
+lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
+ -- {* PROPERTY A 1 *}
+ by (simp add: SC)
+
lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
-by (simp add: CONST PREC_0)
+ -- {* PROPERTY A 2 *}
+ by (simp add: CONST PREC_0)
-(*PROPERTY A 3*)
lemma ack_succ_succ:
- "[| i\<in>nat; j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
-by (simp add: CONST PREC_succ COMP_1 PROJ_0)
+ "[| i\<in>nat; j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
+ -- {* PROPERTY A 3 *}
+ by (simp add: CONST PREC_succ COMP_1 PROJ_0)
-declare ack_0 [simp] ack_succ_0 [simp] ack_succ_succ [simp] ack_type [simp]
-declare ACK_0 [simp del] ACK_succ [simp del]
+lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
+ and [simp del] = ACK.simps
-(*PROPERTY A 4*)
lemma lt_ack2 [rule_format]: "i \<in> nat ==> \<forall>j \<in> nat. j < ack(i,j)"
-apply (induct_tac "i")
-apply simp
-apply (rule ballI)
-apply (induct_tac "j")
-apply (erule_tac [2] succ_leI [THEN lt_trans1])
-apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
-apply auto
-done
+ -- {* PROPERTY A 4 *}
+ apply (induct_tac i)
+ apply simp
+ apply (rule ballI)
+ apply (induct_tac j)
+ apply (erule_tac [2] succ_leI [THEN lt_trans1])
+ apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
+ apply auto
+ done
-(*PROPERTY A 5-, the single-step lemma*)
lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
-by (induct_tac "i", simp_all add: lt_ack2)
+ -- {* PROPERTY A 5-, the single-step lemma *}
+ by (induct_tac i) (simp_all add: lt_ack2)
-(*PROPERTY A 5, monotonicity for < *)
lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
-apply (frule lt_nat_in_nat , assumption)
-apply (erule succ_lt_induct)
-apply assumption
-apply (rule_tac [2] lt_trans)
-apply (auto intro: ack_lt_ack_succ2)
-done
+ -- {* PROPERTY A 5, monotonicity for @{text "<"} *}
+ apply (frule lt_nat_in_nat, assumption)
+ apply (erule succ_lt_induct)
+ apply assumption
+ apply (rule_tac [2] lt_trans)
+ apply (auto intro: ack_lt_ack_succ2)
+ done
-(*PROPERTY A 5', monotonicity for\<le>*)
lemma ack_le_mono2: "[|j\<le>k; i\<in>nat; k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"
-apply (rule_tac f = "%j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
-apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+;
-done
+ -- {* PROPERTY A 5', monotonicity for @{text \<le>} *}
+ apply (rule_tac f = "\<lambda>j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
+ apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+
+ done
-(*PROPERTY A 6*)
lemma ack2_le_ack1:
- "[| i\<in>nat; j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
-apply (induct_tac "j")
-apply (simp_all)
-apply (rule ack_le_mono2)
-apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])
-apply auto
-done
+ "[| i\<in>nat; j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
+ -- {* PROPERTY A 6 *}
+ apply (induct_tac j)
+ apply simp_all
+ apply (rule ack_le_mono2)
+ apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])
+ apply auto
+ done
-(*PROPERTY A 7-, the single-step lemma*)
lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"
-apply (rule ack_lt_mono2 [THEN lt_trans2])
-apply (rule_tac [4] ack2_le_ack1)
-apply auto
-done
+ -- {* PROPERTY A 7-, the single-step lemma *}
+ apply (rule ack_lt_mono2 [THEN lt_trans2])
+ apply (rule_tac [4] ack2_le_ack1)
+ apply auto
+ done
-(*PROPERTY A 7, monotonicity for < *)
lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"
-apply (frule lt_nat_in_nat , assumption)
-apply (erule succ_lt_induct)
-apply assumption
-apply (rule_tac [2] lt_trans)
-apply (auto intro: ack_lt_ack_succ1)
-done
+ -- {* PROPERTY A 7, monotonicity for @{text "<"} *}
+ apply (frule lt_nat_in_nat, assumption)
+ apply (erule succ_lt_induct)
+ apply assumption
+ apply (rule_tac [2] lt_trans)
+ apply (auto intro: ack_lt_ack_succ1)
+ done
-(*PROPERTY A 7', monotonicity for\<le>*)
lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"
-apply (rule_tac f = "%j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
-apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+;
-done
+ -- {* PROPERTY A 7', monotonicity for @{text \<le>} *}
+ apply (rule_tac f = "\<lambda>j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
+ apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+
+ done
-(*PROPERTY A 8*)
lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
-by (induct_tac "j", simp_all)
+ -- {* PROPERTY A 8 *}
+ by (induct_tac j) simp_all
-(*PROPERTY A 9*)
lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
-by (induct_tac "j", simp_all add: ack_1)
+ -- {* PROPERTY A 9 *}
+ by (induct_tac j) (simp_all add: ack_1)
-(*PROPERTY A 10*)
lemma ack_nest_bound:
- "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
- ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
-apply (rule lt_trans2 [OF _ ack2_le_ack1])
-apply simp
-apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
-apply auto
-apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])
-done
+ "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
+ ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
+ -- {* PROPERTY A 10 *}
+ apply (rule lt_trans2 [OF _ ack2_le_ack1])
+ apply simp
+ apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
+ apply auto
+ apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])
+ done
-(*PROPERTY A 11*)
lemma ack_add_bound:
- "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
- ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
-apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans)
-apply (simp add: ack_2)
-apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
-apply (rule add_le_mono [THEN leI, THEN leI])
-apply (auto intro: add_le_self add_le_self2 ack_le_mono1)
-done
+ "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
+ ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
+ -- {* PROPERTY A 11 *}
+ apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans)
+ apply (simp add: ack_2)
+ apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
+ apply (rule add_le_mono [THEN leI, THEN leI])
+ apply (auto intro: add_le_self add_le_self2 ack_le_mono1)
+ done
-(*PROPERTY A 12. Article uses existential quantifier but the ALF proof
- used k#+4. Quantified version must be nested \<exists>k'. \<forall>i,j... *)
lemma ack_add_bound2:
- "[| i < ack(k,j); j \<in> nat; k \<in> nat |]
+ "[| i < ack(k,j); j \<in> nat; k \<in> nat |]
==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
-apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
-apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
-apply (rule add_lt_mono)
-apply auto
-done
+ -- {* PROPERTY A 12. *}
+ -- {* Article uses existential quantifier but the ALF proof used @{term "k#+#4"}. *}
+ -- {* Quantified version must be nested @{text "\<exists>k'. \<forall>i,j \<dots>"}. *}
+ apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
+ apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
+ apply (rule add_lt_mono)
+ apply auto
+ done
-(*** MAIN RESULT ***)
+
+subsection {* Main result *}
declare list_add_type [simp]
lemma SC_case: "l \<in> list(nat) ==> SC ` l < ack(1, list_add(l))"
-apply (unfold SC_def)
-apply (erule list.cases)
-apply (simp add: succ_iff)
-apply (simp add: ack_1 add_le_self)
-done
+ apply (unfold SC_def)
+ apply (erule list.cases)
+ apply (simp add: succ_iff)
+ apply (simp add: ack_1 add_le_self)
+ done
-(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
-apply (induct_tac "i")
-apply (simp add: nat_0_le)
-apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
-apply auto
-done
+ -- {* PROPERTY A 4'? Extra lemma needed for @{text CONST} case, constant functions. *}
+ apply (induct_tac i)
+ apply (simp add: nat_0_le)
+ apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
+ apply auto
+ done
-lemma CONST_case:
+lemma CONST_case:
"[| l \<in> list(nat); k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
-by (simp add: CONST_def lt_ack1)
+ by (simp add: CONST_def lt_ack1)
-lemma PROJ_case [rule_format]:
+lemma PROJ_case [rule_format]:
"l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
-apply (unfold PROJ_def)
-apply simp
-apply (erule list.induct)
-apply (simp add: nat_0_le)
-apply simp
-apply (rule ballI)
-apply (erule_tac n = "x" in natE)
-apply (simp add: add_le_self)
-apply simp
-apply (erule bspec [THEN lt_trans2])
-apply (rule_tac [2] add_le_self2 [THEN succ_leI])
-apply auto
-done
+ apply (unfold PROJ_def)
+ apply simp
+ apply (erule list.induct)
+ apply (simp add: nat_0_le)
+ apply simp
+ apply (rule ballI)
+ apply (erule_tac n = "x" in natE)
+ apply (simp add: add_le_self)
+ apply simp
+ apply (erule bspec [THEN lt_trans2])
+ apply (rule_tac [2] add_le_self2 [THEN succ_leI])
+ apply auto
+ done
-(** COMP case **)
+text {*
+ \medskip @{text COMP} case.
+*}
lemma COMP_map_lemma:
- "fs \<in> list({f \<in> prim_rec .
- \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))})
- ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat).
- list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))"
-apply (erule list.induct)
-apply (rule_tac x = "0" in bexI)
-apply (simp_all add: lt_ack1 nat_0_le)
-apply clarify
-apply (rule ballI [THEN bexI])
-apply (rule add_lt_mono [THEN lt_trans])
-apply (rule_tac [5] ack_add_bound)
-apply blast
-apply auto
-done
+ "fs \<in> list({f \<in> prim_rec. \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))})
+ ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat).
+ list_add(map(\<lambda>f. f ` l, fs)) < ack(k, list_add(l))"
+ apply (erule list.induct)
+ apply (rule_tac x = 0 in bexI)
+ apply (simp_all add: lt_ack1 nat_0_le)
+ apply clarify
+ apply (rule ballI [THEN bexI])
+ apply (rule add_lt_mono [THEN lt_trans])
+ apply (rule_tac [5] ack_add_bound)
+ apply blast
+ apply auto
+ done
-lemma COMP_case:
- "[| kg\<in>nat;
- \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l));
- fs \<in> list({f \<in> prim_rec .
- \<exists>kf \<in> nat. \<forall>l \<in> list(nat).
+lemma COMP_case:
+ "[| kg\<in>nat;
+ \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l));
+ fs \<in> list({f \<in> prim_rec .
+ \<exists>kf \<in> nat. \<forall>l \<in> list(nat).
f`l < ack(kf, list_add(l))}) |]
==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))"
-apply (simp add: COMP_def)
-apply (frule list_CollectD)
-apply (erule COMP_map_lemma [THEN bexE])
-apply (rule ballI [THEN bexI])
-apply (erule bspec [THEN lt_trans])
-apply (rule_tac [2] lt_trans)
-apply (rule_tac [3] ack_nest_bound)
-apply (erule_tac [2] bspec [THEN ack_lt_mono2])
-apply auto
-done
+ apply (simp add: COMP_def)
+ apply (frule list_CollectD)
+ apply (erule COMP_map_lemma [THEN bexE])
+ apply (rule ballI [THEN bexI])
+ apply (erule bspec [THEN lt_trans])
+ apply (rule_tac [2] lt_trans)
+ apply (rule_tac [3] ack_nest_bound)
+ apply (erule_tac [2] bspec [THEN ack_lt_mono2])
+ apply auto
+ done
-(** PREC case **)
+text {*
+ \medskip @{text PREC} case.
+*}
-lemma PREC_case_lemma:
- "[| \<forall>l \<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));
- \<forall>l \<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));
- f \<in> prim_rec; kf\<in>nat;
- g \<in> prim_rec; kg\<in>nat;
+lemma PREC_case_lemma:
+ "[| \<forall>l \<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));
+ \<forall>l \<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));
+ f \<in> prim_rec; kf\<in>nat;
+ g \<in> prim_rec; kg\<in>nat;
l \<in> list(nat) |]
==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
-apply (unfold PREC_def)
-apply (erule list.cases)
-apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
-apply simp
-apply (erule ssubst) (*get rid of the needless assumption*)
-apply (induct_tac "a")
-apply simp_all
-(*base case*)
-apply (rule lt_trans, erule bspec, assumption);
-apply (simp add: add_le_self [THEN ack_lt_mono1])
-(*ind step*)
-apply (rule succ_leI [THEN lt_trans1])
-apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
-apply (erule_tac [2] bspec)
-apply (rule nat_le_refl [THEN add_le_mono])
-apply typecheck
-apply (simp add: add_le_self2)
-(*final part of the simplification*)
-apply simp
-apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])
-apply (erule_tac [4] ack_lt_mono2)
-apply auto
-done
+ apply (unfold PREC_def)
+ apply (erule list.cases)
+ apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
+ apply simp
+ apply (erule ssubst) -- {* get rid of the needless assumption *}
+ apply (induct_tac a)
+ apply simp_all
+ txt {* base case *}
+ apply (rule lt_trans, erule bspec, assumption)
+ apply (simp add: add_le_self [THEN ack_lt_mono1])
+ txt {* ind step *}
+ apply (rule succ_leI [THEN lt_trans1])
+ apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
+ apply (erule_tac [2] bspec)
+ apply (rule nat_le_refl [THEN add_le_mono])
+ apply typecheck
+ apply (simp add: add_le_self2)
+ txt {* final part of the simplification *}
+ apply simp
+ apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])
+ apply (erule_tac [4] ack_lt_mono2)
+ apply auto
+ done
lemma PREC_case:
- "[| f \<in> prim_rec; kf\<in>nat;
- g \<in> prim_rec; kg\<in>nat;
- \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l));
- \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)) |]
- ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))"
-apply (rule ballI [THEN bexI])
-apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])
-apply typecheck
-apply (blast intro: ack_add_bound2 list_add_type)+
-done
+ "[| f \<in> prim_rec; kf\<in>nat;
+ g \<in> prim_rec; kg\<in>nat;
+ \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l));
+ \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)) |]
+ ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))"
+ apply (rule ballI [THEN bexI])
+ apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])
+ apply typecheck
+ apply (blast intro: ack_add_bound2 list_add_type)+
+ done
lemma ack_bounds_prim_rec:
- "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
-apply (erule prim_rec.induct)
-apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
-done
+ "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
+ apply (erule prim_rec.induct)
+ apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
+ done
-lemma ack_not_prim_rec:
- "~ (\<lambda>l \<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \<in> prim_rec"
-apply (rule notI)
-apply (drule ack_bounds_prim_rec)
-apply force
-done
+theorem ack_not_prim_rec:
+ "(\<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. ack(x,x), l)) \<notin> prim_rec"
+ apply (rule notI)
+ apply (drule ack_bounds_prim_rec)
+ apply force
+ done
end
-
-
-
--- a/src/ZF/Induct/PropLog.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/PropLog.thy Sat Dec 29 18:36:12 2001 +0100
@@ -2,296 +2,339 @@
ID: $Id$
Author: Tobias Nipkow & Lawrence C Paulson
Copyright 1993 University of Cambridge
-
-Datatype definition of propositional logic formulae and inductive definition
-of the propositional tautologies.
+*)
-Inductive definition of propositional logic.
-Soundness and completeness w.r.t. truth-tables.
-
-Prove: If H|=p then G|=p where G \<in> Fin(H)
-*)
+header {* Meta-theory of propositional logic *}
theory PropLog = Main:
-(** The datatype of propositions; note mixfix syntax **)
-consts
- propn :: "i"
+text {*
+ Datatype definition of propositional logic formulae and inductive
+ definition of the propositional tautologies.
+
+ Inductive definition of propositional logic. Soundness and
+ completeness w.r.t.\ truth-tables.
-datatype
- "propn" = Fls
- | Var ("n \<in> nat") ("#_" [100] 100)
- | "=>" ("p \<in> propn", "q \<in> propn") (infixr 90)
+ Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
+ Fin(H)"}
+*}
+
+
+subsection {* The datatype of propositions *}
-(** The proof system **)
consts
- thms :: "i => i"
+ propn :: i
-syntax
- "|-" :: "[i,i] => o" (infixl 50)
+datatype propn =
+ Fls
+ | Var ("n \<in> nat") ("#_" [100] 100)
+ | Imp ("p \<in> propn", "q \<in> propn") (infixr "=>" 90)
+
-translations
- "H |- p" == "p \<in> thms(H)"
+subsection {* The proof system *}
+
+consts thms :: "i => i"
+syntax "_thms" :: "[i,i] => o" (infixl "|-" 50)
+translations "H |- p" == "p \<in> thms(H)"
inductive
- domains "thms(H)" <= "propn"
+ domains "thms(H)" \<subseteq> "propn"
intros
H: "[| p \<in> H; p \<in> propn |] ==> H |- p"
K: "[| p \<in> propn; q \<in> propn |] ==> H |- p=>q=>p"
- S: "[| p \<in> propn; q \<in> propn; r \<in> propn |]
+ S: "[| p \<in> propn; q \<in> propn; r \<in> propn |]
==> H |- (p=>q=>r) => (p=>q) => p=>r"
DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
MP: "[| H |- p=>q; H |- p; p \<in> propn; q \<in> propn |] ==> H |- q"
type_intros "propn.intros"
-
-(** The semantics **)
-consts
- "|=" :: "[i,i] => o" (infixl 50)
- hyps :: "[i,i] => i"
- is_true_fun :: "[i,i] => i"
-
-constdefs (*this definitionis necessary since predicates can't be recursive*)
- is_true :: "[i,i] => o"
- "is_true(p,t) == is_true_fun(p,t)=1"
-
-defs
- (*Logical consequence: for every valuation, if all elements of H are true
- then so is p*)
- logcon_def: "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) --> is_true(p,t)"
-
-primrec (** A finite set of hypotheses from t and the Vars in p **)
- "hyps(Fls, t) = 0"
- "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})"
- "hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)"
-
-primrec (** Semantics of propositional logic **)
- "is_true_fun(Fls, t) = 0"
- "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
- "is_true_fun(p=>q, t) = (if is_true_fun(p,t)=1 then is_true_fun(q,t)
- else 1)"
-
declare propn.intros [simp]
-(*** Semantics of propositional logic ***)
+
+subsection {* The semantics *}
+
+subsubsection {* Semantics of propositional logic. *}
-(** The function is_true **)
+consts
+ is_true_fun :: "[i,i] => i"
+primrec
+ "is_true_fun(Fls, t) = 0"
+ "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
+ "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"
+
+constdefs
+ is_true :: "[i,i] => o"
+ "is_true(p,t) == is_true_fun(p,t) = 1"
+ -- {* this definition is required since predicates can't be recursive *}
lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
-by (simp add: is_true_def)
+ by (simp add: is_true_def)
lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
-by (simp add: is_true_def)
+ by (simp add: is_true_def)
lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
-by (simp add: is_true_def)
+ by (simp add: is_true_def)
+
+
+subsubsection {* Logical consequence *}
+
+text {*
+ For every valuation, if all elements of @{text H} are true then so
+ is @{text p}.
+*}
+
+constdefs
+ logcon :: "[i,i] => o" (infixl "|=" 50)
+ "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) --> is_true(p,t)"
-(*** Proof theory of propositional logic ***)
+text {*
+ A finite set of hypotheses from @{text t} and the @{text Var}s in
+ @{text p}.
+*}
+
+consts
+ hyps :: "[i,i] => i"
+primrec
+ "hyps(Fls, t) = 0"
+ "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})"
+ "hyps(p=>q, t) = hyps(p,t) \<union> hyps(q,t)"
+
+
+
+subsection {* Proof theory of propositional logic *}
lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
-apply (unfold thms.defs )
-apply (rule lfp_mono)
-apply (rule thms.bnd_mono)+
-apply (assumption | rule univ_mono basic_monos)+
-done
+ apply (unfold thms.defs)
+ apply (rule lfp_mono)
+ apply (rule thms.bnd_mono)+
+ apply (assumption | rule univ_mono basic_monos)+
+ done
lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
inductive_cases ImpE: "p=>q \<in> propn"
-(*Stronger Modus Ponens rule: no typechecking!*)
lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q"
-apply (rule thms.MP)
-apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
-done
+ -- {* Stronger Modus Ponens rule: no typechecking! *}
+ apply (rule thms.MP)
+ apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
+ done
-(*Rule is called I for Identity Combinator, not for Introduction*)
lemma thms_I: "p \<in> propn ==> H |- p=>p"
-apply (rule thms.S [THEN thms_MP, THEN thms_MP])
-apply (rule_tac [5] thms.K)
-apply (rule_tac [4] thms.K)
-apply (simp_all add: propn.intros )
-done
+ -- {*Rule is called @{text I} for Identity Combinator, not for Introduction. *}
+ apply (rule thms.S [THEN thms_MP, THEN thms_MP])
+ apply (rule_tac [5] thms.K)
+ apply (rule_tac [4] thms.K)
+ apply simp_all
+ done
+
-(** Weakening, left and right **)
+subsubsection {* Weakening, left and right *}
-(* [| G \<subseteq> H; G|-p |] ==> H|-p Order of premises is convenient with RS*)
-lemmas weaken_left = thms_mono [THEN subsetD, standard]
+lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p"
+ -- {* Order of premises is convenient with @{text THEN} *}
+ by (erule thms_mono [THEN subsetD])
-(* H |- p ==> cons(a,H) |- p *)
-lemmas weaken_left_cons = subset_consI [THEN weaken_left]
+lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
+ by (erule subset_consI [THEN weaken_left])
lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left]
lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left]
lemma weaken_right: "[| H |- q; p \<in> propn |] ==> H |- p=>q"
-by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
+ by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
-(*The deduction theorem*)
-lemma deduction: "[| cons(p,H) |- q; p \<in> propn |] ==> H |- p=>q"
-apply (erule thms.induct)
- apply (blast intro: thms_I thms.H [THEN weaken_right])
- apply (blast intro: thms.K [THEN weaken_right])
- apply (blast intro: thms.S [THEN weaken_right])
- apply (blast intro: thms.DN [THEN weaken_right])
-apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
-done
+subsubsection {* The deduction theorem *}
+
+theorem deduction: "[| cons(p,H) |- q; p \<in> propn |] ==> H |- p=>q"
+ apply (erule thms.induct)
+ apply (blast intro: thms_I thms.H [THEN weaken_right])
+ apply (blast intro: thms.K [THEN weaken_right])
+ apply (blast intro: thms.S [THEN weaken_right])
+ apply (blast intro: thms.DN [THEN weaken_right])
+ apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
+ done
-(*The cut rule*)
+subsubsection {* The cut rule *}
+
lemma cut: "[| H|-p; cons(p,H) |- q |] ==> H |- q"
-apply (rule deduction [THEN thms_MP])
-apply (simp_all add: thms_in_pl)
-done
+ apply (rule deduction [THEN thms_MP])
+ apply (simp_all add: thms_in_pl)
+ done
lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
-apply (rule thms.DN [THEN thms_MP])
-apply (rule_tac [2] weaken_right)
-apply (simp_all add: propn.intros)
-done
+ apply (rule thms.DN [THEN thms_MP])
+ apply (rule_tac [2] weaken_right)
+ apply (simp_all add: propn.intros)
+ done
-(* [| H |- p=>Fls; H |- p; q \<in> propn |] ==> H |- q *)
-lemmas thms_notE = thms_MP [THEN thms_FlsE, standard]
+lemma thms_notE: "[| H |- p=>Fls; H |- p; q \<in> propn |] ==> H |- q"
+ by (erule thms_MP [THEN thms_FlsE])
+
+
+subsubsection {* Soundness of the rules wrt truth-table semantics *}
-(*Soundness of the rules wrt truth-table semantics*)
-lemma soundness: "H |- p ==> H |= p"
-apply (unfold logcon_def)
-apply (erule thms.induct)
-apply auto
-done
+theorem soundness: "H |- p ==> H |= p"
+ apply (unfold logcon_def)
+ apply (erule thms.induct)
+ apply auto
+ done
-(*** Towards the completeness proof ***)
+
+subsection {* Completeness *}
+
+subsubsection {* Towards the completeness proof *}
lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
-apply (frule thms_in_pl)
-apply (rule deduction)
-apply (rule weaken_left_cons [THEN thms_notE])
-apply (blast intro: thms.H elim: ImpE)+
-done
+ apply (frule thms_in_pl)
+ apply (rule deduction)
+ apply (rule weaken_left_cons [THEN thms_notE])
+ apply (blast intro: thms.H elim: ImpE)+
+ done
lemma Imp_Fls: "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
-apply (frule thms_in_pl)
-apply (frule thms_in_pl [of concl: "q=>Fls"])
-apply (rule deduction)
-apply (erule weaken_left_cons [THEN thms_MP])
-apply (rule consI1 [THEN thms.H, THEN thms_MP])
-apply (blast intro: weaken_left_cons elim: ImpE)+
-done
+ apply (frule thms_in_pl)
+ apply (frule thms_in_pl [of concl: "q=>Fls"])
+ apply (rule deduction)
+ apply (erule weaken_left_cons [THEN thms_MP])
+ apply (rule consI1 [THEN thms.H, THEN thms_MP])
+ apply (blast intro: weaken_left_cons elim: ImpE)+
+ done
-(*Typical example of strengthening the induction formula*)
lemma hyps_thms_if:
- "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
-apply (simp (no_asm))
-apply (induct_tac "p")
-apply (simp_all (no_asm_simp) add: thms_I thms.H)
-apply (safe elim!: Fls_Imp [THEN weaken_left_Un1]
- Fls_Imp [THEN weaken_left_Un2])
-apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
-done
+ "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
+ -- {* Typical example of strengthening the induction statement. *}
+ apply simp
+ apply (induct_tac p)
+ apply (simp_all add: thms_I thms.H)
+ apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
+ apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
+ done
+
+lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p"
+ -- {* Key lemma for completeness; yields a set of assumptions satisfying @{text p} *}
+ apply (drule hyps_thms_if)
+ apply (simp add: logcon_def)
+ done
+
+text {*
+ For proving certain theorems in our new propositional logic.
+*}
-(*Key lemma for completeness; yields a set of assumptions satisfying p*)
-lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p"
-apply (unfold logcon_def)
-apply (drule hyps_thms_if)
-apply simp
-done
+lemmas propn_SIs = propn.intros deduction
+ and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
+
+text {*
+ The excluded middle in the form of an elimination rule.
+*}
+lemma thms_excluded_middle:
+ "[| p \<in> propn; q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
+ apply (rule deduction [THEN deduction])
+ apply (rule thms.DN [THEN thms_MP])
+ apply (best intro!: propn_SIs intro: propn_Is)+
+ done
-(*For proving certain theorems in our new propositional logic*)
-lemmas propn_SIs = propn.intros deduction
-lemmas propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
+lemma thms_excluded_middle_rule:
+ "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q"
+ -- {* Hard to prove directly because it requires cuts *}
+ apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
+ apply (blast intro!: propn_SIs intro: propn_Is)+
+ done
-(*The excluded middle in the form of an elimination rule*)
-lemma thms_excluded_middle:
- "[| p \<in> propn; q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
-apply (rule deduction [THEN deduction])
-apply (rule thms.DN [THEN thms_MP])
-apply (best intro!: propn_SIs intro: propn_Is)+
-done
+subsubsection {* Completeness -- lemmas for reducing the set of assumptions *}
-(*Hard to prove directly because it requires cuts*)
-lemma thms_excluded_middle_rule:
- "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q"
-apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
-apply (blast intro!: propn_SIs intro: propn_Is)+
-done
+text {*
+ For the case @{prop "hyps(p,t)-cons(#v,Y) |- p"} we also have @{prop
+ "hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})"}.
+*}
+lemma hyps_Diff:
+ "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
+ by (induct_tac p) auto
-(*** Completeness -- lemmas for reducing the set of assumptions ***)
-
-(*For the case hyps(p,t)-cons(#v,Y) |- p
- we also have hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v}) *)
-lemma hyps_Diff:
- "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
-by (induct_tac "p", auto)
+text {*
+ For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have
+ @{prop "hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t))"}.
+*}
-(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p
- we also have hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t)) *)
lemma hyps_cons:
- "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
-by (induct_tac "p", auto)
+ "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
+ by (induct_tac p) auto
-(** Two lemmas for use with weaken_left **)
+text {* Two lemmas for use with @{text weaken_left} *}
lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
-by blast
+ by blast
lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
-by blast
+ by blast
-(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls
- could probably prove the stronger hyps(p,t) \<in> Fin(hyps(p,0) Un hyps(p,nat))*)
+text {*
+ The set @{term "hyps(p,t)"} is finite, and elements have the form
+ @{term "#v"} or @{term "#v=>Fls"}; could probably prove the stronger
+ @{prop "hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))"}.
+*}
+
lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
-by (induct_tac "p", auto)
+ by (induct_tac p) auto
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
-(*Induction on the finite set of assumptions hyps(p,t0).
- We may repeatedly subtract assumptions until none are left!*)
+text {*
+ Induction on the finite set of assumptions @{term "hyps(p,t0)"}. We
+ may repeatedly subtract assumptions until none are left!
+*}
+
lemma completeness_0_lemma [rule_format]:
"[| p \<in> propn; 0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
-apply (frule hyps_finite)
-apply (erule Fin_induct)
-apply (simp add: logcon_thms_p Diff_0)
-(*inductive step*)
-apply safe
-(*Case hyps(p,t)-cons(#v,Y) |- p *)
- apply (rule thms_excluded_middle_rule)
- apply (erule_tac [3] propn.intros)
+ apply (frule hyps_finite)
+ apply (erule Fin_induct)
+ apply (simp add: logcon_thms_p Diff_0)
+ txt {* inductive step *}
+ apply safe
+ txt {* Case @{prop "hyps(p,t)-cons(#v,Y) |- p"} *}
+ apply (rule thms_excluded_middle_rule)
+ apply (erule_tac [3] propn.intros)
+ apply (blast intro: cons_Diff_same [THEN weaken_left])
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
+ hyps_Diff [THEN Diff_weaken_left])
+ txt {* Case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} *}
+ apply (rule thms_excluded_middle_rule)
+ apply (erule_tac [3] propn.intros)
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
+ hyps_cons [THEN Diff_weaken_left])
apply (blast intro: cons_Diff_same [THEN weaken_left])
- apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
- hyps_Diff [THEN Diff_weaken_left])
-(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
-apply (rule thms_excluded_middle_rule)
- apply (erule_tac [3] propn.intros)
- apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
- hyps_cons [THEN Diff_weaken_left])
-apply (blast intro: cons_Diff_same [THEN weaken_left])
-done
+ done
+
+
+subsubsection {* Completeness theorem *}
-(*The base case for completeness*)
lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p"
-apply (rule Diff_cancel [THEN subst])
-apply (blast intro: completeness_0_lemma)
-done
+ -- {* The base case for completeness *}
+ apply (rule Diff_cancel [THEN subst])
+ apply (blast intro: completeness_0_lemma)
+ done
-(*A semantic analogue of the Deduction Theorem*)
lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
-by (simp add: logcon_def)
+ -- {* A semantic analogue of the Deduction Theorem *}
+ by (simp add: logcon_def)
lemma completeness [rule_format]:
"H \<in> Fin(propn) ==> \<forall>p \<in> propn. H |= p --> H |- p"
-apply (erule Fin_induct)
-apply (safe intro!: completeness_0)
-apply (rule weaken_left_cons [THEN thms_MP])
- apply (blast intro!: logcon_Imp propn.intros)
-apply (blast intro: propn_Is)
-done
+ apply (erule Fin_induct)
+ apply (safe intro!: completeness_0)
+ apply (rule weaken_left_cons [THEN thms_MP])
+ apply (blast intro!: logcon_Imp propn.intros)
+ apply (blast intro: propn_Is)
+ done
-lemma thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p & p \<in> propn"
-by (blast intro: soundness completeness thms_in_pl)
+theorem thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p \<and> p \<in> propn"
+ by (blast intro: soundness completeness thms_in_pl)
end
--- a/src/ZF/Induct/Rmap.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Rmap.thy Sat Dec 29 18:36:12 2001 +0100
@@ -1,10 +1,10 @@
-(* Title: ZF/ex/Rmap
+(* Title: ZF/Induct/Rmap.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
+*)
-Inductive definition of an operator to "map" a relation over a list
-*)
+header {* An operator to ``map'' a relation over a list *}
theory Rmap = Main:
@@ -12,60 +12,60 @@
rmap :: "i=>i"
inductive
- domains "rmap(r)" <= "list(domain(r))*list(range(r))"
+ domains "rmap(r)" \<subseteq> "list(domain(r)) \<times> list(range(r))"
intros
NilI: "<Nil,Nil> \<in> rmap(r)"
- ConsI: "[| <x,y>: r; <xs,ys> \<in> rmap(r) |]
+ ConsI: "[| <x,y>: r; <xs,ys> \<in> rmap(r) |]
==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
type_intros domainI rangeI list.intros
lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
-apply (unfold rmap.defs )
-apply (rule lfp_mono)
-apply (rule rmap.bnd_mono)+
-apply (assumption |
- rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
-done
+ apply (unfold rmap.defs)
+ apply (rule lfp_mono)
+ apply (rule rmap.bnd_mono)+
+ apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
+ done
-inductive_cases Nil_rmap_case [elim!]: "<Nil,zs> \<in> rmap(r)"
-inductive_cases Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)"
+inductive_cases
+ Nil_rmap_case [elim!]: "<Nil,zs> \<in> rmap(r)"
+ and Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)"
declare rmap.intros [intro]
-lemma rmap_rel_type: "r \<subseteq> A*B ==> rmap(r) \<subseteq> list(A)*list(B)"
-apply (rule rmap.dom_subset [THEN subset_trans])
-apply (assumption |
- rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
-done
+lemma rmap_rel_type: "r \<subseteq> A \<times> B ==> rmap(r) \<subseteq> list(A) \<times> list(B)"
+ apply (rule rmap.dom_subset [THEN subset_trans])
+ apply (assumption |
+ rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
+ done
lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
-apply (rule subsetI)
-apply (erule list.induct)
-apply blast+
-done
+ apply (rule subsetI)
+ apply (erule list.induct)
+ apply blast+
+ done
lemma rmap_functional: "function(r) ==> function(rmap(r))"
-apply (unfold function_def)
-apply (rule impI [THEN allI, THEN allI])
-apply (erule rmap.induct)
-apply blast+
-done
+ apply (unfold function_def)
+ apply (rule impI [THEN allI, THEN allI])
+ apply (erule rmap.induct)
+ apply blast+
+ done
-
-(** If f is a function then rmap(f) behaves as expected. **)
+text {*
+ \medskip If @{text f} is a function then @{text "rmap(f)"} behaves
+ as expected.
+*}
lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
-by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
+ by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
lemma rmap_Nil: "rmap(f)`Nil = Nil"
-by (unfold apply_def, blast)
+ by (unfold apply_def) blast
-lemma rmap_Cons: "[| f \<in> A->B; x \<in> A; xs: list(A) |]
+lemma rmap_Cons: "[| f \<in> A->B; x \<in> A; xs: list(A) |]
==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
-by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
-
+ by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
end
-
--- a/src/ZF/Induct/Term.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Term.thy Sat Dec 29 18:36:12 2001 +0100
@@ -167,7 +167,8 @@
*}
lemma term_map [simp]:
- "ts \<in> list(A) ==> term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
+ "ts \<in> list(A) ==>
+ term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
by (rule term_map_def [THEN def_term_rec])
lemma term_map_type [TC]:
@@ -289,7 +290,8 @@
\medskip Theorems about preorder.
*}
-lemma preorder_term_map: "t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
+lemma preorder_term_map:
+ "t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
apply (erule term_induct_eqn)
apply (simp add: map_flat)
done
--- a/src/ZF/Induct/Tree_Forest.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Sat Dec 29 18:36:12 2001 +0100
@@ -54,7 +54,8 @@
done
lemma (notes rews = tree_forest.con_defs tree_def forest_def)
- tree_forest_unfold: "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
+ tree_forest_unfold: "tree_forest(A) =
+ (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
-- {* NOT useful, but interesting \dots *}
apply (unfold tree_def forest_def)
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
@@ -206,7 +207,8 @@
!!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f))
|] ==> R(f)"
-- {* Essentially the same as list induction. *}
- apply (erule tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp])
+ apply (erule tree_forest.mutual_induct
+ [THEN conjunct2, THEN spec, THEN [2] rev_mp])
apply (rule TrueI)
apply simp
apply simp
--- a/src/ZF/Induct/document/root.tex Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Induct/document/root.tex Sat Dec 29 18:36:12 2001 +0100
@@ -2,11 +2,8 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage[latin1]{inputenc}
-
-% this should be the last package used
\usepackage{pdfsetup}
-% proper setup for best-style documents
\urlstyle{rm}
\isabellestyle{it}
@@ -22,4 +19,7 @@
\parindent 0pt\parskip 0.5ex
\input{session}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}
--- a/src/ZF/IsaMakefile Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/IsaMakefile Sat Dec 29 18:36:12 2001 +0100
@@ -84,8 +84,8 @@
ZF-IMP: ZF $(LOG)/ZF-IMP.gz
-$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy \
- IMP/Denotation.thy IMP/Equiv.thy IMP/ROOT.ML
+$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy \
+ IMP/ROOT.ML IMP/document/root.bib IMP/document/root.tex
@$(ISATOOL) usedir $(OUT)/ZF IMP
--- a/src/ZF/Resid/Redex.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Resid/Redex.thy Sat Dec 29 18:36:12 2001 +0100
@@ -125,16 +125,17 @@
declare Scomp.intros [intro]
-inductive_cases [elim!]: "regular(App(b,f,a))"
-inductive_cases [elim!]: "regular(Fun(b))"
-inductive_cases [elim!]: "regular(Var(b))"
-inductive_cases [elim!]: "Fun(u) ~ Fun(t)"
-inductive_cases [elim!]: "u ~ Fun(t)"
-inductive_cases [elim!]: "u ~ Var(n)"
-inductive_cases [elim!]: "u ~ App(b,t,a)"
-inductive_cases [elim!]: "Fun(t) ~ v"
-inductive_cases [elim!]: "App(b,f,a) ~ v"
-inductive_cases [elim!]: "Var(n) ~ u"
+inductive_cases [elim!]:
+ "regular(App(b,f,a))"
+ "regular(Fun(b))"
+ "regular(Var(b))"
+ "Fun(u) ~ Fun(t)"
+ "u ~ Fun(t)"
+ "u ~ Var(n)"
+ "u ~ App(b,t,a)"
+ "Fun(t) ~ v"
+ "App(b,f,a) ~ v"
+ "Var(n) ~ u"
--- a/src/ZF/Resid/Residuals.thy Sat Dec 29 18:35:27 2001 +0100
+++ b/src/ZF/Resid/Residuals.thy Sat Dec 29 18:36:12 2001 +0100
@@ -42,25 +42,28 @@
declare Sreg.intros [intro]
declare subst_type [intro]
-inductive_cases [elim!]: "residuals(Var(n),Var(n),v)"
-inductive_cases [elim!]: "residuals(Fun(t),Fun(u),v)"
-inductive_cases [elim!]: "residuals(App(b, u1, u2), App(0, v1, v2),v)"
-inductive_cases [elim!]: "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
-inductive_cases [elim!]: "residuals(Var(n),u,v)"
-inductive_cases [elim!]: "residuals(Fun(t),u,v)"
-inductive_cases [elim!]: "residuals(App(b, u1, u2), w,v)"
-inductive_cases [elim!]: "residuals(u,Var(n),v)"
-inductive_cases [elim!]: "residuals(u,Fun(t),v)"
-inductive_cases [elim!]: "residuals(w,App(b, u1, u2),v)"
+inductive_cases [elim!]:
+ "residuals(Var(n),Var(n),v)"
+ "residuals(Fun(t),Fun(u),v)"
+ "residuals(App(b, u1, u2), App(0, v1, v2),v)"
+ "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
+ "residuals(Var(n),u,v)"
+ "residuals(Fun(t),u,v)"
+ "residuals(App(b, u1, u2), w,v)"
+ "residuals(u,Var(n),v)"
+ "residuals(u,Fun(t),v)"
+ "residuals(w,App(b, u1, u2),v)"
-inductive_cases [elim!]: "Var(n) <== u"
-inductive_cases [elim!]: "Fun(n) <== u"
-inductive_cases [elim!]: "u <== Fun(n)"
-inductive_cases [elim!]: "App(1,Fun(t),a) <== u"
-inductive_cases [elim!]: "App(0,t,a) <== u"
+inductive_cases [elim!]:
+ "Var(n) <== u"
+ "Fun(n) <== u"
+ "u <== Fun(n)"
+ "App(1,Fun(t),a) <== u"
+ "App(0,t,a) <== u"
-inductive_cases [elim!]: "Fun(t):redexes"
+inductive_cases [elim!]:
+ "Fun(t) \<in> redexes"
declare Sres.intros [simp]