--- a/src/LCF/IsaMakefile Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/IsaMakefile Thu Jun 01 21:14:05 2006 +0200
@@ -34,8 +34,7 @@
LCF-ex: LCF $(LOG)/LCF-ex.gz
-$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.ML ex/Ex1.thy ex/Ex2.ML ex/Ex2.thy \
- ex/Ex3.ML ex/Ex3.thy ex/Ex4.ML ex/Ex4.thy ex/ROOT.ML
+$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.thy ex/Ex2.thy ex/Ex3.thy ex/Ex4.thy ex/ROOT.ML
@$(ISATOOL) usedir $(OUT)/LCF ex
--- a/src/LCF/LCF_lemmas.ML Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/LCF_lemmas.ML Thu Jun 01 21:14:05 2006 +0200
@@ -12,76 +12,76 @@
fun strip_tac i = REPEAT(rstac [impI,allI] i);
-val eq_imp_less1 = prove_goal (the_context ()) "x=y ==> x << y"
- (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
+bind_thm ("eq_imp_less1", prove_goal (the_context ()) "x=y ==> x << y"
+ (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]));
-val eq_imp_less2 = prove_goal (the_context ()) "x=y ==> y << x"
- (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
+bind_thm ("eq_imp_less2", prove_goal (the_context ()) "x=y ==> y << x"
+ (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]));
-val less_refl = refl RS eq_imp_less1;
+bind_thm ("less_refl", refl RS eq_imp_less1);
-val less_anti_sym = prove_goal (the_context ()) "[| x << y; y << x |] ==> x=y"
+bind_thm ("less_anti_sym", prove_goal (the_context ()) "[| x << y; y << x |] ==> x=y"
(fn prems => [rewtac eq_def,
- REPEAT(rstac(conjI::prems)1)]);
+ REPEAT(rstac(conjI::prems)1)]));
-val ext = prove_goal (the_context ())
+bind_thm ("ext", prove_goal (the_context ())
"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
prem RS eq_imp_less1,
- prem RS eq_imp_less2]1)]);
+ prem RS eq_imp_less2]1)]));
-val cong = prove_goal (the_context ()) "[| f=g; x=y |] ==> f(x)=g(y)"
+bind_thm ("cong", prove_goal (the_context ()) "[| f=g; x=y |] ==> f(x)=g(y)"
(fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
- rtac refl 1]);
+ rtac refl 1]));
-val less_ap_term = less_refl RS mono;
-val less_ap_thm = less_refl RSN (2,mono);
-val ap_term = refl RS cong;
-val ap_thm = refl RSN (2,cong);
+bind_thm ("less_ap_term", less_refl RS mono);
+bind_thm ("less_ap_thm", less_refl RSN (2,mono));
+bind_thm ("ap_term", refl RS cong);
+bind_thm ("ap_thm", refl RSN (2,cong));
-val UU_abs = prove_goal (the_context ()) "(%x::'a::cpo. UU) = UU"
+bind_thm ("UU_abs", prove_goal (the_context ()) "(%x::'a::cpo. UU) = UU"
(fn _ => [rtac less_anti_sym 1, rtac minimal 2,
- rtac less_ext 1, rtac allI 1, rtac minimal 1]);
+ rtac less_ext 1, rtac allI 1, rtac minimal 1]));
-val UU_app = UU_abs RS sym RS ap_thm;
+bind_thm ("UU_app", UU_abs RS sym RS ap_thm);
-val less_UU = prove_goal (the_context ()) "x << UU ==> x=UU"
- (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
+bind_thm ("less_UU", prove_goal (the_context ()) "x << UU ==> x=UU"
+ (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]));
-val tr_induct = prove_goal (the_context ()) "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
+bind_thm ("tr_induct", prove_goal (the_context ()) "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
(fn prems => [rtac allI 1, rtac mp 1,
res_inst_tac[("p","b")]tr_cases 2,
- fast_tac (FOL_cs addIs prems) 1]);
+ fast_tac (FOL_cs addIs prems) 1]));
-val Contrapos = prove_goal (the_context ()) "(A ==> B) ==> (~B ==> ~A)"
+bind_thm ("Contrapos", prove_goal (the_context ()) "(A ==> B) ==> (~B ==> ~A)"
(fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
- rstac prems 1, atac 1]);
+ rstac prems 1, atac 1]));
-val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos;
-val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos;
+bind_thm ("not_less_imp_not_eq1", eq_imp_less1 COMP Contrapos);
+bind_thm ("not_less_imp_not_eq2", eq_imp_less2 COMP Contrapos);
-val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2;
-val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2;
-val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1;
-val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1;
-val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1;
-val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1;
+bind_thm ("not_UU_eq_TT", not_TT_less_UU RS not_less_imp_not_eq2);
+bind_thm ("not_UU_eq_FF", not_FF_less_UU RS not_less_imp_not_eq2);
+bind_thm ("not_TT_eq_UU", not_TT_less_UU RS not_less_imp_not_eq1);
+bind_thm ("not_TT_eq_FF", not_TT_less_FF RS not_less_imp_not_eq1);
+bind_thm ("not_FF_eq_UU", not_FF_less_UU RS not_less_imp_not_eq1);
+bind_thm ("not_FF_eq_TT", not_FF_less_TT RS not_less_imp_not_eq1);
-val COND_cases_iff = (prove_goal (the_context ())
+bind_thm ("COND_cases_iff", (prove_goal (the_context ())
"ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
(fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
- stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec;
+ stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec);
val lemma = prove_goal (the_context ()) "A<->B ==> B ==> A"
(fn prems => [cut_facts_tac prems 1, rewtac iff_def,
fast_tac FOL_cs 1]);
-val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));
+bind_thm ("COND_cases", conjI RSN (2,conjI RS (COND_cases_iff RS lemma)));
val LCF_ss = FOL_ss addsimps
--- a/src/LCF/ex/Ex1.ML Thu Jun 01 14:54:44 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-
-(* $Id$ *)
-
-Addsimps [P_strict,K];
-
-val H_unfold = prove_goal (the_context ()) "H = K(H)"
- (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
-
-bind_thm ("H_unfold", H_unfold);
-
-
-val H_strict = prove_goal (the_context ()) "H(UU)=UU"
- (fn _ => [stac H_unfold 1, Simp_tac 1]);
-
-bind_thm ("H_strict", H_strict);
-Addsimps [H_strict];
-
-Goal "ALL x. H(FIX(K,x)) = FIX(K,x)";
-by (induct_tac "K" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
-by (strip_tac 1);
-by (stac H_unfold 1);
-by (Asm_simp_tac 1);
-qed "H_idemp_lemma";
-
-val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
-bind_thm ("H_idemp", H_idemp);
--- a/src/LCF/ex/Ex1.thy Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex1.thy Thu Jun 01 21:14:05 2006 +0200
@@ -18,6 +18,30 @@
K: "K = (%h x. P(x) => x | h(h(G(x))))"
H: "H = FIX(K)"
-ML {* use_legacy_bindings (the_context ()) *}
+
+declare P_strict [simp] K [simp]
+
+lemma H_unfold: "H = K(H)"
+ apply (simplesubst H)
+ apply (rule FIX_eq [symmetric])
+ done
+
+lemma H_strict [simp]: "H(UU)=UU"
+ apply (simplesubst H_unfold)
+ apply simp
+ done
+
+lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
+ apply (tactic {* induct_tac "K" 1 *})
+ apply (simp (no_asm))
+ apply (simp (no_asm) split: COND_cases_iff)
+ apply (intro strip)
+ apply (subst H_unfold)
+ apply (simp (no_asm_simp))
+ done
+
+lemma H_idemp: "ALL x. H(H(x)) = H(x)"
+ apply (rule H_idemp_lemma [folded H])
+ done
end
--- a/src/LCF/ex/Ex2.ML Thu Jun 01 14:54:44 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-
-(* $Id$ *)
-
-Addsimps [F_strict,K];
-
-Goal "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
-by (stac H 1);
-by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
-qed "example";
--- a/src/LCF/ex/Ex2.thy Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex2.thy Thu Jun 01 21:14:05 2006 +0200
@@ -19,6 +19,13 @@
K: "K = (%h x y. P(x) => y | F(h(G(x),y)))"
H: "H = FIX(K)"
-ML {* use_legacy_bindings (the_context ()) *}
+declare F_strict [simp] K [simp]
+
+lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
+ apply (simplesubst H)
+ apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+ apply (simp (no_asm))
+ apply (simp (no_asm_simp) split: COND_cases_iff)
+ done
end
--- a/src/LCF/ex/Ex3.ML Thu Jun 01 14:54:44 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-(* $Id$ *)
-
-Addsimps [p_strict,p_s];
-
-Goal "p(FIX(s),y) = FIX(s)";
-by (induct_tac "s" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "example";
--- a/src/LCF/ex/Ex3.thy Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex3.thy Thu Jun 01 21:14:05 2006 +0200
@@ -15,6 +15,12 @@
p_strict: "p(UU) = UU"
p_s: "p(s(x),y) = s(p(x,y))"
-ML {* use_legacy_bindings (the_context ()) *}
+declare p_strict [simp] p_s [simp]
+
+lemma example: "p(FIX(s),y) = FIX(s)"
+ apply (tactic {* induct_tac "s" 1 *})
+ apply (simp (no_asm))
+ apply (simp (no_asm))
+ done
end
--- a/src/LCF/ex/Ex4.ML Thu Jun 01 14:54:44 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* $Id$ *)
-
-val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
-by (rewtac eq_def);
-by (rtac conjI 1);
-by (induct_tac "f" 1);
-by (rtac minimal 1);
-by (strip_tac 1);
-by (rtac less_trans 1);
-by (resolve_tac asms 2);
-by (etac less_ap_term 1);
-by (resolve_tac asms 1);
-by (rtac (FIX_eq RS eq_imp_less1) 1);
-qed "example";
--- a/src/LCF/ex/Ex4.thy Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex4.thy Thu Jun 01 21:14:05 2006 +0200
@@ -5,4 +5,20 @@
imports LCF
begin
+lemma example:
+ assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q"
+ shows "FIX(f)=p"
+ apply (unfold eq_def)
+ apply (rule conjI)
+ apply (tactic {* induct_tac "f" 1 *})
+ apply (rule minimal)
+ apply (intro strip)
+ apply (rule less_trans)
+ prefer 2
+ apply (rule asms)
+ apply (erule less_ap_term)
+ apply (rule asms)
+ apply (rule FIX_eq [THEN eq_imp_less1])
+ done
+
end