# HG changeset patch # User paulson # Date 962182461 -7200 # Node ID 85a47aa21f749af5fa3dc58e0bfcb5751c069089 # Parent 77658111e1228f4d25425bda27d2088b47906388 tidying and unbatchifying diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Pcpo.ML --- 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 X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\ -\ ==> lub(range(X))< - [ - (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 X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\ +\ ==> lub(range(X))< 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 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))< - [ - (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))< [ - Fast_tac 1]); - -qed_goal "eq_UU_iff" thy "(x=UU)=(x< - [ - (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< ~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)< ~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=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~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=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~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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Porder.ML --- 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< 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< 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< 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< 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< 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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Porder0.ML --- 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); diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Ssum0.ML --- 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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Ssum1.ML --- 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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Ssum2.ML --- 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< - [ - (res_inst_tac [("x","Isinl UU")] exI 1), - (rtac (minimal_ssum RS allI) 1) - ]); +Goal "? x::'a++'b.!y. 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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Ssum3.ML --- 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"; (* ------------------------------------------------------------------------ *) diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Tr.ML --- 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 *) diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Up1.ML --- 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< [ (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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Up2.ML --- 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< - [ - (fold_goals_tac [less_up_def]), - (rtac refl 1) - ]); +\ | Inr(z2) => y2< - [ - (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< - [ - (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1), - (rtac (minimal_up RS allI) 1) - ]); +Goal "? x::'a u.!y. x< - [ - (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)< - [ - (simp_tac (simpset() addsimps [less_up1c]) 1) - ]); +Goal "(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)< 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)<\ -\ 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"; diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/Up3.ML --- 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 *) diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/ex/Loop.ML --- 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), diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/ex/Stream.ML --- 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 => [ diff -r 77658111e122 -r 85a47aa21f74 src/HOLCF/ex/Stream.thy --- 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