# HG changeset patch # User wenzelm # Date 1149271979 -7200 # Node ID 372065f34795551e788f69902aa2a9feafd6b6f3 # Parent ec18656a2c102c07b9e478d3139512dab3b16c49 removed obsolete ML files; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Cfun.ML --- a/src/HOLCF/Cfun.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ - -(* legacy ML bindings *) - -val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; -val adm_cont = thm "adm_cont"; -val assoc_oo = thm "assoc_oo"; -val beta_cfun = thm "beta_cfun"; -val cfcomp1 = thm "cfcomp1"; -val cfcomp2 = thm "cfcomp2"; -val cfun_arg_cong = thm "cfun_arg_cong"; -val cfun_cong = thm "cfun_cong"; -val cfun_fun_cong = thm "cfun_fun_cong"; -val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; -val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; -val ch2ch_Rep_CFun = thm "ch2ch_Rep_CFun"; -val chain_monofun = thm "chain_monofun"; -val chfin2chfin = thm "chfin2chfin"; -val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; -val cont2cont_LAM = thm "cont2cont_LAM"; -val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; -val cont2mono_LAM = thm "cont2mono_LAM"; -val cont_cfun_arg = thm "cont_cfun_arg"; -val cont_cfun_fun = thm "cont_cfun_fun"; -val cont_cfun = thm "cont_cfun"; -val cont_strictify1 = thm "cont_strictify1"; -val cont_strictify2 = thm "cont_strictify2"; -val cont_lemmas1 = thms "cont_lemmas1"; -val contlub_cfun_arg = thm "contlub_cfun_arg"; -val contlub_cfun_fun = thm "contlub_cfun_fun"; -val cont_lub_cfun = thm "cont_lub_cfun"; -val contlub_cfun = thm "contlub_cfun"; -val contlub_strictify2 = thm "contlub_strictify2"; -val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; -val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; -val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; -val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; -val eta_cfun = thm "eta_cfun"; -val ex_lub_cfun = thm "ex_lub_cfun"; -val ext_cfun = thm "ext_cfun"; -val flat2flat = thm "flat2flat"; -val flat_codom = thm "flat_codom"; -val flat_eqI = thm "flat_eqI"; -val ID1 = thm "ID1"; -val ID2 = thm "ID2"; -val ID3 = thm "ID3"; -val ID_def = thm "ID_def"; -val injection_defined_rev = thm "injection_defined_rev"; -val injection_defined = thm "injection_defined"; -val injection_eq = thm "injection_eq"; -val injection_less = thm "injection_less"; -val inst_cfun_pcpo = thm "inst_cfun_pcpo"; -val less_cfun_def = thm "less_CFun_def"; -val less_cfun_ext = thm "less_cfun_ext"; -val lub_cfun_mono = thm "lub_cfun_mono"; -val lub_cfun = thm "lub_cfun"; -val monofun_cfun_arg = thm "monofun_cfun_arg"; -val monofun_cfun_fun = thm "monofun_cfun_fun"; -val monofun_cfun = thm "monofun_cfun"; -val monofun_strictify2 = thm "monofun_strictify2"; -val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; -val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; -val oo_def = thm "oo_def"; -val Rep_CFun_strict1 = thm "Rep_CFun_strict1"; -val retraction_strict = thm "retraction_strict"; -val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; -val strictify1 = thm "strictify1"; -val strictify2 = thm "strictify2"; -val strictify_conv_if = thm "strictify_conv_if"; -val strictify_def = thm "strictify_def"; -val strictI = thm "strictI"; -val thelub_cfun = thm "thelub_cfun"; -val UU_CFun = thm "UU_CFun"; - -structure Cfun = -struct - val thy = the_context (); - val strictify_def = strictify_def; - val ID_def = ID_def; - val oo_def = oo_def; -end; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Cont.ML --- a/src/HOLCF/Cont.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ - -(* legacy ML bindings *) - -val binchain_cont = thm "binchain_cont"; -val ch2ch_cont = thm "ch2ch_cont"; -val ch2ch_monofun = thm "ch2ch_monofun"; -val chfindom_monofun2cont = thm "chfindom_monofun2cont"; -val cont2cont_app2 = thm "cont2cont_app2"; -val cont2cont_app3 = thm "cont2cont_app3"; -val cont2cont_app = thm "cont2cont_app"; -val cont2cont_fun = thm "cont2cont_fun"; -val cont2cont_lambda = thm "cont2cont_lambda"; -val cont2contlub_app = thm "cont2contlub_app"; -val cont2contlubE = thm "cont2contlubE"; -val cont2cont_lub = thm "cont2cont_lub"; -val cont2contlub = thm "cont2contlub"; -val cont2mono = thm "cont2mono"; -val cont_const = thm "cont_const"; -val cont_def = thm "cont_def"; -val contE = thm "contE"; -val cont_finch2finch = thm "cont_finch2finch"; -val cont_id = thm "cont_id"; -val cont_if = thm "cont_if"; -val contI = thm "contI"; -val contlub_abstraction = thm "contlub_abstraction"; -val contlub_def = thm "contlub_def"; -val contlubE = thm "contlubE"; -val contlubI = thm "contlubI"; -val contlub_lub_fun = thm "contlub_lub_fun"; -val flatdom_strict2cont = thm "flatdom_strict2cont"; -val flatdom_strict2mono = thm "flatdom_strict2mono"; -val mono2mono_app = thm "mono2mono_app"; -val mono2mono_fun = thm "mono2mono_fun"; -val mono2mono_lambda = thm "mono2mono_lambda"; -val monocontlub2cont = thm "monocontlub2cont"; -val monofun_def = thm "monofun_def"; -val monofunE = thm "monofunE"; -val monofun_finch2finch = thm "monofun_finch2finch"; -val monofun_fun_arg = thm "monofun_fun_arg"; -val monofun_fun_fun = thm "monofun_fun_fun"; -val monofun_fun = thm "monofun_fun"; -val monofunI = thm "monofunI"; -val monofun_lub_fun = thm "monofun_lub_fun"; -val ub2ub_monofun = thm "ub2ub_monofun"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Cprod.ML --- a/src/HOLCF/Cprod.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ - -(* legacy ML bindings *) - -val antisym_less_cprod = thm "antisym_less_cprod"; -val cfst_cpair = thm "cfst_cpair"; -val cfst_def = thm "cfst_def"; -val cfst_strict = thm "cfst_strict"; -val CLet_def = thm "CLet_def"; -val compact_cpair = thm "compact_cpair"; -val cont_fst = thm "cont_fst"; -val contlub_fst = thm "contlub_fst"; -val contlub_pair1 = thm "contlub_pair1"; -val contlub_pair2 = thm "contlub_pair2"; -val contlub_snd = thm "contlub_snd"; -val cont_pair1 = thm "cont_pair1"; -val cont_pair2 = thm "cont_pair2"; -val cont_snd = thm "cont_snd"; -val cpair_def = thm "cpair_def"; -val cpair_defined_iff = thm "cpair_defined_iff"; -val cpair_eq_pair = thm "cpair_eq_pair"; -val cpair_eq = thm "cpair_eq"; -val cpair_less = thm "cpair_less"; -val cpo_cprod = thm "cpo_cprod"; -val cprodE = thm "cprodE"; -val Cprod_rews = thms "Cprod_rews"; -val csnd_cpair = thm "csnd_cpair"; -val csnd_def = thm "csnd_def"; -val csnd_strict = thm "csnd_strict"; -val csplit2 = thm "csplit2"; -val csplit3 = thm "csplit3"; -val csplit_def = thm "csplit_def"; -val defined_cpair_rev = thm "defined_cpair_rev"; -val eq_cprod = thm "eq_cprod"; -val Exh_Cprod2 = thm "Exh_Cprod2"; (* rename *) -val inject_cpair = thm "inject_cpair"; -val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; (**) -val inst_cprod_pcpo = thm "inst_cprod_pcpo"; -val least_cprod = thm "least_cprod"; -val less_cprod_def = thm "less_cprod_def"; -val less_cprod = thm "less_cprod"; -val lub_cprod2 = thm "lub_cprod2"; (* *) -val lub_cprod = thm "lub_cprod"; -val minimal_cprod = thm "minimal_cprod"; -val monofun_fst = thm "monofun_fst"; -val monofun_pair1 = thm "monofun_pair1"; -val monofun_pair2 = thm "monofun_pair2"; -val monofun_pair = thm "monofun_pair"; -val monofun_snd = thm "monofun_snd"; -val refl_less_cprod = thm "refl_less_cprod"; -val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; (* rename *) -val thelub_cprod2 = thm "thelub_cprod2"; (* *) -val thelub_cprod = thm "thelub_cprod"; -val trans_less_cprod = thm "trans_less_cprod"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Fri Jun 02 20:12:59 2006 +0200 @@ -161,12 +161,12 @@ lemma slen_fscons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" apply (simp add: fscons_def2 slen_scons_eq_rev) -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") -apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) apply (erule contrapos_np) apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) done diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Ffun.ML --- a/src/HOLCF/Ffun.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ - -(* legacy ML bindings *) - -val antisym_less_fun = thm "antisym_less_fun"; -val app_strict = thm "app_strict"; -val ch2ch_fun = thm "ch2ch_fun"; -val ch2ch_lambda = thm "ch2ch_lambda"; -val cpo_fun = thm "cpo_fun"; -val expand_fun_less = thm "expand_fun_less"; -val inst_fun_pcpo = thm "inst_fun_pcpo"; -val least_fun = thm "least_fun"; -val less_fun_def = thm "less_fun_def"; -val less_fun_ext = thm "less_fun_ext"; -val lub_fun = thm "lub_fun"; -val minimal_fun = thm "minimal_fun"; -val refl_less_fun = thm "refl_less_fun"; -val thelub_fun = thm "thelub_fun"; -val trans_less_fun = thm "trans_less_fun"; -val ub2ub_fun = thm "ub2ub_fun"; - diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,67 +0,0 @@ - -(* legacy ML bindings *) - -val adm_chfindom = thm "adm_chfindom"; -val adm_impl_admw = thm "adm_impl_admw"; -val admw_def = thm "admw_def"; -val chain_iterate2 = thm "chain_iterate2"; -val chain_iterate = thm "chain_iterate"; -val def_fix_ind = thm "def_fix_ind"; -val def_wfix_ind = thm "def_wfix_ind"; -val fix_const = thm "fix_const"; -val fix_def2 = thm "fix_def2"; -val fix_defined = thm "fix_defined"; -val fix_defined_iff = thm "fix_defined_iff"; -val fix_def = thm "fix_def"; -val fix_eq2 = thm "fix_eq2"; -val fix_eq3 = thm "fix_eq3"; -val fix_eq4 = thm "fix_eq4"; -val fix_eq5 = thm "fix_eq5"; -val fix_eqI = thm "fix_eqI"; -val fix_eq = thm "fix_eq"; -val fix_id = thm "fix_id"; -val fix_ind = thm "fix_ind"; -val fix_least = thm "fix_least"; -val fix_strict = thm "fix_strict"; -val iterate_0 = thm "iterate_0"; -val iterate_Suc2 = thm "iterate_Suc2"; -val iterate_Suc = thm "iterate_Suc"; -val wfix_ind = thm "wfix_ind"; - -structure Fix = -struct - val thy = the_context (); - val fix_def = fix_def; - val adm_def = adm_def; - val admw_def = admw_def; -end; - -fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); - -fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); - -(* proves the unfolding theorem for function equations f = fix$... *) -fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [ - (rtac trans 1), - (rtac (fixeq RS fix_eq4) 1), - (rtac trans 1), - (rtac beta_cfun 1), - (Simp_tac 1) - ]); - -(* proves the unfolding theorem for function definitions f == fix$... *) -fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [ - (rtac trans 1), - (rtac (fix_eq2) 1), - (rtac fixdef 1), - (rtac beta_cfun 1), - (Simp_tac 1) - ]); - -(* proves an application case for a function from its unfolding thm *) -fun case_prover thy unfold s = prove_goal thy s (fn prems => [ - (cut_facts_tac prems 1), - (rtac trans 1), - (stac unfold 1), - Auto_tac - ]); diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IOA/Modelcheck/Cockpit.ML --- a/src/HOLCF/IOA/Modelcheck/Cockpit.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ - -val aut_simps = [cockpit_def,cockpit_asig_def,cockpit_trans_def, - cockpit_initial_def,cockpit_hide_def, - Al_before_Ack_def,Al_before_Ack_asig_def, - Al_before_Ack_initial_def,Al_before_Ack_trans_def, - Info_while_Al_def,Info_while_Al_asig_def, - Info_while_Al_initial_def,Info_while_Al_trans_def, - Info_before_Al_def,Info_before_Al_asig_def, - Info_before_Al_initial_def,Info_before_Al_trans_def]; - - -(* to prove, that info is always set at the recent alarm *) -Goal "cockpit =<| Info_while_Al"; -by (is_sim_tac aut_simps 1); -qed"cockpit_implements_Info_while_Al"; - -(* to prove that before any alarm arrives (and after each acknowledgment), - info remains at None *) -Goal "cockpit =<| Info_before_Al"; -by (is_sim_tac aut_simps 1); -qed"cockpit_implements_Info_before_Al"; - -(* to prove that before any alarm would be acknowledged, it must be arrived *) -Goal "cockpit_hide =<| Al_before_Ack"; -by (is_sim_tac aut_simps 1); -by Auto_tac; -qed"cockpit_implements_Al_before_Ack"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IOA/Modelcheck/Cockpit.thy --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Jun 02 20:12:59 2006 +0200 @@ -89,6 +89,32 @@ "Ack a" post info_at_NONE:="True" -ML {* use_legacy_bindings (the_context ()) *} +lemmas aut_simps = + cockpit_def cockpit_asig_def cockpit_trans_def + cockpit_initial_def cockpit_hide_def + Al_before_Ack_def Al_before_Ack_asig_def + Al_before_Ack_initial_def Al_before_Ack_trans_def + Info_while_Al_def Info_while_Al_asig_def + Info_while_Al_initial_def Info_while_Al_trans_def + Info_before_Al_def Info_before_Al_asig_def + Info_before_Al_initial_def Info_before_Al_trans_def + + +(* to prove, that info is always set at the recent alarm *) +lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al" +apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +done + +(* to prove that before any alarm arrives (and after each acknowledgment), + info remains at None *) +lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al" +apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +done + +(* to prove that before any alarm would be acknowledged, it must be arrived *) +lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack" +apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply auto +done end diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IOA/Modelcheck/ROOT.ML --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Fri Jun 02 20:12:59 2006 +0200 @@ -5,9 +5,6 @@ Modelchecker setup for I/O automata. *) -goals_limit := 1; - -use "../../../HOL/Modelcheck/mucke_oracle.ML"; with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle"; (*examples*) diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IOA/Modelcheck/Ring3.ML --- a/src/HOLCF/IOA/Modelcheck/Ring3.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ - -val aut_simps = [Greater_def,one_leader_def, - one_leader_asig_def,one_leader_trans_def,one_leader_initial_def, - ring_def,aut0_asig_def,aut0_trans_def,aut0_initial_def,aut0_def, - aut1_asig_def,aut1_trans_def,aut1_initial_def,aut1_def, - aut2_asig_def,aut2_trans_def,aut2_initial_def,aut2_def]; - -(* property to prove: at most one (of 3) members of the ring will - declare itself to leader *) -Goal "ring =<| one_leader"; -by (is_sim_tac aut_simps 1); -by Auto_tac; -qed"at_most_one_leader"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IOA/Modelcheck/Ring3.thy --- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Fri Jun 02 20:12:59 2006 +0200 @@ -104,6 +104,18 @@ pre "leader=id2 | leader=Leader" post leader:="id2" -ML {* use_legacy_bindings (the_context ()) *} +lemmas aut_simps = + Greater_def one_leader_def + one_leader_asig_def one_leader_trans_def one_leader_initial_def + ring_def aut0_asig_def aut0_trans_def aut0_initial_def aut0_def + aut1_asig_def aut1_trans_def aut1_initial_def aut1_def + aut2_asig_def aut2_trans_def aut2_initial_def aut2_def + +(* property to prove: at most one (of 3) members of the ring will + declare itself to leader *) +lemma at_most_one_leader: "ring =<| one_leader" +apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply auto +done end diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/IsaMakefile Fri Jun 02 20:12:59 2006 +0200 @@ -27,11 +27,11 @@ HOL: @cd $(SRC)/HOL; $(ISATOOL) make HOL -$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.ML Cfun.thy Cont.ML Cont.thy \ - Cprod.ML Cprod.thy Discrete.thy Domain.thy Fix.ML Fix.thy Fixrec.thy \ - Ffun.ML Ffun.thy HOLCF.ML HOLCF.thy Lift.ML Lift.thy One.ML One.thy \ - Pcpo.ML Pcpo.thy Porder.ML Porder.thy ROOT.ML Sprod.ML Sprod.thy \ - Ssum.ML Ssum.thy Tr.ML Tr.thy Up.ML Pcpodef.thy pcpodef_package.ML \ +$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy \ + Cprod.thy Discrete.thy Domain.thy Fix.thy Fixrec.thy \ + Ffun.thy HOLCF.ML HOLCF.thy Lift.thy One.thy \ + Pcpo.thy Porder.thy ROOT.ML Sprod.thy \ + Ssum.thy Tr.thy Pcpodef.thy pcpodef_package.ML \ Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \ domain/axioms.ML domain/extender.ML domain/library.ML \ domain/syntax.ML domain/theorems.ML holcf_logic.ML ex/Stream.thy \ @@ -115,10 +115,10 @@ IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz -$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML IOA/Modelcheck/Cockpit.ML\ +$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.ML IOA/Modelcheck/MuIOA.thy \ IOA/Modelcheck/MuIOAOracle.ML IOA/Modelcheck/MuIOAOracle.thy \ - IOA/Modelcheck/Ring3.ML IOA/Modelcheck/Ring3.thy + IOA/Modelcheck/Ring3.thy @cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ - -(* legacy ML bindings *) - -structure lift = -struct - val distinct = thms "lift.distinct"; - val inject = thms "lift.inject"; - val exhaust = thm "lift.exhaust"; - val cases = thms "lift.cases"; - val split = thm "lift.split"; - val split_asm = thm "lift.split_asm"; - val induct = thm "lift.induct"; - val recs = thms "lift.recs"; - val simps = thms "lift.simps"; - val size = thms "lift.size"; -end; - -val cont2cont_flift1 = thm "cont2cont_flift1"; -val cont2cont_lift_case = thm "cont2cont_lift_case"; -val cont_flift1 = thm "cont_flift1"; -val cont_lemmas_ext = thms "cont_lemmas_ext"; -val cont_lift_case1 = thm "cont_lift_case1"; -val cont_lift_case2 = thm "cont_lift_case2"; -val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; -val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; -val DefE2 = thm "DefE2"; -val DefE = thm "DefE"; -val Def_inject_less_eq = thm "Def_inject_less_eq"; -val Def_inject = thm "Def_inject"; -val Def_less_is_eq = thm "Def_less_is_eq"; -val Def_not_UU = thm "Def_not_UU"; -val flift1_def = thm "flift1_def"; -val flift1_Def = thm "flift1_Def"; -val flift1_strict = thm "flift1_strict"; -val flift2_defined = thm "flift2_defined"; -val flift2_def = thm "flift2_def"; -val flift2_Def = thm "flift2_Def"; -val flift2_strict = thm "flift2_strict"; -val inst_lift_pcpo = thm "inst_lift_pcpo"; -val less_lift_def = thm "less_lift_def"; -val less_lift = thm "less_lift"; -val Lift_cases = thm "Lift_cases"; -val lift_definedE = thm "lift_definedE"; -val lift_distinct1 = thm "lift_distinct1"; -val lift_distinct2 = thm "lift_distinct2"; -val Lift_exhaust = thm "Lift_exhaust"; -val lift_induct = thm "lift_induct"; -val liftpair_def = thm "liftpair_def"; -val not_Undef_is_Def = thm "not_Undef_is_Def"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/Lift.thy Fri Jun 02 20:12:59 2006 +0200 @@ -185,13 +185,15 @@ cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if ML {* -val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; +local + val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext"; + val flift1_def = thm "flift1_def"; +in fun cont_tac i = resolve_tac cont_lemmas2 i; fun cont_tacR i = REPEAT (cont_tac i); -local val flift1_def = thm "flift1_def" -in fun cont_tacRs ss i = +fun cont_tacRs ss i = simp_tac ss i THEN REPEAT (cont_tac i) end; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/One.ML --- a/src/HOLCF/One.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ - -(* legacy ML bindings *) - -val compact_ONE = thm "compact_ONE"; -val dist_eq_one = thms "dist_eq_one"; -val dist_less_one = thm "dist_less_one"; -val Exh_one = thm "Exh_one"; -val oneE = thm "oneE"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ - -(* legacy ML bindings *) - -val ax_flat = thm "ax_flat"; -val ch2ch_lub = thm "ch2ch_lub"; -val chain_mono2 = thm "chain_mono2"; -val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2"; -val chain_UU_I_inverse = thm "chain_UU_I_inverse"; -val chain_UU_I = thm "chain_UU_I"; -val chfin2finch = thm "chfin2finch"; -val chfin_imp_cpo = thm "chfin_imp_cpo"; -val chfin = thm "chfin"; -val cpo = thm "cpo"; -val diag_lub = thm "diag_lub"; -val eq_UU_iff = thm "eq_UU_iff"; -val ex_lub = thm "ex_lub"; -val flat_eq = thm "flat_eq"; -val flat_imp_chfin = thm "flat_imp_chfin"; -val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma"; -val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma"; -val is_lub_thelub = thm "is_lub_thelub"; -val is_ub_thelub = thm "is_ub_thelub"; -val least = thm "least"; -val lub_equal2 = thm "lub_equal2"; -val lub_equal = thm "lub_equal"; -val lub_mono2 = thm "lub_mono2"; -val lub_mono3 = thm "lub_mono3"; -val lub_mono = thm "lub_mono"; -val lub_range_shift = thm "lub_range_shift"; -val maxinch_is_thelub = thm "maxinch_is_thelub"; -val minimal = thm "minimal"; -val not_less2not_eq = thm "not_less2not_eq"; -val notUU_I = thm "notUU_I"; -val thelubE = thm "thelubE"; -val UU_def = thm "UU_def"; -val UU_I = thm "UU_I"; -val UU_least = thm "UU_least"; -val UU_reorient = thm "UU_reorient"; - -structure Pcpo = -struct - val thy = the_context (); - val UU_def = UU_def; -end; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Porder.ML --- a/src/HOLCF/Porder.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,56 +0,0 @@ - -(* legacy ML bindings *) - -val antisym_less_inverse = thm "antisym_less_inverse"; -val antisym_less = thm "antisym_less"; -val bin_chainmax = thm "bin_chainmax"; -val bin_chain = thm "bin_chain"; -val box_less = thm "box_less"; -val chain_def = thm "chain_def"; -val chainE = thm "chainE"; -val chainI = thm "chainI"; -val chain_const = thm "chain_const"; -val chain_mono3 = thm "chain_mono3"; -val chain_mono = thm "chain_mono"; -val chain_shift = thm "chain_shift"; -val chain_tord = thm "chain_tord"; -val finite_chain_def = thm "finite_chain_def"; -val is_lubD1 = thm "is_lubD1"; -val is_lub_def = thm "is_lub_def"; -val is_lubI = thm "is_lubI"; -val is_lub_lub = thm "is_lub_lub"; -val is_lub_range_shift = thm "is_lub_range_shift"; -val is_ub_def = thm "is_ub_def"; -val is_ub_lub = thm "is_ub_lub"; -val is_ub_range_shift = thm "is_ub_range_shift"; -val lub_bin_chain = thm "lub_bin_chain"; -val lub_chain_maxelem = thm "lub_chain_maxelem"; -val lub_const = thm "lub_const"; -val lub_def = thm "lub_def"; -val lub_finch1 = thm "lub_finch1"; -val lub_finch2 = thm "lub_finch2"; -val lubI = thm "lubI"; -val lub_singleton = thm "lub_singleton"; -val lub = thm "lub"; -val max_in_chain_def = thm "max_in_chain_def"; -val minimal2UU = thm "minimal2UU"; -val po_eq_conv = thm "po_eq_conv"; -val refl_less = thm "refl_less"; -val thelubI = thm "thelubI"; -val tord_def = thm "tord_def"; -val trans_less = thm "trans_less"; -val ub_rangeD = thm "ub_rangeD"; -val ub_rangeI = thm "ub_rangeI"; -val unique_lub = thm "unique_lub"; - -structure Porder = -struct - val thy = the_context (); - val is_ub_def = is_ub_def; - val is_lub_def = is_lub_def; - val tord_def = tord_def; - val chain_def = chain_def; - val max_in_chain_def = max_in_chain_def; - val finite_chain_def = finite_chain_def; - val lub_def = lub_def; -end; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Sprod.ML --- a/src/HOLCF/Sprod.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ - -(* legacy ML bindings *) - -val compact_spair = thm "compact_spair"; -val eq_sprod = thm "eq_sprod"; -val Exh_Sprod2 = thm "Exh_Sprod2"; (* *) -val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *) -val less_sprod_def = thm "less_Sprod_def"; -val less_sprod = thm "less_sprod"; -val Rep_Sprod_spair = thm "Rep_Sprod_spair"; -val sfst_defined_iff = thm "sfst_defined_iff"; -val sfst_defined = thm "sfst_defined"; -val sfst_def = thm "sfst_def"; -val sfst_spair = thm "sfst_spair"; -val sfst_strict = thm "sfst_strict"; -val spair_Abs_Sprod = thm "spair_Abs_Sprod"; -val spair_defined_rev = thm "spair_defined_rev"; -val spair_defined = thm "spair_defined"; -val spair_def = thm "spair_def"; -val spair_eq = thm "spair_eq"; -val spair_inject = thm "spair_inject"; -val spair_lemma = thm "spair_lemma"; -val spair_less = thm "spair_less"; -val spair_strict1 = thm "spair_strict1"; -val spair_strict2 = thm "spair_strict2"; -val spair_strict_rev = thm "spair_strict_rev"; -val spair_strict = thm "spair_strict"; -val sprodE = thm "sprodE"; -val ssnd_defined_iff = thm "ssnd_defined_iff"; -val ssnd_defined = thm "ssnd_defined"; -val ssnd_def = thm "ssnd_def"; -val ssnd_spair = thm "ssnd_spair"; -val ssnd_strict = thm "ssnd_strict"; -val ssplit1 = thm "ssplit1"; -val ssplit2 = thm "ssplit2"; -val ssplit3 = thm "ssplit3"; -val ssplit_def = thm "ssplit_def"; -val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Ssum.ML --- a/src/HOLCF/Ssum.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ - -(* legacy ML bindings *) - -val beta_sscase = thm "beta_sscase"; -val compact_sinl = thm "compact_sinl"; -val compact_sinr = thm "compact_sinr"; -val cont_Iwhen1 = thm "cont_Iwhen1"; -val cont_Iwhen2 = thm "cont_Iwhen2"; -val cont_Iwhen3 = thm "cont_Iwhen3"; -val Exh_Ssum = thm "Exh_Ssum"; -val Iwhen1 = thm "Iwhen1"; -val Iwhen2 = thm "Iwhen2"; -val Iwhen3 = thm "Iwhen3"; -val Iwhen4 = thm "Iwhen4"; -val Iwhen5 = thm "Iwhen5"; -val Iwhen_def = thm "Iwhen_def"; -val less_sinlD = thm "less_sinlD"; -val less_sinrD = thm "less_sinrD"; -val less_ssum_def = thm "less_Ssum_def"; -val Rep_Ssum_sinl = thm "Rep_Ssum_sinl"; -val Rep_Ssum_sinr = thm "Rep_Ssum_sinr"; -val sinl_Abs_Ssum = thm "sinl_Abs_Ssum"; -val sinl_defined_iff = thm "sinl_defined_iff"; -val sinl_defined = thm "sinl_defined"; -val sinl_def = thm "sinl_def"; -val sinl_eq_sinr = thm "sinl_eq_sinr"; -val sinl_eq = thm "sinl_eq"; -val sinl_inject = thm "sinl_inject"; -val sinl_less_sinr = thm "sinl_less_sinr"; -val sinl_less = thm "sinl_less"; -val sinl_strict = thm "sinl_strict"; -val sinr_Abs_Ssum = thm "sinr_Abs_Ssum"; -val sinr_defined_iff = thm "sinr_defined_iff"; -val sinr_defined = thm "sinr_defined"; -val sinr_def = thm "sinr_def"; -val sinr_eq_sinl = thm "sinr_eq_sinl"; -val sinr_eq = thm "sinr_eq"; -val sinr_inject = thm "sinr_inject"; -val sinr_less_sinl = thm "sinr_less_sinl"; -val sinr_less = thm "sinr_less"; -val sinr_strict = thm "sinr_strict"; -val sscase1 = thm "sscase1"; -val sscase2 = thm "sscase2"; -val sscase3 = thm "sscase3"; -val sscase4 = thm "sscase4"; -val sscase_def = thm "sscase_def"; -val ssum_chain_lemma = thm "ssum_chain_lemma"; -val ssumE2 = thm "ssumE2"; -val ssumE = thm "ssumE"; -val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined, - sscase1, sscase2, sscase3]; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Tr.ML --- a/src/HOLCF/Tr.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ - -(* legacy ML bindings *) - -val andalso_and = thm "andalso_and"; -val andalso_def = thm "andalso_def"; -val andalso_or = thm "andalso_or"; -val andalso_thms = thms "andalso_thms"; -val compact_FF = thm "compact_FF"; -val compact_TT = thm "compact_TT"; -val Def_bool1 = thm "Def_bool1"; -val Def_bool2 = thm "Def_bool2"; -val Def_bool3 = thm "Def_bool3"; -val Def_bool4 = thm "Def_bool4"; -val dist_eq_tr = thms "dist_eq_tr"; -val dist_less_tr = thms "dist_less_tr"; -val Exh_tr = thm "Exh_tr"; -val FF_def = thm "FF_def"; -val If2_def = thm "If2_def"; -val If_and_if = thm "If_and_if"; -val ifte_def = thm "ifte_def"; -val ifte_thms = thms "ifte_thms"; -val neg_def = thm "neg_def"; -val neg_thms = thms "neg_thms"; -val orelse_def = thm "orelse_def"; -val orelse_thms = thms "orelse_thms"; -val split_If2 = thm "split_If2"; -val tr_defs = thms "tr_defs"; -val trE = thm "trE"; -val TT_def = thm "TT_def"; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/Up.ML --- a/src/HOLCF/Up.ML Fri Jun 02 19:41:37 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ - -(* legacy ML bindings *) - -val antisym_less_up = thm "antisym_less_up"; -val compact_up = thm "compact_up"; -val cont_Ifup1 = thm "cont_Ifup1"; -val cont_Ifup2 = thm "cont_Ifup2"; -val cont_Iup = thm "cont_Iup"; -val cpo_up = thm "cpo_up"; -val Exh_Up = thm "Exh_Up"; -val fup1 = thm "fup1"; -val fup2 = thm "fup2"; -val fup3 = thm "fup3"; -val fup_def = thm "fup_def"; -val inst_up_pcpo = thm "inst_up_pcpo"; -val is_lub_Iup = thm "is_lub_Iup"; -val Iup_less = thm "Iup_less"; -val least_up = thm "least_up"; -val less_up_def = thm "less_up_def"; -val minimal_up = thm "minimal_up"; -val monofun_Ifup2 = thm "monofun_Ifup2"; -val not_Iup_less = thm "not_Iup_less"; -val not_up_less_UU = thm "not_up_less_UU"; -val refl_less_up = thm "refl_less_up"; -val trans_less_up = thm "trans_less_up"; -val up_chain_cases = thm "up_chain_cases"; -val up_defined = thm "up_defined"; -val up_def = thm "up_def"; -val up_eq = thm "up_eq"; -val upE = thm "upE"; -val up_inject = thm "up_inject"; -val up_lemma1 = thm "up_lemma1"; -val up_lemma2 = thm "up_lemma2"; -val up_lemma3 = thm "up_lemma3"; -val up_lemma4 = thm "up_lemma4"; -val up_lemma5 = thm "up_lemma5"; -val up_lemma6 = thm "up_lemma6"; -val up_less = thm "up_less"; - diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/domain/theorems.ML Fri Jun 02 20:12:59 2006 +0200 @@ -12,6 +12,33 @@ local +val adm_impl_admw = thm "adm_impl_admw"; +val antisym_less_inverse = thm "antisym_less_inverse"; +val beta_cfun = thm "beta_cfun"; +val cfun_arg_cong = thm "cfun_arg_cong"; +val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; +val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; +val chain_iterate = thm "chain_iterate"; +val compact_ONE = thm "compact_ONE"; +val compact_sinl = thm "compact_sinl"; +val compact_sinr = thm "compact_sinr"; +val compact_spair = thm "compact_spair"; +val compact_up = thm "compact_up"; +val contlub_cfun_arg = thm "contlub_cfun_arg"; +val contlub_cfun_fun = thm "contlub_cfun_fun"; +val fix_def2 = thm "fix_def2"; +val injection_eq = thm "injection_eq"; +val injection_less = thm "injection_less"; +val lub_equal = thm "lub_equal"; +val monofun_cfun_arg = thm "monofun_cfun_arg"; +val retraction_strict = thm "retraction_strict"; +val spair_eq = thm "spair_eq"; +val spair_less = thm "spair_less"; +val sscase1 = thm "sscase1"; +val ssplit1 = thm "ssplit1"; +val strictify1 = thm "strictify1"; +val wfix_ind = thm "wfix_ind"; + open Domain_Library; infixr 0 ===>; infixr 0 ==>; @@ -603,7 +630,7 @@ (* ----- theorems concerning finite approximation and finite induction ------ *) local - val iterate_Cprod_ss = simpset_of Fix.thy; + val iterate_Cprod_ss = simpset_of (theory "Fix"); val copy_con_rews = copy_rews @ con_rews; val copy_take_defs = (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/ex/Dnat.thy --- a/src/HOLCF/ex/Dnat.thy Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/ex/Dnat.thy Fri Jun 02 20:12:59 2006 +0200 @@ -19,14 +19,16 @@ \medskip Expand fixed point properties. *} -ML_setup {* -bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def" RS eq_reflection) - "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"); -*} +lemma iterator_def2: + "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))" + apply (rule trans) + apply (rule fix_eq2) + apply (rule iterator_def [THEN eq_reflection]) + apply (rule beta_cfun) + apply simp + done -text {* - \medskip Recursive properties. -*} +text {* \medskip Recursive properties. *} lemma iterator1: "iterator $ UU $ f $ x = UU" apply (subst iterator_def2) diff -r ec18656a2c10 -r 372065f34795 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Fri Jun 02 19:41:37 2006 +0200 +++ b/src/HOLCF/fixrec_package.ML Fri Jun 02 20:12:59 2006 +0200 @@ -16,6 +16,10 @@ structure FixrecPackage: FIXREC_PACKAGE = struct +val fix_eq2 = thm "fix_eq2"; +val def_fix_ind = thm "def_fix_ind"; + + fun fixrec_err s = error ("fixrec definition error:\n" ^ s); fun fixrec_eq_err thy s eq = fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));