# HG changeset patch # User oheimb # Date 854715453 -3600 # Node ID cbf02fc743320c9e26492606770bc190cfdcb690 # Parent 64e52912eb090961c692296be00a8cda5e17518b changed handling of cont_lemmas and adm_lemmas diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Cfun3.ML --- a/src/HOLCF/Cfun3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Cfun3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -193,13 +193,15 @@ (* cont2cont tactic *) (* ------------------------------------------------------------------------ *) -val cont_lemmas = [cont_const, cont_id, cont_fapp2, - cont2cont_fapp,cont2cont_LAM2]; +val cont_lemmas1 = [cont_const, cont_id, cont_fapp2, + cont2cont_fapp,cont2cont_LAM2]; + +Addsimps cont_lemmas1; -val cont_tac = (fn i => (resolve_tac cont_lemmas i)); +(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*) -val cont_tacR = (fn i => (REPEAT (cont_tac i))); +(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*) (* ------------------------------------------------------------------------ *) (* function application _[_] is strict in its first arguments *) @@ -211,7 +213,7 @@ (stac inst_cfun_pcpo 1), (rewtac UU_cfun_def), (stac beta_cfun 1), - (cont_tac 1), + (Simp_tac 1), (rtac refl 1) ]); @@ -350,29 +352,20 @@ (monofun_Istrictify2 RS monocontlub2cont)); -qed_goalw "strictify1" Cfun3.thy [strictify_def] - "strictify`f`UU=UU" - (fn prems => - [ +qed_goalw "strictify1" Cfun3.thy [strictify_def] "strictify`f`UU=UU" (fn _ => [ (stac beta_cfun 1), - (cont_tac 1), - (rtac cont_Istrictify2 1), - (rtac cont2cont_CF1L 1), - (rtac cont_Istrictify1 1), + (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1, + cont2cont_CF1L]) 1), (stac beta_cfun 1), (rtac cont_Istrictify2 1), (rtac Istrictify1 1) ]); qed_goalw "strictify2" Cfun3.thy [strictify_def] - "~x=UU ==> strictify`f`x=f`x" - (fn prems => - [ + "~x=UU ==> strictify`f`x=f`x" (fn prems => [ (stac beta_cfun 1), - (cont_tac 1), - (rtac cont_Istrictify2 1), - (rtac cont2cont_CF1L 1), - (rtac cont_Istrictify1 1), + (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1, + cont2cont_CF1L]) 1), (stac beta_cfun 1), (rtac cont_Istrictify2 1), (rtac Istrictify2 1), @@ -391,4 +384,4 @@ (* use cont_tac as autotac. *) (* ------------------------------------------------------------------------ *) -simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac)); +(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*) diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Cprod3.ML --- a/src/HOLCF/Cprod3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Cprod3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -148,10 +148,7 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tac 1), - (rtac cont_pair2 1), - (rtac cont2cont_CF1L 1), - (rtac cont_pair1 1), + (simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1), (stac beta_cfun 1), (rtac cont_pair2 1), (rtac refl 1) @@ -299,7 +296,6 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tacR 1), (Simp_tac 1), (simp_tac (!simpset addsimps [cfst2,csnd2]) 1) ]); @@ -309,7 +305,7 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1) ]); diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Fix.ML Fri Jan 31 13:57:33 1997 +0100 @@ -398,8 +398,7 @@ (rtac (fixdef RS fix_eq4) 1), (rtac trans 1), (rtac beta_cfun 1), - (cont_tacR 1), - (rtac refl 1) + (Simp_tac 1) ]); (* use this one for definitions! *) @@ -411,7 +410,7 @@ (rtac (fix_eq2) 1), (rtac fixdef 1), (rtac beta_cfun 1), - (cont_tacR 1) + (Simp_tac 1) ]); (* ------------------------------------------------------------------------ *) @@ -1323,6 +1322,8 @@ etac adm_disj 1, atac 1]); -val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, +val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less, adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less]; +Addsimps adm_lemmas; + diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Lift3.ML --- a/src/HOLCF/Lift3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Lift3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -224,17 +224,18 @@ val cont2cont_CF1L_rev2 = (allI RS cont2cont_CF1L_rev); -val cont_lemmas = cont_lemmas@ +val cont_lemmas2 = cont_lemmas1@ [cont_flift1_arg,cont_flift2_arg, cont_flift1_not_arg2,cont2cont_CF1L_rev2, cont_fapp_app1,cont_fapp_app2,cont_if]; +Addsimps [cont_flift1_arg,cont_flift2_arg, + cont_flift1_not_arg2,cont2cont_CF1L_rev2, + cont_fapp_app1,cont_fapp_app2,cont_if]; -val cont_tac = (fn i => ((resolve_tac cont_lemmas i))); - -val cont_tacR = (fn i => ((simp_tac (!simpset - addsimps [flift1_def,flift2_def]) i) - THEN REPEAT (cont_tac i) )); +fun cont_tac i = resolve_tac cont_lemmas2 i; +fun cont_tacR i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN + REPEAT (cont_tac i); (* --------------------------------------------------------- *) (* Admissibility tactic and tricks *) @@ -253,10 +254,10 @@ val adm_tricks = [adm_trick_1,adm_trick_2]; -val adm_tac = (fn i => ((resolve_tac adm_thms i))); -val adm_tacR = (fn i => (REPEAT (adm_tac i))); -val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i))); +(*val adm_tac = (fn i => ((resolve_tac adm_lemmas i)));*) +(*val adm_tacR = (fn i => (REPEAT (adm_tac i)));*) +(*val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));*) (* ----------------------------------------------------------------- *) (* Relations between domains and terms using lift constructs *) @@ -308,9 +309,6 @@ goal Lift3.thy "plift P`(Def y) = blift (P y)"; by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1); -by (stac beta_cfun 1); -by (cont_tacR 1); -by (Simp_tac 1); qed"plift2blift"; goal Lift3.thy diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Sprod3.ML --- a/src/HOLCF/Sprod3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Sprod3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -320,10 +320,8 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tac 1), - (rtac cont_Ispair2 1), - (rtac cont2cont_CF1L 1), - (rtac cont_Ispair1 1), + (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1, + cont2cont_CF1L]) 1), (stac beta_cfun 1), (rtac cont_Ispair2 1), (rtac refl 1) @@ -624,7 +622,7 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (stac strictify1 1), (rtac refl 1) ]); @@ -634,13 +632,13 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (stac strictify2 1), (rtac defined_spair 1), (resolve_tac prems 1), (resolve_tac prems 1), (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (stac sfst2 1), (resolve_tac prems 1), (stac ssnd2 1), @@ -654,7 +652,7 @@ (fn prems => [ (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (case_tac "z=UU" 1), (hyp_subst_tac 1), (rtac strictify1 1), @@ -662,7 +660,7 @@ (rtac strictify2 1), (atac 1), (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (rtac surjective_pairing_Sprod2 1) ]); diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Ssum3.ML --- a/src/HOLCF/Ssum3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Ssum3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -486,101 +486,78 @@ ]); qed_goalw "sswhen1" Ssum3.thy [sswhen_def,sinl_def,sinr_def] - "sswhen`f`g`UU = UU" - (fn prems => - [ + "sswhen`f`g`UU = UU" (fn _ => let +val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2, + cont_Iwhen3,cont2cont_CF1L]) 1)) in + [ (stac inst_ssum_pcpo 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont2cont_CF1L]) 1)), + tac, + (stac beta_cfun 1), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont2cont_CF1L]) 1)), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont2cont_CF1L]) 1)), + tac, (simp_tac Ssum0_ss 1) - ]); + ] end); + + +val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2, + cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)); qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def] - "x~=UU==> sswhen`f`g`(sinl`x) = f`x" - (fn prems => - [ + "x~=UU==> sswhen`f`g`(sinl`x) = f`x" (fn prems => [ (cut_facts_tac prems 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (asm_simp_tac Ssum0_ss 1) ]); - - qed_goalw "sswhen3" Ssum3.thy [sswhen_def,sinl_def,sinr_def] - "x~=UU==> sswhen`f`g`(sinr`x) = g`x" - (fn prems => - [ + "x~=UU==> sswhen`f`g`(sinr`x) = g`x" (fn prems => [ (cut_facts_tac prems 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (asm_simp_tac Ssum0_ss 1) ]); qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def] - "(sinl`x << sinl`y) = (x << y)" - (fn prems => - [ + "(sinl`x << sinl`y) = (x << y)" (fn prems => [ (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac less_ssum3a 1) ]); qed_goalw "less_ssum4b" Ssum3.thy [sinl_def,sinr_def] - "(sinr`x << sinr`y) = (x << y)" - (fn prems => - [ + "(sinr`x << sinr`y) = (x << y)" (fn prems => [ (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac less_ssum3b 1) ]); qed_goalw "less_ssum4c" Ssum3.thy [sinl_def,sinr_def] - "(sinl`x << sinr`y) = (x = UU)" - (fn prems => + "(sinl`x << sinr`y) = (x = UU)" (fn prems => [ (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac less_ssum3c 1) ]); @@ -589,11 +566,9 @@ (fn prems => [ (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac less_ssum3d 1) ]); @@ -614,13 +589,13 @@ [ (cut_facts_tac prems 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac (beta_cfun RS ext) 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac thelub_ssum1a 1), (atac 1), (rtac allI 1), @@ -639,17 +614,13 @@ [ (cut_facts_tac prems 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (stac (beta_cfun RS ext) 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, - cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), + tac, (rtac thelub_ssum1b 1), (atac 1), (rtac allI 1), diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/Up3.ML --- a/src/HOLCF/Up3.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/Up3.ML Fri Jan 31 13:57:33 1997 +0100 @@ -181,17 +181,17 @@ (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1) ]); +val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1); qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU" (fn prems => [ (stac inst_up_pcpo 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), + tac, (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) ]); @@ -201,8 +201,7 @@ (stac beta_cfun 1), (rtac cont_Iup 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), (rtac cont_Ifup2 1), (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) @@ -230,15 +229,11 @@ [ (cut_facts_tac prems 1), (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), + tac, (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), - + tac, (stac (beta_cfun RS ext) 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, - cont_Ifup2,cont2cont_CF1L]) 1)), + tac, (rtac thelub_up1a 1), (atac 1), (etac exE 1), diff -r 64e52912eb09 -r cbf02fc74332 src/HOLCF/ccc1.ML --- a/src/HOLCF/ccc1.ML Wed Jan 29 15:58:17 1997 +0100 +++ b/src/HOLCF/ccc1.ML Fri Jan 31 13:57:33 1997 +0100 @@ -22,23 +22,19 @@ (rtac refl 1) ]); -qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" - (fn prems => - [ +qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [ (stac beta_cfun 1), - (cont_tacR 1), + (Simp_tac 1), (stac beta_cfun 1), - (cont_tacR 1), - (rtac refl 1) + (Simp_tac 1), + (rtac refl 1) ]); -qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)" - (fn prems => - [ +qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)" (fn _ => [ (stac cfcomp1 1), (stac beta_cfun 1), - (cont_tacR 1), - (rtac refl 1) + (Simp_tac 1), + (rtac refl 1) ]);