1.1 --- a/src/LCF/LCF.thy Mon Mar 19 21:25:15 2012 +0100
1.2 +++ b/src/LCF/LCF.thy Mon Mar 19 21:49:52 2012 +0100
1.3 @@ -44,77 +44,83 @@
1.4 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
1.5 less :: "['a,'a] => o" (infixl "<<" 50)
1.6
1.7 -axioms
1.8 +axiomatization where
1.9 (** DOMAIN THEORY **)
1.10
1.11 - eq_def: "x=y == x << y & y << x"
1.12 + eq_def: "x=y == x << y & y << x" and
1.13
1.14 - less_trans: "[| x << y; y << z |] ==> x << z"
1.15 + less_trans: "[| x << y; y << z |] ==> x << z" and
1.16
1.17 - less_ext: "(ALL x. f(x) << g(x)) ==> f << g"
1.18 + less_ext: "(ALL x. f(x) << g(x)) ==> f << g" and
1.19
1.20 - mono: "[| f << g; x << y |] ==> f(x) << g(y)"
1.21 + mono: "[| f << g; x << y |] ==> f(x) << g(y)" and
1.22
1.23 - minimal: "UU << x"
1.24 + minimal: "UU << x" and
1.25
1.26 - FIX_eq: "f(FIX(f)) = FIX(f)"
1.27 + FIX_eq: "\<And>f. f(FIX(f)) = FIX(f)"
1.28
1.29 +axiomatization where
1.30 (** TR **)
1.31
1.32 - tr_cases: "p=UU | p=TT | p=FF"
1.33 + tr_cases: "p=UU | p=TT | p=FF" and
1.34
1.35 - not_TT_less_FF: "~ TT << FF"
1.36 - not_FF_less_TT: "~ FF << TT"
1.37 - not_TT_less_UU: "~ TT << UU"
1.38 - not_FF_less_UU: "~ FF << UU"
1.39 + not_TT_less_FF: "~ TT << FF" and
1.40 + not_FF_less_TT: "~ FF << TT" and
1.41 + not_TT_less_UU: "~ TT << UU" and
1.42 + not_FF_less_UU: "~ FF << UU" and
1.43
1.44 - COND_UU: "UU => x | y = UU"
1.45 - COND_TT: "TT => x | y = x"
1.46 + COND_UU: "UU => x | y = UU" and
1.47 + COND_TT: "TT => x | y = x" and
1.48 COND_FF: "FF => x | y = y"
1.49
1.50 +axiomatization where
1.51 (** PAIRS **)
1.52
1.53 - surj_pairing: "<FST(z),SND(z)> = z"
1.54 + surj_pairing: "<FST(z),SND(z)> = z" and
1.55
1.56 - FST: "FST(<x,y>) = x"
1.57 + FST: "FST(<x,y>) = x" and
1.58 SND: "SND(<x,y>) = y"
1.59
1.60 +axiomatization where
1.61 (*** STRICT SUM ***)
1.62
1.63 - INL_DEF: "~x=UU ==> ~INL(x)=UU"
1.64 - INR_DEF: "~x=UU ==> ~INR(x)=UU"
1.65 + INL_DEF: "~x=UU ==> ~INL(x)=UU" and
1.66 + INR_DEF: "~x=UU ==> ~INR(x)=UU" and
1.67
1.68 - INL_STRICT: "INL(UU) = UU"
1.69 - INR_STRICT: "INR(UU) = UU"
1.70 + INL_STRICT: "INL(UU) = UU" and
1.71 + INR_STRICT: "INR(UU) = UU" and
1.72
1.73 - WHEN_UU: "WHEN(f,g,UU) = UU"
1.74 - WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)"
1.75 - WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)"
1.76 + WHEN_UU: "WHEN(f,g,UU) = UU" and
1.77 + WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" and
1.78 + WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" and
1.79
1.80 SUM_EXHAUSTION:
1.81 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))"
1.82
1.83 +axiomatization where
1.84 (** VOID **)
1.85
1.86 void_cases: "(x::void) = UU"
1.87
1.88 (** INDUCTION **)
1.89
1.90 +axiomatization where
1.91 induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
1.92
1.93 +axiomatization where
1.94 (** Admissibility / Chain Completeness **)
1.95 (* All rules can be found on pages 199--200 of Larry's LCF book.
1.96 Note that "easiness" of types is not taken into account
1.97 because it cannot be expressed schematically; flatness could be. *)
1.98
1.99 - adm_less: "adm(%x. t(x) << u(x))"
1.100 - adm_not_less: "adm(%x.~ t(x) << u)"
1.101 - adm_not_free: "adm(%x. A)"
1.102 - adm_subst: "adm(P) ==> adm(%x. P(t(x)))"
1.103 - adm_conj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
1.104 - adm_disj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
1.105 - adm_imp: "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
1.106 - adm_all: "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
1.107 + adm_less: "\<And>t u. adm(%x. t(x) << u(x))" and
1.108 + adm_not_less: "\<And>t u. adm(%x.~ t(x) << u)" and
1.109 + adm_not_free: "\<And>A. adm(%x. A)" and
1.110 + adm_subst: "\<And>P t. adm(P) ==> adm(%x. P(t(x)))" and
1.111 + adm_conj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" and
1.112 + adm_disj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" and
1.113 + adm_imp: "\<And>P Q. [| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" and
1.114 + adm_all: "\<And>P. (!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
1.115
1.116
1.117 lemma eq_imp_less1: "x = y ==> x << y"
2.1 --- a/src/LCF/ex/Ex1.thy Mon Mar 19 21:25:15 2012 +0100
2.2 +++ b/src/LCF/ex/Ex1.thy Mon Mar 19 21:49:52 2012 +0100
2.3 @@ -4,15 +4,14 @@
2.4 imports LCF
2.5 begin
2.6
2.7 -consts
2.8 - P :: "'a => tr"
2.9 - G :: "'a => 'a"
2.10 - H :: "'a => 'a"
2.11 +axiomatization
2.12 + P :: "'a => tr" and
2.13 + G :: "'a => 'a" and
2.14 + H :: "'a => 'a" and
2.15 K :: "('a => 'a) => ('a => 'a)"
2.16 -
2.17 -axioms
2.18 - P_strict: "P(UU) = UU"
2.19 - K: "K = (%h x. P(x) => x | h(h(G(x))))"
2.20 +where
2.21 + P_strict: "P(UU) = UU" and
2.22 + K: "K = (%h x. P(x) => x | h(h(G(x))))" and
2.23 H: "H = FIX(K)"
2.24
2.25
2.26 @@ -30,11 +29,11 @@
2.27
2.28 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
2.29 apply (tactic {* induct_tac @{context} "K" 1 *})
2.30 - apply (simp (no_asm))
2.31 - apply (simp (no_asm) split: COND_cases_iff)
2.32 + apply simp
2.33 + apply (simp split: COND_cases_iff)
2.34 apply (intro strip)
2.35 apply (subst H_unfold)
2.36 - apply (simp (no_asm_simp))
2.37 + apply simp
2.38 done
2.39
2.40 lemma H_idemp: "ALL x. H(H(x)) = H(x)"
3.1 --- a/src/LCF/ex/Ex2.thy Mon Mar 19 21:25:15 2012 +0100
3.2 +++ b/src/LCF/ex/Ex2.thy Mon Mar 19 21:49:52 2012 +0100
3.3 @@ -4,16 +4,15 @@
3.4 imports LCF
3.5 begin
3.6
3.7 -consts
3.8 - P :: "'a => tr"
3.9 - F :: "'a => 'a"
3.10 - G :: "'a => 'a"
3.11 - H :: "'a => 'b => 'b"
3.12 +axiomatization
3.13 + P :: "'a => tr" and
3.14 + F :: "'b => 'b" and
3.15 + G :: "'a => 'a" and
3.16 + H :: "'a => 'b => 'b" and
3.17 K :: "('a => 'b => 'b) => ('a => 'b => 'b)"
3.18 -
3.19 -axioms
3.20 - F_strict: "F(UU) = UU"
3.21 - K: "K = (%h x y. P(x) => y | F(h(G(x),y)))"
3.22 +where
3.23 + F_strict: "F(UU) = UU" and
3.24 + K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" and
3.25 H: "H = FIX(K)"
3.26
3.27 declare F_strict [simp] K [simp]
3.28 @@ -21,8 +20,8 @@
3.29 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
3.30 apply (simplesubst H)
3.31 apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
3.32 - apply (simp (no_asm))
3.33 - apply (simp (no_asm_simp) split: COND_cases_iff)
3.34 + apply simp
3.35 + apply (simp split: COND_cases_iff)
3.36 done
3.37
3.38 end
4.1 --- a/src/LCF/ex/Ex3.thy Mon Mar 19 21:25:15 2012 +0100
4.2 +++ b/src/LCF/ex/Ex3.thy Mon Mar 19 21:49:52 2012 +0100
4.3 @@ -4,20 +4,19 @@
4.4 imports LCF
4.5 begin
4.6
4.7 -consts
4.8 - s :: "'a => 'a"
4.9 +axiomatization
4.10 + s :: "'a => 'a" and
4.11 p :: "'a => 'a => 'a"
4.12 -
4.13 -axioms
4.14 - p_strict: "p(UU) = UU"
4.15 +where
4.16 + p_strict: "p(UU) = UU" and
4.17 p_s: "p(s(x),y) = s(p(x,y))"
4.18
4.19 declare p_strict [simp] p_s [simp]
4.20
4.21 lemma example: "p(FIX(s),y) = FIX(s)"
4.22 apply (tactic {* induct_tac @{context} "s" 1 *})
4.23 - apply (simp (no_asm))
4.24 - apply (simp (no_asm))
4.25 + apply simp
4.26 + apply simp
4.27 done
4.28
4.29 end