--- 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;
--- 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";
--- 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";
--- 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
--- 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";
-
--- 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
- ]);
--- 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";
--- 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
--- 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*)
--- 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";
--- 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
--- 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
--- 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";
--- 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;
--- 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";
--- 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;
--- 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;
--- 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";
--- 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];
--- 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";
--- 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";
-
--- 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;
--- 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)
--- 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));