--- a/src/HOLCF/Pcpo.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Pcpo.ML Wed Jun 28 10:54:21 2000 +0200
@@ -1,38 +1,32 @@
-(* Title: HOLCF/pcpo.ML
+(* Title: HOLCF/Pcpo.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for pcpo.thy
+introduction of the classes cpo and pcpo
*)
-open Pcpo;
-
(* ------------------------------------------------------------------------ *)
(* derive the old rule minimal *)
(* ------------------------------------------------------------------------ *)
+
+Goalw [UU_def] "ALL z. UU << z";
+by (rtac (select_eq_Ex RS iffD2) 1);
+by (rtac least 1);
+qed "UU_least";
-qed_goalw "UU_least" thy [ UU_def ] "!z. UU << z"
-(fn prems => [
- (rtac (select_eq_Ex RS iffD2) 1),
- (rtac least 1)]);
-
-bind_thm("minimal",UU_least RS spec);
+bind_thm("minimal", UU_least RS spec);
(* ------------------------------------------------------------------------ *)
(* in cpo's everthing equal to THE lub has lub properties for every chain *)
(* ------------------------------------------------------------------------ *)
-qed_goal "thelubE" thy
- "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (hyp_subst_tac 1),
- (rtac lubI 1),
- (etac cpo 1)
- ]);
+Goal "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l ";
+by (hyp_subst_tac 1);
+by (rtac lubI 1);
+by (etac cpo 1);
+qed "thelubE";
(* ------------------------------------------------------------------------ *)
(* Properties of the lub *)
@@ -45,230 +39,150 @@
bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
-qed_goal "maxinch_is_thelub" thy "chain Y ==> \
-\ max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))"
-(fn prems =>
- [
- cut_facts_tac prems 1,
- rtac iffI 1,
- fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1,
- rewtac max_in_chain_def,
- safe_tac (HOL_cs addSIs [antisym_less]),
- fast_tac (HOL_cs addSEs [chain_mono3]) 1,
- dtac sym 1,
- fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss simpset()) 1
- ]);
+Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))";
+by (rtac iffI 1);
+by (fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1);
+by (rewtac max_in_chain_def);
+by (safe_tac (HOL_cs addSIs [antisym_less]));
+by (fast_tac (HOL_cs addSEs [chain_mono3]) 1);
+by (dtac sym 1);
+by (force_tac (HOL_cs addSEs [is_ub_thelub], simpset()) 1);
+qed "maxinch_is_thelub";
(* ------------------------------------------------------------------------ *)
(* the << relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_mono" thy
- "[|chain(C1::(nat=>'a::cpo));chain(C2); ! k. C1(k) << C2(k)|]\
-\ ==> lub(range(C1)) << lub(range(C2))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac is_lub_thelub 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (rtac trans_less 1),
- (etac spec 1),
- (etac is_ub_thelub 1)
- ]);
+Goal "[|chain(C1::(nat=>'a::cpo));chain(C2); ALL k. C1(k) << C2(k)|]\
+\ ==> lub(range(C1)) << lub(range(C2))";
+by (etac is_lub_thelub 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (rtac trans_less 1);
+by (etac spec 1);
+by (etac is_ub_thelub 1);
+qed "lub_mono";
(* ------------------------------------------------------------------------ *)
(* the = relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_equal" thy
-"[| chain(C1::(nat=>'a::cpo));chain(C2);!k. C1(k)=C2(k)|]\
-\ ==> lub(range(C1))=lub(range(C2))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac antisym_less 1),
- (rtac lub_mono 1),
- (atac 1),
- (atac 1),
- (strip_tac 1),
- (rtac (antisym_less_inverse RS conjunct1) 1),
- (etac spec 1),
- (rtac lub_mono 1),
- (atac 1),
- (atac 1),
- (strip_tac 1),
- (rtac (antisym_less_inverse RS conjunct2) 1),
- (etac spec 1)
- ]);
+Goal "[| chain(C1::(nat=>'a::cpo));chain(C2);ALL k. C1(k)=C2(k)|]\
+\ ==> lub(range(C1))=lub(range(C2))";
+by (rtac antisym_less 1);
+by (rtac lub_mono 1);
+by (atac 1);
+by (atac 1);
+by (strip_tac 1);
+by (rtac (antisym_less_inverse RS conjunct1) 1);
+by (etac spec 1);
+by (rtac lub_mono 1);
+by (atac 1);
+by (atac 1);
+by (strip_tac 1);
+by (rtac (antisym_less_inverse RS conjunct2) 1);
+by (etac spec 1);
+qed "lub_equal";
(* ------------------------------------------------------------------------ *)
(* more results about mono and = of lubs of chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_mono2" thy
-"[|? j.!i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
-\ ==> lub(range(X))<<lub(range(Y))"
- (fn prems =>
- [
- (rtac exE 1),
- (resolve_tac prems 1),
- (rtac is_lub_thelub 1),
- (resolve_tac prems 1),
- (rtac ub_rangeI 1),
- (strip_tac 1),
- (case_tac "x<i" 1),
- (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
- (rtac sym 1),
- (Fast_tac 1),
- (rtac is_ub_thelub 1),
- (resolve_tac prems 1),
- (res_inst_tac [("y","X(Suc(x))")] trans_less 1),
- (rtac (chain_mono RS mp) 1),
- (resolve_tac prems 1),
- (rtac (not_less_eq RS subst) 1),
- (atac 1),
- (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1),
- (rtac sym 1),
- (Asm_simp_tac 1),
- (rtac is_ub_thelub 1),
- (resolve_tac prems 1)
- ]);
+Goal "[|EX j. ALL i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
+\ ==> lub(range(X))<<lub(range(Y))";
+by (etac exE 1);
+by (rtac is_lub_thelub 1);
+by (assume_tac 1);
+by (rtac ub_rangeI 1);
+by (strip_tac 1);
+by (case_tac "j<i" 1);
+by (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1);
+by (rtac sym 1);
+by (Fast_tac 1);
+by (rtac is_ub_thelub 1);
+by (assume_tac 1);
+by (res_inst_tac [("y","X(Suc(j))")] trans_less 1);
+by (rtac (chain_mono RS mp) 1);
+by (assume_tac 1);
+by (rtac (not_less_eq RS subst) 1);
+by (atac 1);
+by (res_inst_tac [("s","Y(Suc(j))"),("t","X(Suc(j))")] subst 1);
+by (Asm_simp_tac 1);
+by (etac is_ub_thelub 1);
+qed "lub_mono2";
-qed_goal "lub_equal2" thy
-"[|? j.!i. j<i --> X(i)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
-\ ==> lub(range(X))=lub(range(Y))"
- (fn prems =>
- [
- (rtac antisym_less 1),
- (rtac lub_mono2 1),
- (REPEAT (resolve_tac prems 1)),
- (cut_facts_tac prems 1),
- (rtac lub_mono2 1),
- Safe_tac,
- (Step_tac 1),
- Safe_tac,
- (rtac sym 1),
- (Fast_tac 1)
- ]);
+Goal "[|EX j. ALL i. j<i --> X(i)=Y(i); chain(X::nat=>'a::cpo); chain(Y)|]\
+\ ==> lub(range(X))=lub(range(Y))";
+by (blast_tac (claset() addIs [antisym_less, lub_mono2, sym]) 1);
+qed "lub_equal2";
-qed_goal "lub_mono3" thy "[|chain(Y::nat=>'a::cpo);chain(X);\
-\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lub_thelub 1),
- (atac 1),
- (rtac ub_rangeI 1),
- (strip_tac 1),
- (etac allE 1),
- (etac exE 1),
- (rtac trans_less 1),
- (rtac is_ub_thelub 2),
- (atac 2),
- (atac 1)
- ]);
+Goal "[|chain(Y::nat=>'a::cpo);chain(X);\
+\ALL i. EX j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))";
+by (rtac is_lub_thelub 1);
+by (atac 1);
+by (rtac ub_rangeI 1);
+by (strip_tac 1);
+by (etac allE 1);
+by (etac exE 1);
+by (rtac trans_less 1);
+by (rtac is_ub_thelub 2);
+by (atac 2);
+by (atac 1);
+qed "lub_mono3";
(* ------------------------------------------------------------------------ *)
(* usefull lemmas about UU *)
(* ------------------------------------------------------------------------ *)
-val eq_UU_sym = prove_goal thy "(UU = x) = (x = UU)" (fn _ => [
- Fast_tac 1]);
-
-qed_goal "eq_UU_iff" thy "(x=UU)=(x<<UU)"
- (fn prems =>
- [
- (rtac iffI 1),
- (hyp_subst_tac 1),
- (rtac refl_less 1),
- (rtac antisym_less 1),
- (atac 1),
- (rtac minimal 1)
- ]);
-
-qed_goal "UU_I" thy "x << UU ==> x = UU"
- (fn prems =>
- [
- (stac eq_UU_iff 1),
- (resolve_tac prems 1)
- ]);
+Goal "(x=UU)=(x<<UU)";
+by (rtac iffI 1);
+by (hyp_subst_tac 1);
+by (rtac refl_less 1);
+by (rtac antisym_less 1);
+by (atac 1);
+by (rtac minimal 1);
+qed "eq_UU_iff";
-qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac classical2 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac refl_less 1)
- ]);
+Goal "x << UU ==> x = UU";
+by (stac eq_UU_iff 1);
+by (assume_tac 1);
+qed "UU_I";
-qed_goal "chain_UU_I" thy
- "[|chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac allI 1),
- (rtac antisym_less 1),
- (rtac minimal 2),
- (etac subst 1),
- (etac is_ub_thelub 1)
- ]);
+Goal "~(x::'a::po)<<y ==> ~x=y";
+by Auto_tac;
+qed "not_less2not_eq";
+
+Goal "[|chain(Y);lub(range(Y))=UU|] ==> ALL i. Y(i)=UU";
+by (rtac allI 1);
+by (rtac antisym_less 1);
+by (rtac minimal 2);
+by (etac subst 1);
+by (etac is_ub_thelub 1);
+qed "chain_UU_I";
-qed_goal "chain_UU_I_inverse" thy
- "!i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac lub_chain_maxelem 1),
- (rtac exI 1),
- (etac spec 1),
- (rtac allI 1),
- (rtac (antisym_less_inverse RS conjunct1) 1),
- (etac spec 1)
- ]);
-
-qed_goal "chain_UU_I_inverse2" thy
- "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (not_all RS iffD1) 1),
- (rtac swap 1),
- (rtac chain_UU_I_inverse 2),
- (etac notnotD 2),
- (atac 1)
- ]);
-
+Goal "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU";
+by (rtac lub_chain_maxelem 1);
+by (rtac exI 1);
+by (etac spec 1);
+by (rtac allI 1);
+by (rtac (antisym_less_inverse RS conjunct1) 1);
+by (etac spec 1);
+qed "chain_UU_I_inverse";
-qed_goal "notUU_I" thy "[| x<<y; ~x=UU |] ==> ~y=UU"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac contrapos 1),
- (rtac UU_I 1),
- (hyp_subst_tac 1),
- (atac 1)
- ]);
-
+Goal "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> EX i.~ Y(i)=UU";
+by (blast_tac (claset() addIs [chain_UU_I_inverse]) 1);
+qed "chain_UU_I_inverse2";
-qed_goal "chain_mono2" thy
-"[|? j.~Y(j)=UU;chain(Y::nat=>'a::pcpo)|]\
-\ ==> ? j.!i. j<i-->~Y(i)=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- Safe_tac,
- (Step_tac 1),
- (strip_tac 1),
- (rtac notUU_I 1),
- (atac 2),
- (etac (chain_mono RS mp) 1),
- (atac 1)
- ]);
+Goal "[| x<<y; ~x=UU |] ==> ~y=UU";
+by (blast_tac (claset() addIs [UU_I]) 1);
+qed "notUU_I";
+
+Goal
+ "[|EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)|] ==> EX j. ALL i. j<i-->~Y(i)=UU";
+by (blast_tac (claset() addDs [notUU_I, chain_mono RS mp]) 1);
+qed "chain_mono2";
(**************************************)
(* some properties for chfin and flat *)
@@ -278,72 +192,66 @@
(* flat types are chfin *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chfin" thy [max_in_chain_def]
- "!Y::nat=>'a::flat. chain Y-->(? n. max_in_chain n Y)"
- (fn _ =>
- [
- (strip_tac 1),
- (case_tac "!i. Y(i)=UU" 1),
- (res_inst_tac [("x","0")] exI 1),
- (Asm_simp_tac 1),
- (Asm_full_simp_tac 1),
- (etac exE 1),
- (res_inst_tac [("x","i")] exI 1),
- (strip_tac 1),
- (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
- (etac (le_imp_less_or_eq RS disjE) 1),
- Safe_tac,
- (dtac (ax_flat RS spec RS spec RS mp) 1),
- (Fast_tac 1)
- ]);
+Goalw [max_in_chain_def]
+ "ALL Y::nat=>'a::flat. chain Y-->(EX n. max_in_chain n Y)";
+by (strip_tac 1);
+by (case_tac "ALL i. Y(i)=UU" 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac exE 1);
+by (res_inst_tac [("x","i")] exI 1);
+by (strip_tac 1);
+by (dres_inst_tac [("x","i"),("y","j")] chain_mono 1);
+by (etac (le_imp_less_or_eq RS disjE) 1);
+by Safe_tac;
+by (dtac (ax_flat RS spec RS spec RS mp) 1);
+by (Fast_tac 1);
+qed "flat_imp_chfin";
(* flat subclass of chfin --> adm_flat not needed *)
-qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)"
-(fn prems=>
- [
- cut_facts_tac prems 1,
- safe_tac (HOL_cs addSIs [refl_less]),
- dtac (ax_flat RS spec RS spec RS mp) 1,
- fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1
- ]);
+Goal "(a::'a::flat) ~= UU ==> a << b = (a = b)";
+by (safe_tac (HOL_cs addSIs [refl_less]));
+by (dtac (ax_flat RS spec RS spec RS mp) 1);
+by (fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1);
+qed "flat_eq";
-qed_goal "chfin2finch" thy
- "chain (Y::nat=>'a::chfin) ==> finite_chain Y"
- (fn prems =>
- [
- cut_facts_tac prems 1,
- fast_tac (HOL_cs addss
- (simpset() addsimps [chfin,finite_chain_def])) 1
- ]);
+Goal "chain (Y::nat=>'a::chfin) ==> finite_chain Y";
+by (force_tac (HOL_cs, simpset() addsimps [chfin,finite_chain_def]) 1);
+qed "chfin2finch";
(* ------------------------------------------------------------------------ *)
(* lemmata for improved admissibility introdution rule *)
(* ------------------------------------------------------------------------ *)
-qed_goal "infinite_chain_adm_lemma" Porder.thy
-"[|chain Y; !i. P (Y i); \
-\ (!!Y. [| chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
-\ |] ==> P (lub (range Y))"
- (fn prems => [
- cut_facts_tac prems 1,
- case_tac "finite_chain Y" 1,
- eresolve_tac prems 2, atac 2, atac 2,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
+val prems = Goal
+"[|chain Y; ALL i. P (Y i); \
+\ (!!Y. [| chain Y; ALL i. P (Y i); ~ finite_chain Y |] ==> P (lub(range Y)))\
+\ |] ==> P (lub (range Y))";
+by (cut_facts_tac prems 1);
+by (case_tac "finite_chain Y" 1);
+by (eresolve_tac prems 2);
+by (atac 2);
+by (atac 2);
+by (rewtac finite_chain_def);
+by (safe_tac HOL_cs);
+by (etac (lub_finch1 RS thelubI RS ssubst) 1);
+by (atac 1);
+by (etac spec 1);
+qed "infinite_chain_adm_lemma";
-qed_goal "increasing_chain_adm_lemma" Porder.thy
-"[|chain Y; !i. P (Y i); \
-\ (!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
-\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
- (fn prems => [
- cut_facts_tac prems 1,
- etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- etac swap 1,
- rewtac max_in_chain_def,
- resolve_tac prems 1, atac 1, atac 1,
- fast_tac (HOL_cs addDs [le_imp_less_or_eq]
- addEs [chain_mono RS mp]) 1]);
+val prems = Goal
+"[|chain Y; ALL i. P (Y i); \
+\ (!!Y. [| chain Y; ALL i. P (Y i); \
+\ ALL i. EX j. i < j & Y i ~= Y j & Y i << Y j|]\
+\ ==> P (lub (range Y))) |] ==> P (lub (range Y))";
+by (cut_facts_tac prems 1);
+by (etac infinite_chain_adm_lemma 1);
+by (atac 1);
+by (etac thin_rl 1);
+by (rewtac finite_chain_def);
+by (rewtac max_in_chain_def);
+by (fast_tac (HOL_cs addIs prems
+ addDs [le_imp_less_or_eq] addEs [chain_mono RS mp]) 1);
+qed "increasing_chain_adm_lemma";
--- a/src/HOLCF/Porder.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Porder.ML Wed Jun 28 10:54:21 2000 +0200
@@ -45,17 +45,14 @@
(atac 1)
]);
-qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (le_imp_less_or_eq RS disjE) 1),
- (atac 1),
- (etac (chain_mono RS mp) 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac refl_less 1)
- ]);
+Goal "[| chain F; x <= y |] ==> F x << F y";
+by (rtac (le_imp_less_or_eq RS disjE) 1);
+by (atac 1);
+by (etac (chain_mono RS mp) 1);
+by (atac 1);
+by (hyp_subst_tac 1);
+by (rtac refl_less 1);
+qed "chain_mono3";
(* ------------------------------------------------------------------------ *)
@@ -75,39 +72,28 @@
(* ------------------------------------------------------------------------ *)
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
-qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (stac lub 1),
- (etac (select_eq_Ex RS iffD2) 1)
- ]);
+Goal "? x. M <<| x ==> M <<| lub(M)";
+by (stac lub 1);
+by (etac (select_eq_Ex RS iffD2) 1);
+qed "lubI";
-qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exI 1)
- ]);
+Goal "M <<| lub(M) ==> ? x. M <<| x";
+by (etac exI 1);
+qed "lubE";
-qed_goal "lub_eq" thy "(? x. M <<| x) = M <<| lub(M)"
-(fn prems =>
- [
- (stac lub 1),
- (rtac (select_eq_Ex RS subst) 1),
- (rtac refl 1)
- ]);
+Goal "(? x. M <<| x) = M <<| lub(M)";
+by (stac lub 1);
+by (rtac (select_eq_Ex RS subst) 1);
+by (rtac refl 1);
+qed "lub_eq";
-qed_goal "thelubI" thy "M <<| l ==> lub(M) = l"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac unique_lub 1),
- (stac lub 1),
- (etac selectI 1),
- (atac 1)
- ]);
+Goal "M <<| l ==> lub(M) = l";
+by (rtac unique_lub 1);
+by (stac lub 1);
+by (etac selectI 1);
+by (atac 1);
+qed "thelubI";
Goal "lub{x} = x";
@@ -216,16 +202,13 @@
]);
-qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac chainI 1),
- (rtac allI 1),
- (induct_tac "i" 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1)
- ]);
+Goal "x<<y ==> chain (%i. if i=0 then x else y)";
+by (rtac chainI 1);
+by (rtac allI 1);
+by (induct_tac "i" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+qed "bin_chain";
qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
@@ -238,51 +221,42 @@
(Asm_simp_tac 1)
]);
-qed_goal "lub_bin_chain" thy
- "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y"
-(fn prems=>
- [ (cut_facts_tac prems 1),
- (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1),
- (rtac lub_finch1 2),
- (etac bin_chain 2),
- (etac bin_chainmax 2),
- (Simp_tac 1)
- ]);
+Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
+by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1
+ THEN rtac lub_finch1 2);
+by (etac bin_chain 2);
+by (etac bin_chainmax 2);
+by (Simp_tac 1);
+qed "lub_bin_chain";
(* ------------------------------------------------------------------------ *)
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_chain_maxelem" thy
-"[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac thelubI 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (etac ub_rangeI 1),
- (strip_tac 1),
- (etac exE 1),
- (hyp_subst_tac 1),
- (etac (ub_rangeE RS spec) 1)
- ]);
+Goal "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c";
+by (rtac thelubI 1);
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (etac ub_rangeI 1);
+by (strip_tac 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (etac (ub_rangeE RS spec) 1);
+qed "lub_chain_maxelem";
(* ------------------------------------------------------------------------ *)
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_const" thy "range(%x. c) <<| c"
- (fn prems =>
- [
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (strip_tac 1),
- (rtac refl_less 1),
- (strip_tac 1),
- (etac (ub_rangeE RS spec) 1)
- ]);
+Goal "range(%x. c) <<| c";
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (strip_tac 1);
+by (rtac refl_less 1);
+by (strip_tac 1);
+by (etac (ub_rangeE RS spec) 1);
+qed "lub_const";
--- a/src/HOLCF/Porder0.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Porder0.ML Wed Jun 28 10:54:21 2000 +0200
@@ -27,25 +27,18 @@
(* the reverse law of anti--symmetrie of << *)
(* ------------------------------------------------------------------------ *)
-qed_goal "antisym_less_inverse" thy "(x::'a::po)=y ==> x << y & y << x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
- ]);
+Goal "(x::'a::po)=y ==> x << y & y << x";
+by (rtac conjI 1);
+by ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1));
+by ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1));
+qed "antisym_less_inverse";
-qed_goal "box_less" thy
-"[| (a::'a::po) << b; c << a; b << d|] ==> c << d"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac trans_less 1),
- (etac trans_less 1),
- (atac 1)
- ]);
+Goal "[| (a::'a::po) << b; c << a; b << d|] ==> c << d";
+by (etac trans_less 1);
+by (etac trans_less 1);
+by (atac 1);
+qed "box_less";
Goal "((x::'a::po)=y) = (x << y & y << x)";
by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
--- a/src/HOLCF/Ssum0.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Ssum0.ML Wed Jun 28 10:54:21 2000 +0200
@@ -1,13 +1,11 @@
-(* Title: HOLCF/ssum0.ML
+(* Title: HOLCF/Ssum0.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory ssum0.thy
+Strict sum with typedef
*)
-open Ssum0;
-
(* ------------------------------------------------------------------------ *)
(* A non-emptyness result for Sssum *)
(* ------------------------------------------------------------------------ *)
@@ -30,12 +28,10 @@
(rtac refl 1)
]);
-qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
-(fn prems =>
- [
- (rtac inj_on_inverseI 1),
- (etac Abs_Ssum_inverse 1)
- ]);
+Goal "inj_on Abs_Ssum Ssum";
+by (rtac inj_on_inverseI 1);
+by (etac Abs_Ssum_inverse 1);
+qed "inj_on_Abs_Ssum";
(* ------------------------------------------------------------------------ *)
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
@@ -144,39 +140,31 @@
(resolve_tac prems 1)
]);
-qed_goal "inject_Sinl_Rep" Ssum0.thy
- "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (case_tac "a1=UU" 1),
- (hyp_subst_tac 1),
- (rtac (inject_Sinl_Rep1 RS sym) 1),
- (etac sym 1),
- (case_tac "a2=UU" 1),
- (hyp_subst_tac 1),
- (etac inject_Sinl_Rep1 1),
- (etac inject_Sinl_Rep2 1),
- (atac 1),
- (atac 1)
- ]);
+Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
+by (case_tac "a1=UU" 1);
+by (hyp_subst_tac 1);
+by (rtac (inject_Sinl_Rep1 RS sym) 1);
+by (etac sym 1);
+by (case_tac "a2=UU" 1);
+by (hyp_subst_tac 1);
+by (etac inject_Sinl_Rep1 1);
+by (etac inject_Sinl_Rep2 1);
+by (atac 1);
+by (atac 1);
+qed "inject_Sinl_Rep";
-qed_goal "inject_Sinr_Rep" Ssum0.thy
- "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (case_tac "b1=UU" 1),
- (hyp_subst_tac 1),
- (rtac (inject_Sinr_Rep1 RS sym) 1),
- (etac sym 1),
- (case_tac "b2=UU" 1),
- (hyp_subst_tac 1),
- (etac inject_Sinr_Rep1 1),
- (etac inject_Sinr_Rep2 1),
- (atac 1),
- (atac 1)
- ]);
+Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2";
+by (case_tac "b1=UU" 1);
+by (hyp_subst_tac 1);
+by (rtac (inject_Sinr_Rep1 RS sym) 1);
+by (etac sym 1);
+by (case_tac "b2=UU" 1);
+by (hyp_subst_tac 1);
+by (etac inject_Sinr_Rep1 1);
+by (etac inject_Sinr_Rep2 1);
+by (atac 1);
+by (atac 1);
+qed "inject_Sinr_Rep";
qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
"Isinl(a1)=Isinl(a2)==> a1=a2"
@@ -200,25 +188,17 @@
(rtac SsumIr 1)
]);
-qed_goal "inject_Isinl_rev" Ssum0.thy
-"a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac contrapos 1),
- (etac inject_Isinl 2),
- (atac 1)
- ]);
+Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
+by (rtac contrapos 1);
+by (etac inject_Isinl 2);
+by (atac 1);
+qed "inject_Isinl_rev";
-qed_goal "inject_Isinr_rev" Ssum0.thy
-"b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac contrapos 1),
- (etac inject_Isinr 2),
- (atac 1)
- ]);
+Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
+by (rtac contrapos 1);
+by (etac inject_Isinr 2);
+by (atac 1);
+qed "inject_Isinr_rev";
(* ------------------------------------------------------------------------ *)
(* Exhaustion of the strict sum ++ *)
@@ -270,34 +250,30 @@
(* elimination rules for the strict sum ++ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "IssumE" Ssum0.thy
+val prems = Goal
"[|p=Isinl(UU) ==> Q ;\
\ !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
-\ !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
- (fn prems =>
- [
- (rtac (Exh_Ssum RS disjE) 1),
- (etac disjE 2),
- (eresolve_tac prems 1),
- (etac exE 1),
- (etac conjE 1),
- (eresolve_tac prems 1),
- (atac 1),
- (etac exE 1),
- (etac conjE 1),
- (eresolve_tac prems 1),
- (atac 1)
- ]);
+\ !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q";
+by (rtac (Exh_Ssum RS disjE) 1);
+by (etac disjE 2);
+by (eresolve_tac prems 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (eresolve_tac prems 1);
+by (atac 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (eresolve_tac prems 1);
+by (atac 1);
+qed "IssumE";
-qed_goal "IssumE2" Ssum0.thy
-"[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
- (fn prems =>
- [
- (rtac IssumE 1),
- (eresolve_tac prems 1),
- (eresolve_tac prems 1),
- (eresolve_tac prems 1)
- ]);
+val prems = Goal
+"[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q";
+by (rtac IssumE 1);
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+qed "IssumE2";
--- a/src/HOLCF/Ssum1.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Ssum1.ML Wed Jun 28 10:54:21 2000 +0200
@@ -3,11 +3,9 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory Ssum1.thy
+Partial ordering for the strict sum ++
*)
-open Ssum1;
-
local
fun eq_left s1 s2 =
@@ -212,142 +210,120 @@
(* optimize lemmas about less_ssum *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_ssum2a" thy
- "(Isinl x) << (Isinl y) = (x << y)"
- (fn prems =>
- [
- (rtac less_ssum1a 1),
- (rtac refl 1),
- (rtac refl 1)
- ]);
+Goal "(Isinl x) << (Isinl y) = (x << y)";
+by (rtac less_ssum1a 1);
+by (rtac refl 1);
+by (rtac refl 1);
+qed "less_ssum2a";
-qed_goal "less_ssum2b" thy
- "(Isinr x) << (Isinr y) = (x << y)"
- (fn prems =>
- [
- (rtac less_ssum1b 1),
- (rtac refl 1),
- (rtac refl 1)
- ]);
+Goal "(Isinr x) << (Isinr y) = (x << y)";
+by (rtac less_ssum1b 1);
+by (rtac refl 1);
+by (rtac refl 1);
+qed "less_ssum2b";
-qed_goal "less_ssum2c" thy
- "(Isinl x) << (Isinr y) = (x = UU)"
- (fn prems =>
- [
- (rtac less_ssum1c 1),
- (rtac refl 1),
- (rtac refl 1)
- ]);
+Goal "(Isinl x) << (Isinr y) = (x = UU)";
+by (rtac less_ssum1c 1);
+by (rtac refl 1);
+by (rtac refl 1);
+qed "less_ssum2c";
-qed_goal "less_ssum2d" thy
- "(Isinr x) << (Isinl y) = (x = UU)"
- (fn prems =>
- [
- (rtac less_ssum1d 1),
- (rtac refl 1),
- (rtac refl 1)
- ]);
+Goal "(Isinr x) << (Isinl y) = (x = UU)";
+by (rtac less_ssum1d 1);
+by (rtac refl 1);
+by (rtac refl 1);
+qed "less_ssum2d";
(* ------------------------------------------------------------------------ *)
(* less_ssum is a partial order on ++ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
- (fn prems =>
- [
- (res_inst_tac [("p","p")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2a RS iffD2) 1),
- (rtac refl_less 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2b RS iffD2) 1),
- (rtac refl_less 1)
- ]);
+Goal "(p::'a++'b) << p";
+by (res_inst_tac [("p","p")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2a RS iffD2) 1);
+by (rtac refl_less 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2b RS iffD2) 1);
+by (rtac refl_less 1);
+qed "refl_less_ssum";
-qed_goal "antisym_less_ssum" thy
- "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] IssumE2 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("f","Isinl")] arg_cong 1),
- (rtac antisym_less 1),
- (etac (less_ssum2a RS iffD1) 1),
- (etac (less_ssum2a RS iffD1) 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2d RS iffD1 RS ssubst) 1),
- (etac (less_ssum2c RS iffD1 RS ssubst) 1),
- (rtac strict_IsinlIsinr 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2c RS iffD1 RS ssubst) 1),
- (etac (less_ssum2d RS iffD1 RS ssubst) 1),
- (rtac (strict_IsinlIsinr RS sym) 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("f","Isinr")] arg_cong 1),
- (rtac antisym_less 1),
- (etac (less_ssum2b RS iffD1) 1),
- (etac (less_ssum2b RS iffD1) 1)
- ]);
+Goal "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2";
+by (res_inst_tac [("p","p1")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("f","Isinl")] arg_cong 1);
+by (rtac antisym_less 1);
+by (etac (less_ssum2a RS iffD1) 1);
+by (etac (less_ssum2a RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
+by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
+by (rtac strict_IsinlIsinr 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
+by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
+by (rtac (strict_IsinlIsinr RS sym) 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("f","Isinr")] arg_cong 1);
+by (rtac antisym_less 1);
+by (etac (less_ssum2b RS iffD1) 1);
+by (etac (less_ssum2b RS iffD1) 1);
+qed "antisym_less_ssum";
-qed_goal "trans_less_ssum" thy
- "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] IssumE2 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p3")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2a RS iffD2) 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac trans_less 1),
- (etac (less_ssum2a RS iffD1) 1),
- (etac (less_ssum2a RS iffD1) 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2c RS iffD1 RS ssubst) 1),
- (rtac minimal 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2c RS iffD2) 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac UU_I 1),
- (rtac trans_less 1),
- (etac (less_ssum2a RS iffD1) 1),
- (rtac (antisym_less_inverse RS conjunct1) 1),
- (etac (less_ssum2c RS iffD1) 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2c RS iffD1) 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p3")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2d RS iffD2) 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2d RS iffD1) 1),
- (hyp_subst_tac 1),
- (rtac UU_I 1),
- (rtac trans_less 1),
- (etac (less_ssum2b RS iffD1) 1),
- (rtac (antisym_less_inverse RS conjunct1) 1),
- (etac (less_ssum2d RS iffD1) 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum2b RS iffD2) 1),
- (res_inst_tac [("p","p2")] IssumE2 1),
- (hyp_subst_tac 1),
- (etac (less_ssum2d RS iffD1 RS ssubst) 1),
- (rtac minimal 1),
- (hyp_subst_tac 1),
- (rtac trans_less 1),
- (etac (less_ssum2b RS iffD1) 1),
- (etac (less_ssum2b RS iffD1) 1)
- ]);
+Goal "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3";
+by (res_inst_tac [("p","p1")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p3")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2a RS iffD2) 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac trans_less 1);
+by (etac (less_ssum2a RS iffD1) 1);
+by (etac (less_ssum2a RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2c RS iffD1 RS ssubst) 1);
+by (rtac minimal 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2c RS iffD2) 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac UU_I 1);
+by (rtac trans_less 1);
+by (etac (less_ssum2a RS iffD1) 1);
+by (rtac (antisym_less_inverse RS conjunct1) 1);
+by (etac (less_ssum2c RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2c RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p3")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2d RS iffD2) 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2d RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (rtac UU_I 1);
+by (rtac trans_less 1);
+by (etac (less_ssum2b RS iffD1) 1);
+by (rtac (antisym_less_inverse RS conjunct1) 1);
+by (etac (less_ssum2d RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum2b RS iffD2) 1);
+by (res_inst_tac [("p","p2")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (etac (less_ssum2d RS iffD1 RS ssubst) 1);
+by (rtac minimal 1);
+by (hyp_subst_tac 1);
+by (rtac trans_less 1);
+by (etac (less_ssum2b RS iffD1) 1);
+by (etac (less_ssum2b RS iffD1) 1);
+qed "trans_less_ssum";
--- a/src/HOLCF/Ssum2.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Ssum2.ML Wed Jun 28 10:54:21 2000 +0200
@@ -3,76 +3,60 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for Ssum2.thy
+Class Instance ++::(pcpo,pcpo)po
*)
-open Ssum2;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_ssum_po" thy "(op <<)=(%s1 s2.@z.\
+Goal "(op <<)=(%s1 s2.@z.\
\ (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)\
\ &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)\
\ &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))\
-\ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
- (fn prems =>
- [
- (fold_goals_tac [less_ssum_def]),
- (rtac refl 1)
- ]);
+\ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))";
+by (fold_goals_tac [less_ssum_def]);
+by (rtac refl 1);
+qed "inst_ssum_po";
(* ------------------------------------------------------------------------ *)
(* access to less_ssum in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_ssum2a]) 1)
- ]);
+Goal "Isinl x << Isinl y = x << y";
+by (simp_tac (simpset() addsimps [less_ssum2a]) 1);
+qed "less_ssum3a";
-qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_ssum2b]) 1)
- ]);
+Goal "Isinr x << Isinr y = x << y";
+by (simp_tac (simpset() addsimps [less_ssum2b]) 1);
+qed "less_ssum3b";
-qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_ssum2c]) 1)
- ]);
+Goal "Isinl x << Isinr y = (x = UU)";
+by (simp_tac (simpset() addsimps [less_ssum2c]) 1);
+qed "less_ssum3c";
-qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_ssum2d]) 1)
- ]);
+Goal "Isinr x << Isinl y = (x = UU)";
+by (simp_tac (simpset() addsimps [less_ssum2d]) 1);
+qed "less_ssum3d";
(* ------------------------------------------------------------------------ *)
(* type ssum ++ is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_ssum" thy "Isinl UU << s"
- (fn prems =>
- [
- (res_inst_tac [("p","s")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum3a RS iffD2) 1),
- (rtac minimal 1),
- (hyp_subst_tac 1),
- (stac strict_IsinlIsinr 1),
- (rtac (less_ssum3b RS iffD2) 1),
- (rtac minimal 1)
- ]);
+Goal "Isinl UU << s";
+by (res_inst_tac [("p","s")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum3a RS iffD2) 1);
+by (rtac minimal 1);
+by (hyp_subst_tac 1);
+by (stac strict_IsinlIsinr 1);
+by (rtac (less_ssum3b RS iffD2) 1);
+by (rtac minimal 1);
+qed "minimal_ssum";
bind_thm ("UU_ssum_def",minimal_ssum RS minimal2UU RS sym);
-qed_goal "least_ssum" thy "? x::'a++'b.!y. x<<y"
-(fn prems =>
- [
- (res_inst_tac [("x","Isinl UU")] exI 1),
- (rtac (minimal_ssum RS allI) 1)
- ]);
+Goal "? x::'a++'b.!y. x<<y";
+by (res_inst_tac [("x","Isinl UU")] exI 1);
+by (rtac (minimal_ssum RS allI) 1);
+qed "least_ssum";
(* ------------------------------------------------------------------------ *)
(* Isinl, Isinr are monotone *)
@@ -173,229 +157,187 @@
(* some kind of exhaustion rules for chains in 'a ++ 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma1" thy
-"[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (fast_tac HOL_cs 1)
- ]);
+Goal "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))";
+by (fast_tac HOL_cs 1);
+qed "ssum_lemma1";
-qed_goal "ssum_lemma2" thy
-"[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] ==>\
-\ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (res_inst_tac [("p","Y(i)")] IssumE 1),
- (dtac spec 1),
- (contr_tac 1),
- (dtac spec 1),
- (contr_tac 1),
- (fast_tac HOL_cs 1)
- ]);
+Goal "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] \
+\ ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)";
+by (etac exE 1);
+by (res_inst_tac [("p","Y(i)")] IssumE 1);
+by (dtac spec 1);
+by (contr_tac 1);
+by (dtac spec 1);
+by (contr_tac 1);
+by (fast_tac HOL_cs 1);
+qed "ssum_lemma2";
-qed_goal "ssum_lemma3" thy
-"[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
-\ (!i.? y. Y(i)=Isinr(y))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (etac exE 1),
- (rtac allI 1),
- (res_inst_tac [("p","Y(ia)")] IssumE 1),
- (rtac exI 1),
- (rtac trans 1),
- (rtac strict_IsinlIsinr 2),
- (atac 1),
- (etac exI 2),
- (etac conjE 1),
- (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
- (hyp_subst_tac 2),
- (etac exI 2),
- (eres_inst_tac [("P","x=UU")] notE 1),
- (rtac (less_ssum3d RS iffD1) 1),
- (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
- (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
- (etac (chain_mono RS mp) 1),
- (atac 1),
- (eres_inst_tac [("P","xa=UU")] notE 1),
- (rtac (less_ssum3c RS iffD1) 1),
- (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
- (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
- (etac (chain_mono RS mp) 1),
- (atac 1)
- ]);
+Goal "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] \
+\ ==> (!i.? y. Y(i)=Isinr(y))";
+by (etac exE 1);
+by (etac exE 1);
+by (rtac allI 1);
+by (res_inst_tac [("p","Y(ia)")] IssumE 1);
+by (rtac exI 1);
+by (rtac trans 1);
+by (rtac strict_IsinlIsinr 2);
+by (atac 1);
+by (etac exI 2);
+by (etac conjE 1);
+by (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1);
+by (hyp_subst_tac 2);
+by (etac exI 2);
+by (eres_inst_tac [("P","x=UU")] notE 1);
+by (rtac (less_ssum3d RS iffD1) 1);
+by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1);
+by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1);
+by (etac (chain_mono RS mp) 1);
+by (atac 1);
+by (eres_inst_tac [("P","xa=UU")] notE 1);
+by (rtac (less_ssum3c RS iffD1) 1);
+by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1);
+by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1);
+by (etac (chain_mono RS mp) 1);
+by (atac 1);
+qed "ssum_lemma3";
-qed_goal "ssum_lemma4" thy
-"chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac case_split_thm 1),
- (etac disjI1 1),
- (rtac disjI2 1),
- (etac ssum_lemma3 1),
- (rtac ssum_lemma2 1),
- (etac ssum_lemma1 1)
- ]);
+Goal "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))";
+by (rtac case_split_thm 1);
+by (etac disjI1 1);
+by (rtac disjI2 1);
+by (etac ssum_lemma3 1);
+by (rtac ssum_lemma2 1);
+by (etac ssum_lemma1 1);
+qed "ssum_lemma4";
(* ------------------------------------------------------------------------ *)
(* restricted surjectivity of Isinl *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma5" thy
-"z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (hyp_subst_tac 1),
- (case_tac "x=UU" 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 1)
- ]);
+Goal "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z";
+by (hyp_subst_tac 1);
+by (case_tac "x=UU" 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 1);
+qed "ssum_lemma5";
(* ------------------------------------------------------------------------ *)
(* restricted surjectivity of Isinr *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma6" thy
-"z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (hyp_subst_tac 1),
- (case_tac "x=UU" 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 1)
- ]);
+Goal "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z";
+by (hyp_subst_tac 1);
+by (case_tac "x=UU" 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 1);
+qed "ssum_lemma6";
(* ------------------------------------------------------------------------ *)
(* technical lemmas *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma7" thy
-"[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","z")] IssumE 1),
- (hyp_subst_tac 1),
- (etac notE 1),
- (rtac antisym_less 1),
- (etac (less_ssum3a RS iffD1) 1),
- (rtac minimal 1),
- (fast_tac HOL_cs 1),
- (hyp_subst_tac 1),
- (rtac notE 1),
- (etac (less_ssum3c RS iffD1) 2),
- (atac 1)
- ]);
+Goal "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU";
+by (res_inst_tac [("p","z")] IssumE 1);
+by (hyp_subst_tac 1);
+by (etac notE 1);
+by (rtac antisym_less 1);
+by (etac (less_ssum3a RS iffD1) 1);
+by (rtac minimal 1);
+by (fast_tac HOL_cs 1);
+by (hyp_subst_tac 1);
+by (rtac notE 1);
+by (etac (less_ssum3c RS iffD1) 2);
+by (atac 1);
+qed "ssum_lemma7";
-qed_goal "ssum_lemma8" thy
-"[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","z")] IssumE 1),
- (hyp_subst_tac 1),
- (etac notE 1),
- (etac (less_ssum3d RS iffD1) 1),
- (hyp_subst_tac 1),
- (rtac notE 1),
- (etac (less_ssum3d RS iffD1) 2),
- (atac 1),
- (fast_tac HOL_cs 1)
- ]);
+Goal "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU";
+by (res_inst_tac [("p","z")] IssumE 1);
+by (hyp_subst_tac 1);
+by (etac notE 1);
+by (etac (less_ssum3d RS iffD1) 1);
+by (hyp_subst_tac 1);
+by (rtac notE 1);
+by (etac (less_ssum3d RS iffD1) 2);
+by (atac 1);
+by (fast_tac HOL_cs 1);
+qed "ssum_lemma8";
(* ------------------------------------------------------------------------ *)
(* the type 'a ++ 'b is a cpo in three steps *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_ssum1a" thy
-"[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
-\ range(Y) <<|\
-\ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (etac allE 1),
- (etac exE 1),
- (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1),
- (atac 1),
- (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
- (rtac is_ub_thelub 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (strip_tac 1),
- (res_inst_tac [("p","u")] IssumE2 1),
- (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1),
- (atac 1),
- (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
- (rtac is_lub_thelub 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ub2ub_monofun) 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum3c RS iffD2) 1),
- (rtac chain_UU_I_inverse 1),
- (rtac allI 1),
- (res_inst_tac [("p","Y(i)")] IssumE 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 2),
- (etac notE 1),
- (rtac (less_ssum3c RS iffD1) 1),
- (res_inst_tac [("t","Isinl(x)")] subst 1),
- (atac 1),
- (etac (ub_rangeE RS spec) 1)
- ]);
+Goal "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
+\ range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))";
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (etac allE 1);
+by (etac exE 1);
+by (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1);
+by (atac 1);
+by (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1);
+by (rtac is_ub_thelub 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","u")] IssumE2 1);
+by (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1);
+by (atac 1);
+by (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1);
+by (rtac is_lub_thelub 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ub2ub_monofun) 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum3c RS iffD2) 1);
+by (rtac chain_UU_I_inverse 1);
+by (rtac allI 1);
+by (res_inst_tac [("p","Y(i)")] IssumE 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 2);
+by (etac notE 1);
+by (rtac (less_ssum3c RS iffD1) 1);
+by (res_inst_tac [("t","Isinl(x)")] subst 1);
+by (atac 1);
+by (etac (ub_rangeE RS spec) 1);
+qed "lub_ssum1a";
-qed_goal "lub_ssum1b" thy
-"[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
-\ range(Y) <<|\
-\ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (etac allE 1),
- (etac exE 1),
- (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1),
- (atac 1),
- (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
- (rtac is_ub_thelub 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (strip_tac 1),
- (res_inst_tac [("p","u")] IssumE2 1),
- (hyp_subst_tac 1),
- (rtac (less_ssum3d RS iffD2) 1),
- (rtac chain_UU_I_inverse 1),
- (rtac allI 1),
- (res_inst_tac [("p","Y(i)")] IssumE 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 1),
- (etac notE 1),
- (rtac (less_ssum3d RS iffD1) 1),
- (res_inst_tac [("t","Isinr(y)")] subst 1),
- (atac 1),
- (etac (ub_rangeE RS spec) 1),
- (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1),
- (atac 1),
- (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
- (rtac is_lub_thelub 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ub2ub_monofun) 1)
- ]);
+Goal "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
+\ range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))";
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (etac allE 1);
+by (etac exE 1);
+by (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1);
+by (atac 1);
+by (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1);
+by (rtac is_ub_thelub 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","u")] IssumE2 1);
+by (hyp_subst_tac 1);
+by (rtac (less_ssum3d RS iffD2) 1);
+by (rtac chain_UU_I_inverse 1);
+by (rtac allI 1);
+by (res_inst_tac [("p","Y(i)")] IssumE 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (etac notE 1);
+by (rtac (less_ssum3d RS iffD1) 1);
+by (res_inst_tac [("t","Isinr(y)")] subst 1);
+by (atac 1);
+by (etac (ub_rangeE RS spec) 1);
+by (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1);
+by (atac 1);
+by (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1);
+by (rtac is_lub_thelub 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ub2ub_monofun) 1);
+qed "lub_ssum1b";
bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
@@ -412,18 +354,14 @@
(lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
*)
-qed_goal "cpo_ssum" thy
- "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (ssum_lemma4 RS disjE) 1),
- (atac 1),
- (rtac exI 1),
- (etac lub_ssum1a 1),
- (atac 1),
- (rtac exI 1),
- (etac lub_ssum1b 1),
- (atac 1)
- ]);
+Goal "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x";
+by (rtac (ssum_lemma4 RS disjE) 1);
+by (atac 1);
+by (rtac exI 1);
+by (etac lub_ssum1a 1);
+by (atac 1);
+by (rtac exI 1);
+by (etac lub_ssum1b 1);
+by (atac 1);
+qed "cpo_ssum";
--- a/src/HOLCF/Ssum3.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Ssum3.ML Wed Jun 28 10:54:21 2000 +0200
@@ -1,151 +1,135 @@
-(* Title: HOLCF/ssum3.ML
+(* Title: HOLCF/Ssum3.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for ssum3.thy
+Class instance of ++ for class pcpo
*)
-open Ssum3;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_ssum_pcpo" thy "UU = Isinl UU"
- (fn prems =>
- [
- (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1)
- ]);
+Goal "UU = Isinl UU";
+by (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1);
+qed "inst_ssum_pcpo";
(* ------------------------------------------------------------------------ *)
(* continuity for Isinl and Isinr *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_ssum1a RS sym) 2),
- (rtac allI 3),
- (rtac exI 3),
- (rtac refl 3),
- (etac (monofun_Isinl RS ch2ch_monofun) 2),
- (case_tac "lub(range(Y))=UU" 1),
- (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
- (atac 1),
- (res_inst_tac [("f","Isinl")] arg_cong 1),
- (rtac (chain_UU_I_inverse RS sym) 1),
- (rtac allI 1),
- (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
- (etac (chain_UU_I RS spec ) 1),
- (atac 1),
- (rtac Iwhen1 1),
- (res_inst_tac [("f","Isinl")] arg_cong 1),
- (rtac lub_equal 1),
- (atac 1),
- (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Isinl RS ch2ch_monofun) 1),
- (rtac allI 1),
- (case_tac "Y(k)=UU" 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 1)
- ]);
+Goal "contlub(Isinl)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_ssum1a RS sym) 2);
+by (rtac allI 3);
+by (rtac exI 3);
+by (rtac refl 3);
+by (etac (monofun_Isinl RS ch2ch_monofun) 2);
+by (case_tac "lub(range(Y))=UU" 1);
+by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
+by (atac 1);
+by (res_inst_tac [("f","Isinl")] arg_cong 1);
+by (rtac (chain_UU_I_inverse RS sym) 1);
+by (rtac allI 1);
+by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1);
+by (etac (chain_UU_I RS spec ) 1);
+by (atac 1);
+by (rtac Iwhen1 1);
+by (res_inst_tac [("f","Isinl")] arg_cong 1);
+by (rtac lub_equal 1);
+by (atac 1);
+by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Isinl RS ch2ch_monofun) 1);
+by (rtac allI 1);
+by (case_tac "Y(k)=UU" 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 1);
+qed "contlub_Isinl";
-qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_ssum1b RS sym) 2),
- (rtac allI 3),
- (rtac exI 3),
- (rtac refl 3),
- (etac (monofun_Isinr RS ch2ch_monofun) 2),
- (case_tac "lub(range(Y))=UU" 1),
- (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
- (atac 1),
- ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
- (rtac allI 1),
- (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
- (etac (chain_UU_I RS spec ) 1),
- (atac 1),
- (rtac (strict_IsinlIsinr RS subst) 1),
- (rtac Iwhen1 1),
- ((rtac arg_cong 1) THEN (rtac lub_equal 1)),
- (atac 1),
- (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Isinr RS ch2ch_monofun) 1),
- (rtac allI 1),
- (case_tac "Y(k)=UU" 1),
- (asm_simp_tac Ssum0_ss 1),
- (asm_simp_tac Ssum0_ss 1)
- ]);
+Goal "contlub(Isinr)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_ssum1b RS sym) 2);
+by (rtac allI 3);
+by (rtac exI 3);
+by (rtac refl 3);
+by (etac (monofun_Isinr RS ch2ch_monofun) 2);
+by (case_tac "lub(range(Y))=UU" 1);
+by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
+by (atac 1);
+by ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1));
+by (rtac allI 1);
+by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1);
+by (etac (chain_UU_I RS spec ) 1);
+by (atac 1);
+by (rtac (strict_IsinlIsinr RS subst) 1);
+by (rtac Iwhen1 1);
+by ((rtac arg_cong 1) THEN (rtac lub_equal 1));
+by (atac 1);
+by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Isinr RS ch2ch_monofun) 1);
+by (rtac allI 1);
+by (case_tac "Y(k)=UU" 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (asm_simp_tac Ssum0_ss 1);
+qed "contlub_Isinr";
-qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Isinl 1),
- (rtac contlub_Isinl 1)
- ]);
+Goal "cont(Isinl)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Isinl 1);
+by (rtac contlub_Isinl 1);
+qed "cont_Isinl";
-qed_goal "cont_Isinr" Ssum3.thy "cont(Isinr)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Isinr 1),
- (rtac contlub_Isinr 1)
- ]);
+Goal "cont(Isinr)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Isinr 1);
+by (rtac contlub_Isinr 1);
+qed "cont_Isinr";
(* ------------------------------------------------------------------------ *)
(* continuity for Iwhen in the firts two arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Iwhen1" Ssum3.thy "contlub(Iwhen)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_fun RS sym) 2),
- (etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
- (rtac (expand_fun_eq RS iffD2) 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_fun RS sym) 2),
- (rtac ch2ch_fun 2),
- (etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
- (rtac (expand_fun_eq RS iffD2) 1),
- (strip_tac 1),
- (res_inst_tac [("p","xa")] IssumE 1),
- (asm_simp_tac Ssum0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum0_ss 1),
- (etac contlub_cfun_fun 1),
- (asm_simp_tac Ssum0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1)
- ]);
+Goal "contlub(Iwhen)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_fun RS sym) 2);
+by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2);
+by (rtac (expand_fun_eq RS iffD2) 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_fun RS sym) 2);
+by (rtac ch2ch_fun 2);
+by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2);
+by (rtac (expand_fun_eq RS iffD2) 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","xa")] IssumE 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (etac contlub_cfun_fun 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+qed "contlub_Iwhen1";
-qed_goal "contlub_Iwhen2" Ssum3.thy "contlub(Iwhen(f))"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_fun RS sym) 2),
- (etac (monofun_Iwhen2 RS ch2ch_monofun) 2),
- (rtac (expand_fun_eq RS iffD2) 1),
- (strip_tac 1),
- (res_inst_tac [("p","x")] IssumE 1),
- (asm_simp_tac Ssum0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum0_ss 1),
- (etac contlub_cfun_fun 1)
- ]);
+Goal "contlub(Iwhen(f))";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_fun RS sym) 2);
+by (etac (monofun_Iwhen2 RS ch2ch_monofun) 2);
+by (rtac (expand_fun_eq RS iffD2) 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","x")] IssumE 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+by (asm_simp_tac Ssum0_ss 1);
+by (etac contlub_cfun_fun 1);
+qed "contlub_Iwhen2";
(* ------------------------------------------------------------------------ *)
(* continuity for Iwhen in its third argument *)
@@ -155,45 +139,36 @@
(* first 5 ugly lemmas *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma9" Ssum3.thy
-"[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("p","Y(i)")] IssumE 1),
- (etac exI 1),
- (etac exI 1),
- (res_inst_tac [("P","y=UU")] notE 1),
- (atac 1),
- (rtac (less_ssum3d RS iffD1) 1),
- (etac subst 1),
- (etac subst 1),
- (etac is_ub_thelub 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)";
+by (strip_tac 1);
+by (res_inst_tac [("p","Y(i)")] IssumE 1);
+by (etac exI 1);
+by (etac exI 1);
+by (res_inst_tac [("P","y=UU")] notE 1);
+by (atac 1);
+by (rtac (less_ssum3d RS iffD1) 1);
+by (etac subst 1);
+by (etac subst 1);
+by (etac is_ub_thelub 1);
+qed "ssum_lemma9";
-qed_goal "ssum_lemma10" Ssum3.thy
-"[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("p","Y(i)")] IssumE 1),
- (rtac exI 1),
- (etac trans 1),
- (rtac strict_IsinlIsinr 1),
- (etac exI 2),
- (res_inst_tac [("P","xa=UU")] notE 1),
- (atac 1),
- (rtac (less_ssum3c RS iffD1) 1),
- (etac subst 1),
- (etac subst 1),
- (etac is_ub_thelub 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)";
+by (strip_tac 1);
+by (res_inst_tac [("p","Y(i)")] IssumE 1);
+by (rtac exI 1);
+by (etac trans 1);
+by (rtac strict_IsinlIsinr 1);
+by (etac exI 2);
+by (res_inst_tac [("P","xa=UU")] notE 1);
+by (atac 1);
+by (rtac (less_ssum3c RS iffD1) 1);
+by (etac subst 1);
+by (etac subst 1);
+by (etac is_ub_thelub 1);
+qed "ssum_lemma10";
-Goal
-"[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
+Goal "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
by (asm_simp_tac Ssum0_ss 1);
by (rtac (chain_UU_I_inverse RS sym) 1);
@@ -206,168 +181,152 @@
by (asm_simp_tac Ssum0_ss 1);
qed "ssum_lemma11";
-qed_goal "ssum_lemma12" Ssum3.thy
-"[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
-\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac Ssum0_ss 1),
- (res_inst_tac [("t","x")] subst 1),
- (rtac inject_Isinl 1),
- (rtac trans 1),
- (atac 2),
- (rtac (thelub_ssum1a RS sym) 1),
- (atac 1),
- (etac ssum_lemma9 1),
- (atac 1),
- (rtac trans 1),
- (rtac contlub_cfun_arg 1),
- (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (atac 1),
- (rtac lub_equal2 1),
- (rtac (chain_mono2 RS exE) 1),
- (atac 2),
- (rtac chain_UU_I_inverse2 1),
- (stac inst_ssum_pcpo 1),
- (etac swap 1),
- (rtac inject_Isinl 1),
- (rtac trans 1),
- (etac sym 1),
- (etac notnotD 1),
- (rtac exI 1),
- (strip_tac 1),
- (rtac (ssum_lemma9 RS spec RS exE) 1),
- (atac 1),
- (atac 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (rtac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac Iwhen2 1),
- (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
- (fast_tac HOL_cs 1),
- (stac inst_ssum_pcpo 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (fast_tac HOL_cs 1),
- (stac Iwhen2 1),
- (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
- (fast_tac HOL_cs 1),
- (stac inst_ssum_pcpo 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (fast_tac HOL_cs 1),
- (simp_tac (simpset_of Cfun3.thy) 1),
- (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
+\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
+by (asm_simp_tac Ssum0_ss 1);
+by (res_inst_tac [("t","x")] subst 1);
+by (rtac inject_Isinl 1);
+by (rtac trans 1);
+by (atac 2);
+by (rtac (thelub_ssum1a RS sym) 1);
+by (atac 1);
+by (etac ssum_lemma9 1);
+by (atac 1);
+by (rtac trans 1);
+by (rtac contlub_cfun_arg 1);
+by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (atac 1);
+by (rtac lub_equal2 1);
+by (rtac (chain_mono2 RS exE) 1);
+by (atac 2);
+by (rtac chain_UU_I_inverse2 1);
+by (stac inst_ssum_pcpo 1);
+by (etac swap 1);
+by (rtac inject_Isinl 1);
+by (rtac trans 1);
+by (etac sym 1);
+by (etac notnotD 1);
+by (rtac exI 1);
+by (strip_tac 1);
+by (rtac (ssum_lemma9 RS spec RS exE) 1);
+by (atac 1);
+by (atac 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (rtac trans 1);
+by (rtac cfun_arg_cong 1);
+by (rtac Iwhen2 1);
+by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
+by (fast_tac HOL_cs 1);
+by (stac inst_ssum_pcpo 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (fast_tac HOL_cs 1);
+by (stac Iwhen2 1);
+by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
+by (fast_tac HOL_cs 1);
+by (stac inst_ssum_pcpo 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (simpset_of Cfun3.thy) 1);
+by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+qed "ssum_lemma12";
-qed_goal "ssum_lemma13" Ssum3.thy
-"[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
-\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac Ssum0_ss 1),
- (res_inst_tac [("t","x")] subst 1),
- (rtac inject_Isinr 1),
- (rtac trans 1),
- (atac 2),
- (rtac (thelub_ssum1b RS sym) 1),
- (atac 1),
- (etac ssum_lemma10 1),
- (atac 1),
- (rtac trans 1),
- (rtac contlub_cfun_arg 1),
- (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (atac 1),
- (rtac lub_equal2 1),
- (rtac (chain_mono2 RS exE) 1),
- (atac 2),
- (rtac chain_UU_I_inverse2 1),
- (stac inst_ssum_pcpo 1),
- (etac swap 1),
- (rtac inject_Isinr 1),
- (rtac trans 1),
- (etac sym 1),
- (rtac (strict_IsinlIsinr RS subst) 1),
- (etac notnotD 1),
- (rtac exI 1),
- (strip_tac 1),
- (rtac (ssum_lemma10 RS spec RS exE) 1),
- (atac 1),
- (atac 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (rtac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac Iwhen3 1),
- (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
- (fast_tac HOL_cs 1),
- (dtac notnotD 1),
- (stac inst_ssum_pcpo 1),
- (stac strict_IsinlIsinr 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (fast_tac HOL_cs 1),
- (stac Iwhen3 1),
- (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
- (fast_tac HOL_cs 1),
- (dtac notnotD 1),
- (stac inst_ssum_pcpo 1),
- (stac strict_IsinlIsinr 1),
- (res_inst_tac [("t","Y(i)")] ssubst 1),
- (atac 1),
- (fast_tac HOL_cs 1),
- (simp_tac (simpset_of Cfun3.thy) 1),
- (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
- (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
+\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
+by (asm_simp_tac Ssum0_ss 1);
+by (res_inst_tac [("t","x")] subst 1);
+by (rtac inject_Isinr 1);
+by (rtac trans 1);
+by (atac 2);
+by (rtac (thelub_ssum1b RS sym) 1);
+by (atac 1);
+by (etac ssum_lemma10 1);
+by (atac 1);
+by (rtac trans 1);
+by (rtac contlub_cfun_arg 1);
+by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (atac 1);
+by (rtac lub_equal2 1);
+by (rtac (chain_mono2 RS exE) 1);
+by (atac 2);
+by (rtac chain_UU_I_inverse2 1);
+by (stac inst_ssum_pcpo 1);
+by (etac swap 1);
+by (rtac inject_Isinr 1);
+by (rtac trans 1);
+by (etac sym 1);
+by (rtac (strict_IsinlIsinr RS subst) 1);
+by (etac notnotD 1);
+by (rtac exI 1);
+by (strip_tac 1);
+by (rtac (ssum_lemma10 RS spec RS exE) 1);
+by (atac 1);
+by (atac 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (rtac trans 1);
+by (rtac cfun_arg_cong 1);
+by (rtac Iwhen3 1);
+by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
+by (fast_tac HOL_cs 1);
+by (dtac notnotD 1);
+by (stac inst_ssum_pcpo 1);
+by (stac strict_IsinlIsinr 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (fast_tac HOL_cs 1);
+by (stac Iwhen3 1);
+by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
+by (fast_tac HOL_cs 1);
+by (dtac notnotD 1);
+by (stac inst_ssum_pcpo 1);
+by (stac strict_IsinlIsinr 1);
+by (res_inst_tac [("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (simpset_of Cfun3.thy) 1);
+by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
+qed "ssum_lemma13";
-qed_goal "contlub_Iwhen3" Ssum3.thy "contlub(Iwhen(f)(g))"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (res_inst_tac [("p","lub(range(Y))")] IssumE 1),
- (etac ssum_lemma11 1),
- (atac 1),
- (etac ssum_lemma12 1),
- (atac 1),
- (atac 1),
- (etac ssum_lemma13 1),
- (atac 1),
- (atac 1)
- ]);
+Goal "contlub(Iwhen(f)(g))";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","lub(range(Y))")] IssumE 1);
+by (etac ssum_lemma11 1);
+by (atac 1);
+by (etac ssum_lemma12 1);
+by (atac 1);
+by (atac 1);
+by (etac ssum_lemma13 1);
+by (atac 1);
+by (atac 1);
+qed "contlub_Iwhen3";
-qed_goal "cont_Iwhen1" Ssum3.thy "cont(Iwhen)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Iwhen1 1),
- (rtac contlub_Iwhen1 1)
- ]);
+Goal "cont(Iwhen)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Iwhen1 1);
+by (rtac contlub_Iwhen1 1);
+qed "cont_Iwhen1";
-qed_goal "cont_Iwhen2" Ssum3.thy "cont(Iwhen(f))"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Iwhen2 1),
- (rtac contlub_Iwhen2 1)
- ]);
+Goal "cont(Iwhen(f))";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Iwhen2 1);
+by (rtac contlub_Iwhen2 1);
+qed "cont_Iwhen2";
-qed_goal "cont_Iwhen3" Ssum3.thy "cont(Iwhen(f)(g))"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Iwhen3 1),
- (rtac contlub_Iwhen3 1)
- ]);
+Goal "cont(Iwhen(f)(g))";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Iwhen3 1);
+by (rtac contlub_Iwhen3 1);
+qed "cont_Iwhen3";
(* ------------------------------------------------------------------------ *)
(* continuous versions of lemmas for 'a ++ 'b *)
@@ -421,27 +380,19 @@
]);
-qed_goal "defined_sinl" Ssum3.thy
- "x~=UU ==> sinl`x ~= UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (rtac inject_sinl 1),
- (stac strict_sinl 1),
- (etac notnotD 1)
- ]);
+Goal "x~=UU ==> sinl`x ~= UU";
+by (etac swap 1);
+by (rtac inject_sinl 1);
+by (stac strict_sinl 1);
+by (etac notnotD 1);
+qed "defined_sinl";
-qed_goal "defined_sinr" Ssum3.thy
- "x~=UU ==> sinr`x ~= UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (rtac inject_sinr 1),
- (stac strict_sinr 1),
- (etac notnotD 1)
- ]);
+Goal "x~=UU ==> sinr`x ~= UU";
+by (etac swap 1);
+by (rtac inject_sinr 1);
+by (stac strict_sinr 1);
+by (etac notnotD 1);
+qed "defined_sinr";
qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def]
"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
@@ -665,33 +616,26 @@
cont_Iwhen3]) 1)
]);
-qed_goal "thelub_ssum3" Ssum3.thy
-"chain(Y) ==>\
+Goal "chain(Y) ==>\
\ lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))\
-\ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (ssum_chainE RS disjE) 1),
- (atac 1),
- (rtac disjI1 1),
- (etac thelub_ssum2a 1),
- (atac 1),
- (rtac disjI2 1),
- (etac thelub_ssum2b 1),
- (atac 1)
- ]);
+\ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))";
+by (rtac (ssum_chainE RS disjE) 1);
+by (atac 1);
+by (rtac disjI1 1);
+by (etac thelub_ssum2a 1);
+by (atac 1);
+by (rtac disjI2 1);
+by (etac thelub_ssum2b 1);
+by (atac 1);
+qed "thelub_ssum3";
-qed_goal "sscase4" Ssum3.thy
- "sscase`sinl`sinr`z=z"
- (fn prems =>
- [
- (res_inst_tac [("p","z")] ssumE 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1)
- ]);
+Goal "sscase`sinl`sinr`z=z";
+by (res_inst_tac [("p","z")] ssumE 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
+qed "sscase4";
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Tr.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Tr.ML Wed Jun 28 10:54:21 2000 +0200
@@ -19,16 +19,13 @@
(fast_tac (HOL_cs addss simpset()) 1)
]);
-qed_goal "trE" thy
- "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
- (fn prems =>
- [
- (rtac (Exh_tr RS disjE) 1),
- (eresolve_tac prems 1),
- (etac disjE 1),
- (eresolve_tac prems 1),
- (eresolve_tac prems 1)
- ]);
+val prems = Goal "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q";
+by (rtac (Exh_tr RS disjE) 1);
+by (eresolve_tac prems 1);
+by (etac disjE 1);
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+qed "trE";
(* ------------------------------------------------------------------------ *)
(* tactic for tr-thms with case split *)
--- a/src/HOLCF/Up1.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Up1.ML Wed Jun 28 10:54:21 2000 +0200
@@ -4,13 +4,9 @@
Copyright 1993 Technische Universitaet Muenchen
*)
-open Up1;
-
-qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
- ]);
+Goal "Rep_Up (Abs_Up y) = y";
+by (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1);
+qed "Abs_Up_inverse2";
qed_goalw "Exh_Up" thy [Iup_def ]
"z = Abs_Up(Inl ()) | (? x. z = Iup x)"
@@ -28,19 +24,15 @@
(atac 1)
]);
-qed_goal "inj_Abs_Up" thy "inj(Abs_Up)"
- (fn prems =>
- [
- (rtac inj_inverseI 1),
- (rtac Abs_Up_inverse2 1)
- ]);
+Goal "inj(Abs_Up)";
+by (rtac inj_inverseI 1);
+by (rtac Abs_Up_inverse2 1);
+qed "inj_Abs_Up";
-qed_goal "inj_Rep_Up" thy "inj(Rep_Up)"
- (fn prems =>
- [
- (rtac inj_inverseI 1),
- (rtac Rep_Up_inverse 1)
- ]);
+Goal "inj(Rep_Up)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Up_inverse 1);
+qed "inj_Rep_Up";
qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y"
(fn prems =>
@@ -51,6 +43,8 @@
(atac 1)
]);
+AddSDs [inject_Iup];
+
qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())"
(fn prems =>
[
@@ -62,15 +56,12 @@
]);
-qed_goal "upE" thy
- "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
- (fn prems =>
- [
- (rtac (Exh_Up RS disjE) 1),
- (eresolve_tac prems 1),
- (etac exE 1),
- (eresolve_tac prems 1)
- ]);
+val prems = Goal "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q";
+by (rtac (Exh_Up RS disjE) 1);
+by (eresolve_tac prems 1);
+by (etac exE 1);
+by (eresolve_tac prems 1);
+qed "upE";
qed_goalw "Ifup1" thy [Ifup_def]
"Ifup(f)(Abs_Up(Inl ()))=UU"
@@ -93,6 +84,8 @@
val Up0_ss = (simpset_of Cfun3.thy) delsimps [range_composition]
addsimps [Ifup1,Ifup2];
+Addsimps [Ifup1,Ifup2];
+
qed_goalw "less_up1a" thy [less_up_def]
"Abs_Up(Inl ())<< z"
(fn prems =>
@@ -117,7 +110,7 @@
]);
qed_goalw "less_up1c" thy [Iup_def,less_up_def]
- " (Iup x) << (Iup y)=(x<<y)"
+ "(Iup x) << (Iup y)=(x<<y)"
(fn prems =>
[
(stac Abs_Up_inverse2 1),
@@ -127,67 +120,43 @@
(rtac refl 1)
]);
+AddIffs [less_up1a, less_up1b, less_up1c];
-qed_goal "refl_less_up" thy "(p::'a u) << p"
- (fn prems =>
- [
- (res_inst_tac [("p","p")] upE 1),
- (hyp_subst_tac 1),
- (rtac less_up1a 1),
- (hyp_subst_tac 1),
- (rtac (less_up1c RS iffD2) 1),
- (rtac refl_less 1)
- ]);
+Goal "(p::'a u) << p";
+by (res_inst_tac [("p","p")] upE 1);
+by Auto_tac;
+qed "refl_less_up";
-qed_goal "antisym_less_up" thy
- "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
- (fn _ =>
- [
- (res_inst_tac [("p","p1")] upE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] upE 1),
- (etac sym 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
- (rtac less_up1b 1),
- (atac 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] upE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
- (rtac less_up1b 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac arg_cong 1),
- (rtac antisym_less 1),
- (etac (less_up1c RS iffD1) 1),
- (etac (less_up1c RS iffD1) 1)
- ]);
+Goal "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2";
+by (res_inst_tac [("p","p1")] upE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (etac sym 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (blast_tac (claset() addIs [arg_cong, antisym_less, less_up1c RS iffD1]) 1);
+qed "antisym_less_up";
-qed_goal "trans_less_up" thy
- "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] upE 1),
- (hyp_subst_tac 1),
- (rtac less_up1a 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] upE 1),
- (hyp_subst_tac 1),
- (rtac notE 1),
- (rtac less_up1b 1),
- (atac 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p3")] upE 1),
- (hyp_subst_tac 1),
- (rtac notE 1),
- (rtac less_up1b 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac (less_up1c RS iffD2) 1),
- (rtac trans_less 1),
- (etac (less_up1c RS iffD1) 1),
- (etac (less_up1c RS iffD1) 1)
- ]);
+Goal "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3";
+by (res_inst_tac [("p","p1")] upE 1);
+by (hyp_subst_tac 1);
+by (rtac less_up1a 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (hyp_subst_tac 1);
+by (rtac notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (res_inst_tac [("p","p3")] upE 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [trans_less]) 1);
+qed "trans_less_up";
--- a/src/HOLCF/Up2.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Up2.ML Wed Jun 28 10:54:21 2000 +0200
@@ -6,53 +6,41 @@
Lemmas for Up2.thy
*)
-open Up2;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_po" thy "(op <<)=(%x1 x2. case Rep_Up(x1) of \
+Goal "(op <<)=(%x1 x2. case Rep_Up(x1) of \
\ Inl(y1) => True \
\ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
-\ | Inr(z2) => y2<<z2))"
- (fn prems =>
- [
- (fold_goals_tac [less_up_def]),
- (rtac refl 1)
- ]);
+\ | Inr(z2) => y2<<z2))";
+by (fold_goals_tac [less_up_def]);
+by (rtac refl 1);
+qed "inst_up_po";
(* -------------------------------------------------------------------------*)
(* type ('a)u is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_up1a]) 1)
- ]);
+Goal "Abs_Up(Inl ()) << z";
+by (simp_tac (simpset() addsimps [less_up1a]) 1);
+qed "minimal_up";
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
-qed_goal "least_up" thy "? x::'a u.!y. x<<y"
-(fn prems =>
- [
- (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
- (rtac (minimal_up RS allI) 1)
- ]);
+Goal "? x::'a u.!y. x<<y";
+by (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1);
+by (rtac (minimal_up RS allI) 1);
+qed "least_up";
(* -------------------------------------------------------------------------*)
(* access to less_up in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_up1b]) 1)
- ]);
+Goal "~ Iup(x) << Abs_Up(Inl ())";
+by (simp_tac (simpset() addsimps [less_up1b]) 1);
+qed "less_up2b";
-qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [less_up1c]) 1)
- ]);
+Goal "(Iup(x)<<Iup(y)) = (x<<y)";
+by (simp_tac (simpset() addsimps [less_up1c]) 1);
+qed "less_up2c";
(* ------------------------------------------------------------------------ *)
(* Iup and Ifup are monotone *)
@@ -99,76 +87,64 @@
(* Some kind of surjectivity lemma *)
(* ------------------------------------------------------------------------ *)
-qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac Up0_ss 1)
- ]);
+Goal "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z";
+by (asm_simp_tac Up0_ss 1);
+qed "up_lemma1";
(* ------------------------------------------------------------------------ *)
(* ('a)u is a cpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_up1a" thy
-"[|chain(Y);? i x. Y(i)=Iup(x)|] ==>\
-\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (res_inst_tac [("p","Y(i)")] upE 1),
- (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1),
- (etac sym 1),
- (rtac minimal_up 1),
- (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1),
- (atac 1),
- (rtac (less_up2c RS iffD2) 1),
- (rtac is_ub_thelub 1),
- (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
- (strip_tac 1),
- (res_inst_tac [("p","u")] upE 1),
- (etac exE 1),
- (etac exE 1),
- (res_inst_tac [("P","Y(i)<<Abs_Up (Inl ())")] notE 1),
- (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
- (atac 1),
- (rtac less_up2b 1),
- (hyp_subst_tac 1),
- (etac (ub_rangeE RS spec) 1),
- (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1),
- (atac 1),
- (rtac (less_up2c RS iffD2) 1),
- (rtac is_lub_thelub 1),
- (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
- (etac (monofun_Ifup2 RS ub2ub_monofun) 1)
- ]);
+Goal "[|chain(Y);? i x. Y(i)=Iup(x)|] \
+\ ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))";
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (res_inst_tac [("p","Y(i)")] upE 1);
+by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1);
+by (etac sym 1);
+by (rtac minimal_up 1);
+by (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1);
+by (atac 1);
+by (rtac (less_up2c RS iffD2) 1);
+by (rtac is_ub_thelub 1);
+by (etac (monofun_Ifup2 RS ch2ch_monofun) 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","u")] upE 1);
+by (etac exE 1);
+by (etac exE 1);
+by (res_inst_tac [("P","Y(i)<<Abs_Up (Inl ())")] notE 1);
+by (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (rtac less_up2b 1);
+by (hyp_subst_tac 1);
+by (etac (ub_rangeE RS spec) 1);
+by (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1);
+by (atac 1);
+by (rtac (less_up2c RS iffD2) 1);
+by (rtac is_lub_thelub 1);
+by (etac (monofun_Ifup2 RS ch2ch_monofun) 1);
+by (etac (monofun_Ifup2 RS ub2ub_monofun) 1);
+qed "lub_up1a";
-qed_goal "lub_up1b" thy
-"[|chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
-\ range(Y) <<| Abs_Up (Inl ())"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (res_inst_tac [("p","Y(i)")] upE 1),
- (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1),
- (atac 1),
- (rtac refl_less 1),
- (rtac notE 1),
- (dtac spec 1),
- (dtac spec 1),
- (atac 1),
- (atac 1),
- (strip_tac 1),
- (rtac minimal_up 1)
- ]);
+Goal "[|chain(Y);!i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())";
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (res_inst_tac [("p","Y(i)")] upE 1);
+by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1);
+by (atac 1);
+by (rtac refl_less 1);
+by (rtac notE 1);
+by (dtac spec 1);
+by (dtac spec 1);
+by (atac 1);
+by (atac 1);
+by (strip_tac 1);
+by (rtac minimal_up 1);
+qed "lub_up1b";
bind_thm ("thelub_up1a", lub_up1a RS thelubI);
(*
@@ -182,18 +158,14 @@
lub (range ?Y1) = UU_up
*)
-qed_goal "cpo_up" thy
- "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac disjE 1),
- (rtac exI 2),
- (etac lub_up1a 2),
- (atac 2),
- (rtac exI 2),
- (etac lub_up1b 2),
- (atac 2),
- (fast_tac HOL_cs 1)
- ]);
+Goal "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x";
+by (rtac disjE 1);
+by (rtac exI 2);
+by (etac lub_up1a 2);
+by (atac 2);
+by (rtac exI 2);
+by (etac lub_up1b 2);
+by (atac 2);
+by (fast_tac HOL_cs 1);
+qed "cpo_up";
--- a/src/HOLCF/Up3.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Up3.ML Wed Jun 28 10:54:21 2000 +0200
@@ -3,85 +3,71 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for Up3.thy
+Class instance of ('a)u for class pcpo
*)
-open Up3;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())"
- (fn prems =>
- [
- (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1)
- ]);
+Goal "UU = Abs_Up(Inl ())";
+by (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1);
+qed "inst_up_pcpo";
(* -------------------------------------------------------------------------*)
(* some lemmas restated for class pcpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up3b" thy "~ Iup(x) << UU"
- (fn prems =>
- [
- (stac inst_up_pcpo 1),
- (rtac less_up2b 1)
- ]);
+Goal "~ Iup(x) << UU";
+by (stac inst_up_pcpo 1);
+by (rtac less_up2b 1);
+qed "less_up3b";
-qed_goal "defined_Iup2" thy "Iup(x) ~= UU"
- (fn prems =>
- [
- (stac inst_up_pcpo 1),
- (rtac defined_Iup 1)
- ]);
+Goal "Iup(x) ~= UU";
+by (stac inst_up_pcpo 1);
+by (rtac defined_Iup 1);
+qed "defined_Iup2";
(* ------------------------------------------------------------------------ *)
(* continuity for Iup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Iup" thy "contlub(Iup)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_up1a RS sym) 2),
- (fast_tac HOL_cs 3),
- (etac (monofun_Iup RS ch2ch_monofun) 2),
- (res_inst_tac [("f","Iup")] arg_cong 1),
- (rtac lub_equal 1),
- (atac 1),
- (rtac (monofun_Ifup2 RS ch2ch_monofun) 1),
- (etac (monofun_Iup RS ch2ch_monofun) 1),
- (asm_simp_tac Up0_ss 1)
- ]);
+Goal "contlub(Iup)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_up1a RS sym) 2);
+by (fast_tac HOL_cs 3);
+by (etac (monofun_Iup RS ch2ch_monofun) 2);
+by (res_inst_tac [("f","Iup")] arg_cong 1);
+by (rtac lub_equal 1);
+by (atac 1);
+by (rtac (monofun_Ifup2 RS ch2ch_monofun) 1);
+by (etac (monofun_Iup RS ch2ch_monofun) 1);
+by (asm_simp_tac Up0_ss 1);
+qed "contlub_Iup";
-qed_goal "cont_Iup" thy "cont(Iup)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Iup 1),
- (rtac contlub_Iup 1)
- ]);
+Goal "cont(Iup)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Iup 1);
+by (rtac contlub_Iup 1);
+qed "cont_Iup";
(* ------------------------------------------------------------------------ *)
(* continuity for Ifup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Ifup1" thy "contlub(Ifup)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_fun RS sym) 2),
- (etac (monofun_Ifup1 RS ch2ch_monofun) 2),
- (rtac ext 1),
- (res_inst_tac [("p","x")] upE 1),
- (asm_simp_tac Up0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Up0_ss 1),
- (etac contlub_cfun_fun 1)
- ]);
+Goal "contlub(Ifup)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_fun RS sym) 2);
+by (etac (monofun_Ifup1 RS ch2ch_monofun) 2);
+by (rtac ext 1);
+by (res_inst_tac [("p","x")] upE 1);
+by (asm_simp_tac Up0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+by (asm_simp_tac Up0_ss 1);
+by (etac contlub_cfun_fun 1);
+qed "contlub_Ifup1";
Goal "contlub(Ifup(f))";
@@ -129,21 +115,17 @@
by (atac 1);
qed "contlub_Ifup2";
-qed_goal "cont_Ifup1" thy "cont(Ifup)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Ifup1 1),
- (rtac contlub_Ifup1 1)
- ]);
+Goal "cont(Ifup)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Ifup1 1);
+by (rtac contlub_Ifup1 1);
+qed "cont_Ifup1";
-qed_goal "cont_Ifup2" thy "cont(Ifup(f))"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Ifup2 1),
- (rtac contlub_Ifup2 1)
- ]);
+Goal "cont(Ifup(f))";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Ifup2 1);
+by (rtac contlub_Ifup2 1);
+qed "cont_Ifup2";
(* ------------------------------------------------------------------------ *)
@@ -272,72 +254,58 @@
]);
-qed_goal "up_lemma2" thy " (? x. z = up`x) = (z~=UU)"
- (fn prems =>
- [
- (rtac iffI 1),
- (etac exE 1),
- (hyp_subst_tac 1),
- (rtac defined_up 1),
- (res_inst_tac [("p","z")] upE1 1),
- (etac notE 1),
- (atac 1),
- (etac exI 1)
- ]);
+Goal "(? x. z = up`x) = (z~=UU)";
+by (rtac iffI 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (rtac defined_up 1);
+by (res_inst_tac [("p","z")] upE1 1);
+by (etac notE 1);
+by (atac 1);
+by (etac exI 1);
+qed "up_lemma2";
-qed_goal "thelub_up2a_rev" thy
-"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac exE 1),
- (rtac chain_UU_I_inverse2 1),
- (rtac (up_lemma2 RS iffD1) 1),
- (etac exI 1),
- (rtac exI 1),
- (rtac (up_lemma2 RS iffD2) 1),
- (atac 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x";
+by (rtac exE 1);
+by (rtac chain_UU_I_inverse2 1);
+by (rtac (up_lemma2 RS iffD1) 1);
+by (etac exI 1);
+by (rtac exI 1);
+by (rtac (up_lemma2 RS iffD2) 1);
+by (atac 1);
+qed "thelub_up2a_rev";
-qed_goal "thelub_up2b_rev" thy
-"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac allI 1),
- (rtac (not_ex RS iffD1) 1),
- (rtac contrapos 1),
- (etac (up_lemma2 RS iffD1) 2),
- (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x";
+by (cut_facts_tac prems 1);
+by (rtac allI 1);
+by (rtac (not_ex RS iffD1) 1);
+by (rtac contrapos 1);
+by (etac (up_lemma2 RS iffD1) 2);
+by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1);
+qed "thelub_up2b_rev";
-qed_goal "thelub_up3" thy
-"chain(Y) ==> lub(range(Y)) = UU |\
-\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac disjE 1),
- (rtac disjI1 2),
- (rtac thelub_up2b 2),
- (atac 2),
- (atac 2),
- (rtac disjI2 2),
- (rtac thelub_up2a 2),
- (atac 2),
- (atac 2),
- (fast_tac HOL_cs 1)
- ]);
+Goal "chain(Y) ==> lub(range(Y)) = UU | \
+\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
+by (cut_facts_tac prems 1);
+by (rtac disjE 1);
+by (rtac disjI1 2);
+by (rtac thelub_up2b 2);
+by (atac 2);
+by (atac 2);
+by (rtac disjI2 2);
+by (rtac thelub_up2a 2);
+by (atac 2);
+by (atac 2);
+by (fast_tac HOL_cs 1);
+qed "thelub_up3";
-qed_goal "fup3" thy "fup`up`x=x"
- (fn prems =>
- [
- (res_inst_tac [("p","x")] upE1 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
- ]);
+Goal "fup`up`x=x";
+by (res_inst_tac [("p","x")] upE1 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
+qed "fup3";
(* ------------------------------------------------------------------------ *)
(* install simplifier for ('a)u *)
--- a/src/HOLCF/ex/Loop.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/ex/Loop.ML Wed Jun 28 10:54:21 2000 +0200
@@ -3,14 +3,12 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory loop.thy
+Theory for a loop primitive like while
*)
-open Loop;
-
-(* --------------------------------------------------------------------------- *)
-(* access to definitions *)
-(* --------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+(* access to definitions *)
+(* ------------------------------------------------------------------------- *)
val step_def2 = prove_goalw Loop.thy [step_def]
"step`b`g`x = If b`x then g`x else x fi"
@@ -40,7 +38,7 @@
]);
val while_unfold2 = prove_goal Loop.thy
- "!x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
+ "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
(fn prems =>
[
(nat_ind_tac "k" 1),
@@ -78,12 +76,13 @@
]);
-(* --------------------------------------------------------------------------- *)
-(* properties of while and iterations *)
-(* --------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+(* properties of while and iterations *)
+(* ------------------------------------------------------------------------- *)
val loop_lemma1 = prove_goal Loop.thy
-"[|? y. b`y=FF; iterate k (step`b`g) x = UU|]==>iterate(Suc k) (step`b`g) x=UU"
+ "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
+\ ==>iterate(Suc k) (step`b`g) x=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -98,7 +97,7 @@
]);
val loop_lemma2 = prove_goal Loop.thy
-"[|? y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
+"[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
\iterate k (step`b`g) x ~=UU"
(fn prems =>
[
@@ -110,9 +109,9 @@
]);
val loop_lemma3 = prove_goal Loop.thy
-"[|!x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
-\? y. b`y=FF; INV x|] ==>\
-\iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)"
+"[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
+\ EX y. b`y=FF; INV x |] \
+\==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -138,7 +137,7 @@
val loop_lemma4 = prove_goal Loop.thy
-"!x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x"
+"ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x"
(fn prems =>
[
(nat_ind_tac "k" 1),
@@ -155,8 +154,8 @@
]);
val loop_lemma5 = prove_goal Loop.thy
-"!k. b`(iterate k (step`b`g) x) ~= FF ==>\
-\ !m. while`b`g`(iterate m (step`b`g) x)=UU"
+"ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
+\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -183,7 +182,7 @@
val loop_lemma6 = prove_goal Loop.thy
-"!k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU"
+"ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU"
(fn prems =>
[
(res_inst_tac [("t","x")] (iterate_0 RS subst) 1),
@@ -192,7 +191,7 @@
]);
val loop_lemma7 = prove_goal Loop.thy
-"while`b`g`x ~= UU ==> ? k. b`(iterate k (step`b`g) x) = FF"
+"while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -202,7 +201,7 @@
]);
val loop_lemma8 = prove_goal Loop.thy
-"while`b`g`x ~= UU ==> ? y. b`y=FF"
+"while`b`g`x ~= UU ==> EX y. b`y=FF"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -216,8 +215,8 @@
(* ------------------------------------------------------------------------- *)
val loop_inv2 = prove_goal Loop.thy
-"[| (!y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
-\ (!y. INV y & b`y=FF --> Q y);\
+"[| (ALL y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
+\ (ALL y. INV y & b`y=FF --> Q y);\
\ INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)"
(fn prems =>
[
@@ -234,7 +233,7 @@
(rtac loop_lemma8 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
- (rtac classical2 1),
+ (rtac notI2 1),
(resolve_tac prems 1),
(etac box_equals 1),
(rtac (loop_lemma4 RS spec RS mp RS sym) 1),
--- a/src/HOLCF/ex/Stream.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/ex/Stream.ML Wed Jun 28 10:54:21 2000 +0200
@@ -1,17 +1,17 @@
-(* Title: FOCUS/Stream.ML
- ID: $ $
+(* Title: HOLCF/ex//Stream.ML
+ ID: $Id$
Author: Franz Regensburger, David von Oheimb
Copyright 1993, 1995 Technische Universitaet Muenchen
-Theorems for Stream.thy
+general Stream domain
*)
-open Stream;
-
fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
+val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
+
(* ----------------------------------------------------------------------- *)
(* theorems about scons *)
(* ----------------------------------------------------------------------- *)
@@ -23,36 +23,40 @@
etac contrapos2 1,
safe_tac (HOL_cs addSIs stream.con_rews)]);
-qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R" (fn prems => [
+qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R"
+ (fn prems => [
cut_facts_tac prems 1,
- dresolve_tac stream.con_rews 1,
+ dresolve_tac [stream_con_rew2] 1,
contr_tac 1]);
-qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU & x = a && y)" (fn _ =>[
+qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU & x = a && y)"
+ (fn _ =>[
cut_facts_tac [stream.exhaust] 1,
safe_tac HOL_cs,
contr_tac 1,
- fast_tac (HOL_cs addDs (tl stream.con_rews)) 1,
+ fast_tac (HOL_cs addDs [stream_con_rew2]) 1,
fast_tac HOL_cs 1,
- fast_tac (HOL_cs addDs (tl stream.con_rews)) 1]);
+ fast_tac (HOL_cs addDs [stream_con_rew2]) 1]);
qed_goal "stream_prefix" thy
-"[| a && s << t; a ~= UU |] ==> ? b tt. t = b && tt & b ~= UU & s << tt" (fn prems => [
+"[| a && s << t; a ~= UU |] ==> ? b tt. t = b && tt & b ~= UU & s << tt"
+ (fn prems => [
cut_facts_tac prems 1,
stream_case_tac "t" 1,
- fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2,hd (tl stream.con_rews)]) 1,
+ fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1,
fast_tac (HOL_cs addDs stream.inverts) 1]);
qed_goal "stream_flat_prefix" thy
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
(fn prems=>[
cut_facts_tac prems 1,
- (cut_facts_tac [read_instantiate[("x1","x::'a::flat"),("x","y::'a::flat")]
- (ax_flat RS spec RS spec)] 1),
+ (cut_facts_tac [read_instantiate[("x1","x::'a::flat"),
+ ("x","y::'a::flat")]
+ (ax_flat RS spec RS spec)] 1),
(forward_tac stream.inverts 1),
(safe_tac HOL_cs),
(dtac (hd stream.con_rews RS subst) 1),
- (fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1)]);
+ (fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1)]);
qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
\(x = UU | (? a y. x = a && y & a ~= UU & a << b & y << z))" (fn prems => [
--- a/src/HOLCF/ex/Stream.thy Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/ex/Stream.thy Wed Jun 28 10:54:21 2000 +0200
@@ -1,5 +1,5 @@
-(* Title: FOCUS/Stream.thy
- ID: $ $
+(* Title: HOLCF/ex//Stream.thy
+ ID: $Id$
Author: Franz Regensburger, David von Oheimb
Copyright 1993, 1995 Technische Universitaet Muenchen