# HG changeset patch
# User wenzelm
# Date 1149189245 -7200
# Node ID 90f80de04c4609ffaa9623837211a7779df1d92a
# Parent  489e6be0b19d5be770aa60e1cd98fb22dc21acc5
removed obsolete ML files;

diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/IsaMakefile
--- 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
 
 
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/LCF_lemmas.ML
--- 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
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex1.ML
--- 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);
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex1.thy
--- 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
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex2.ML
--- 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";
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex2.thy
--- 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
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex3.ML
--- 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";
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex3.thy
--- 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
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex4.ML
--- 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";
diff -r 489e6be0b19d -r 90f80de04c46 src/LCF/ex/Ex4.thy
--- 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