# HG changeset patch # User huffman # Date 1122395399 -7200 # Node ID 2128ac2aa5db6a025a6f4271459efc6ee726fcbb # Parent 16094ed8ac6bd0c67fd8082196fc79df9e218e9e brought ML files up to date with new lemmas diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Cfun.ML --- a/src/HOLCF/Cfun.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Cfun.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,74 +1,78 @@ (* legacy ML bindings *) -val less_cfun_def = thm "less_CFun_def"; +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 cfun_arg_cong = thm "cfun_arg_cong"; -val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; -val beta_cfun = thm "beta_cfun"; -val eta_cfun = thm "eta_cfun"; -val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; -val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; -val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; -val cont_cfun_arg = thm "cont_cfun_arg"; -val contlub_cfun_arg = thm "contlub_cfun_arg"; -val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; -val monofun_cfun_fun = thm "monofun_cfun_fun"; -val monofun_cfun_arg = thm "monofun_cfun_arg"; -val chain_monofun = thm "chain_monofun"; -val monofun_cfun = thm "monofun_cfun"; -val strictI = thm "strictI"; +val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; -val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; -val lub_cfun_mono = thm "lub_cfun_mono"; -val ex_lub_cfun = thm "ex_lub_cfun"; -val cont_lub_cfun = thm "cont_lub_cfun"; -val lub_cfun = thm "lub_cfun"; -val thelub_cfun = thm "thelub_cfun"; -val ext_cfun = thm "ext_cfun"; -val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; -val less_cfun_ext = thm "less_cfun_ext"; -val Istrictify_def = thm "Istrictify_def"; -val strictify_def = thm "strictify_def"; -val ID_def = thm "ID_def"; -val oo_def = thm "oo_def"; -val inst_cfun_pcpo = thm "inst_cfun_pcpo"; -val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; -val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; -val contlub_cfun_fun = thm "contlub_cfun_fun"; -val cont_cfun_fun = thm "cont_cfun_fun"; -val contlub_cfun = thm "contlub_cfun"; -val cont_cfun = thm "cont_cfun"; +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 cont2cont_LAM = thm "cont2cont_LAM"; -val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2, - cont2cont_Rep_CFun, cont2cont_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_Istrictify1 = thm "cont_Istrictify1"; +val cont_Istrictify2 = thm "cont_Istrictify2"; +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_Istrictify2 = thm "contlub_Istrictify2"; +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 Istrictify1 = thm "Istrictify1"; val Istrictify2 = thm "Istrictify2"; +val Istrictify_def = thm "Istrictify_def"; +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_Istrictify2 = thm "monofun_Istrictify2"; -val contlub_Istrictify2 = thm "contlub_Istrictify2"; -val cont_Istrictify1 = thm "cont_Istrictify1"; -val cont_Istrictify2 = thm "cont_Istrictify2"; +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 Rep_CFun_strict1 = thm "Rep_CFun_strict1"; -val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; -val retraction_strict = thm "retraction_strict"; -val injection_eq = thm "injection_eq"; -val injection_less = thm "injection_less"; -val injection_defined_rev = thm "injection_defined_rev"; -val injection_defined = thm "injection_defined"; -val chfin2chfin = thm "chfin2chfin"; -val flat2flat = thm "flat2flat"; -val flat_codom = thm "flat_codom"; -val ID1 = thm "ID1"; -val cfcomp1 = thm "cfcomp1"; -val cfcomp2 = thm "cfcomp2"; -val ID2 = thm "ID2"; -val ID3 = thm "ID3"; -val assoc_oo = thm "assoc_oo"; +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 diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Cont.ML --- a/src/HOLCF/Cont.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Cont.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,38 +1,45 @@ (* legacy ML bindings *) -val monofun_def = thm "monofun_def"; +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_CF1L_rev = thm "cont2cont_CF1L_rev"; +val cont2cont_CF1L = thm "cont2cont_CF1L"; +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 cont_def = thm "cont_def"; +val contlubE = thm "contlubE"; val contlubI = thm "contlubI"; -val contlubE = thm "contlubE"; -val contI = thm "contI"; -val contE = thm "contE"; -val monofunI = thm "monofunI"; +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_MF1L_rev = thm "mono2mono_MF1L_rev"; +val mono2mono_MF1L = thm "mono2mono_MF1L"; +val monocontlub2cont = thm "monocontlub2cont"; +val monofun_def = thm "monofun_def"; val monofunE = thm "monofunE"; -val ch2ch_monofun = thm "ch2ch_monofun"; -val ub2ub_monofun = thm "ub2ub_monofun"; -val monocontlub2cont = thm "monocontlub2cont"; -val binchain_cont = thm "binchain_cont"; -val cont2mono = thm "cont2mono"; -val cont2contlub = thm "cont2contlub"; val monofun_finch2finch = thm "monofun_finch2finch"; -val cont_finch2finch = thm "cont_finch2finch"; +val monofun_fun_arg = thm "monofun_fun_arg"; val monofun_fun_fun = thm "monofun_fun_fun"; -val monofun_fun_arg = thm "monofun_fun_arg"; -val mono2mono_MF1L = thm "mono2mono_MF1L"; -val cont2cont_CF1L = thm "cont2cont_CF1L"; -val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; -val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; -val cont2cont_lambda = thm "cont2cont_lambda"; -val contlub_abstraction = thm "contlub_abstraction"; -val mono2mono_app = thm "mono2mono_app"; -val cont2contlub_app = thm "cont2contlub_app"; -val cont2cont_app = thm "cont2cont_app"; -val cont2cont_app2 = thm "cont2cont_app2"; -val cont_id = thm "cont_id"; -val cont_const = thm "cont_const"; -val cont2cont_app3 = thm "cont2cont_app3"; -val chfindom_monofun2cont = thm "chfindom_monofun2cont"; -val flatdom_strict2mono = thm "flatdom_strict2mono"; -val flatdom_strict2cont = thm "flatdom_strict2cont"; +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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Cprod.ML --- a/src/HOLCF/Cprod.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Cprod.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,46 +1,52 @@ (* 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 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 refl_less_cprod = thm "refl_less_cprod"; -val antisym_less_cprod = thm "antisym_less_cprod"; -val trans_less_cprod = thm "trans_less_cprod"; +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 least_cprod = thm "least_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_fst = thm "monofun_fst"; val monofun_snd = thm "monofun_snd"; -val lub_cprod = thm "lub_cprod"; +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 cpo_cprod = thm "cpo_cprod"; -val cpair_def = thm "cpair_def"; -val cfst_def = thm "cfst_def"; -val csnd_def = thm "csnd_def"; -val csplit_def = thm "csplit_def"; -val CLet_def = thm "CLet_def"; -val inst_cprod_pcpo = thm "inst_cprod_pcpo"; -val contlub_pair1 = thm "contlub_pair1"; -val contlub_pair2 = thm "contlub_pair2"; -val cont_pair1 = thm "cont_pair1"; -val cont_pair2 = thm "cont_pair2"; -val contlub_fst = thm "contlub_fst"; -val contlub_snd = thm "contlub_snd"; -val cont_fst = thm "cont_fst"; -val cont_snd = thm "cont_snd"; -val inject_cpair = thm "inject_cpair"; -val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; -val defined_cpair_rev = thm "defined_cpair_rev"; -val Exh_Cprod2 = thm "Exh_Cprod2"; -val cprodE = thm "cprodE"; -val cfst_cpair = thm "cfst_cpair"; -val csnd_cpair = thm "csnd_cpair"; -val cfst_strict = thm "cfst_strict"; -val csnd_strict = thm "csnd_strict"; -val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; -val lub_cprod2 = thm "lub_cprod2"; -val thelub_cprod2 = thm "thelub_cprod2"; -val csplit2 = thm "csplit2"; -val csplit3 = thm "csplit3"; -val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2]; +val trans_less_cprod = thm "trans_less_cprod"; diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Ffun.ML --- a/src/HOLCF/Ffun.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Ffun.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,16 +1,20 @@ (* legacy ML bindings *) -val less_fun_def = thm "less_fun_def"; -val refl_less_fun = thm "refl_less_fun"; val antisym_less_fun = thm "antisym_less_fun"; -val trans_less_fun = thm "trans_less_fun"; -val minimal_fun = thm "minimal_fun"; -val least_fun = thm "least_fun"; -val less_fun = thm "less_fun"; +val app_strict = thm "app_strict"; val ch2ch_fun = thm "ch2ch_fun"; -val ub2ub_fun = thm "ub2ub_fun"; -val lub_fun = thm "lub_fun"; -val thelub_fun = thm "thelub_fun"; +val ch2ch_fun_rev = thm "ch2ch_fun_rev"; val cpo_fun = thm "cpo_fun"; 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 less_fun = thm "less_fun"; +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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Fix.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,36 +1,41 @@ (* legacy ML bindings *) -val iterate_0 = thm "iterate_0"; -val iterate_Suc = thm "iterate_Suc"; -val Ifix_def = thm "Ifix_def"; -val fix_def = thm "fix_def"; +val adm_chfindom = thm "adm_chfindom"; +val adm_impl_admw = thm "adm_impl_admw"; val admw_def = thm "admw_def"; -val iterate_Suc2 = thm "iterate_Suc2"; val chain_iterate2 = thm "chain_iterate2"; val chain_iterate = thm "chain_iterate"; -val Ifix_eq = thm "Ifix_eq"; -val Ifix_least = thm "Ifix_least"; +val cont_Ifix = thm "cont_Ifix"; val cont_iterate1 = thm "cont_iterate1"; val cont_iterate2 = thm "cont_iterate2"; -val monofun_iterate2 = thm "monofun_iterate2"; +val cont_iterate = thm "cont_iterate"; val contlub_iterate2 = thm "contlub_iterate2"; -val cont_iterate = thm "cont_iterate"; -val cont_Ifix = thm "cont_Ifix"; -val fix_eq = thm "fix_eq"; -val fix_least = thm "fix_least"; -val fix_eqI = thm "fix_eqI"; +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_def2 = thm "fix_def2"; -val def_fix_ind = thm "def_fix_ind"; -val adm_impl_admw = thm "adm_impl_admw"; +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 def_fix_ind = thm "def_fix_ind"; +val fix_least = thm "fix_least"; +val fix_strict = thm "fix_strict"; +val Ifix_def = thm "Ifix_def"; +val Ifix_eq = thm "Ifix_eq"; +val Ifix_least = thm "Ifix_least"; +val iterate_0 = thm "iterate_0"; +val iterate_Suc2 = thm "iterate_Suc2"; +val iterate_Suc = thm "iterate_Suc"; +val monofun_iterate2 = thm "monofun_iterate2"; val wfix_ind = thm "wfix_ind"; -val def_wfix_ind = thm "def_wfix_ind"; structure Fix = struct diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Lift.ML Tue Jul 26 18:29:59 2005 +0200 @@ -15,24 +15,35 @@ val size = thms "lift.size"; end; -val Def_not_UU = thm "Def_not_UU"; +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 DefE2 = thm "DefE2"; 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 Lift_cases = thm "Lift_cases"; -val Lift_exhaust = thm "Lift_exhaust"; -val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; -val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; -val cont_if = thm "cont_if"; +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 flift1_def = thm "flift1_def"; +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 flift2_def = thm "flift2_def"; -val flift2_defined = thm "flift2_defined"; +val inst_lift_pcpo = thm "inst_lift_pcpo"; +val less_lift_def = thm "less_lift_def"; val less_lift = thm "less_lift"; -val less_lift_def = thm "less_lift_def"; +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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/One.ML --- a/src/HOLCF/One.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/One.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,7 +1,7 @@ (* legacy ML bindings *) +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"; -val dist_less_one = thm "dist_less_one"; -val dist_eq_one = thms "dist_eq_one"; diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Pcpo.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,36 +1,41 @@ (* legacy ML bindings *) -val cpo = thm "cpo"; -val least = thm "least"; -val UU_def = thm "UU_def"; +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 ax_flat = thm "ax_flat"; -val UU_least = thm "UU_least"; -val minimal = thm "minimal"; -val thelubE = thm "thelubE"; +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 is_lub_thelub = thm "is_lub_thelub"; -val lub_range_shift = thm "lub_range_shift"; -val maxinch_is_thelub = thm "maxinch_is_thelub"; -val lub_mono = thm "lub_mono"; +val least = thm "least"; +val lub_equal2 = thm "lub_equal2"; val lub_equal = thm "lub_equal"; val lub_mono2 = thm "lub_mono2"; -val lub_equal2 = thm "lub_equal2"; val lub_mono3 = thm "lub_mono3"; -val eq_UU_iff = thm "eq_UU_iff"; -val UU_I = thm "UU_I"; +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 chain_UU_I = thm "chain_UU_I"; -val chain_UU_I_inverse = thm "chain_UU_I_inverse"; -val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2"; val notUU_I = thm "notUU_I"; -val chain_mono2 = thm "chain_mono2"; -val flat_imp_chfin = thm "flat_imp_chfin"; -val flat_eq = thm "flat_eq"; -val chfin2finch = thm "chfin2finch"; -val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma"; -val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma"; +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 diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Porder.ML --- a/src/HOLCF/Porder.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Porder.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,44 +1,46 @@ (* legacy ML bindings *) -val refl_less = thm "refl_less"; +val antisym_less_inverse = thm "antisym_less_inverse"; val antisym_less = thm "antisym_less"; -val trans_less = thm "trans_less"; -val minimal2UU = thm "minimal2UU"; -val antisym_less_inverse = thm "antisym_less_inverse"; +val bin_chainmax = thm "bin_chainmax"; +val bin_chain = thm "bin_chain"; val box_less = thm "box_less"; -val po_eq_conv = thm "po_eq_conv"; -val is_ub_def = thm "is_ub_def"; -val is_lub_def = thm "is_lub_def"; -val tord_def = thm "tord_def"; val chain_def = thm "chain_def"; -val max_in_chain_def = thm "max_in_chain_def"; -val finite_chain_def = thm "finite_chain_def"; -val lub_def = thm "lub_def"; -val unique_lub = thm "unique_lub"; -val chain_mono = thm "chain_mono"; -val chain_mono3 = thm "chain_mono3"; -val chain_tord = thm "chain_tord"; -val lub = thm "lub"; -val lubI = thm "lubI"; -val thelubI = thm "thelubI"; -val lub_singleton = thm "lub_singleton"; -val is_lubD1 = thm "is_lubD1"; -val is_lub_lub = thm "is_lub_lub"; -val is_lubI = thm "is_lubI"; val chainE = thm "chainE"; val chainI = thm "chainI"; +val chain_mono3 = thm "chain_mono3"; +val chain_mono = thm "chain_mono"; val chain_shift = thm "chain_shift"; -val ub_rangeD = thm "ub_rangeD"; -val ub_rangeI = thm "ub_rangeI"; +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 lub_finch1 = thm "lub_finch1"; -val lub_finch2 = thm "lub_finch2"; -val bin_chain = thm "bin_chain"; -val bin_chainmax = thm "bin_chainmax"; +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 diff -r 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Sprod.ML --- a/src/HOLCF/Sprod.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Sprod.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,32 +1,37 @@ (* legacy ML bindings *) +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 spair_def = thm "spair_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 ssnd_def = thm "ssnd_def"; -val ssplit_def = thm "ssplit_def"; -val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; -val spair_strict = thm "spair_strict"; +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_defined_rev = thm "spair_defined_rev"; -val spair_defined = thm "spair_defined"; -val spair_eq = thm "spair_eq"; -val spair_inject = thm "spair_inject"; -val Exh_Sprod2 = thm "Exh_Sprod2"; +val spair_strict = thm "spair_strict"; val sprodE = thm "sprodE"; -val sfst_strict = thm "sfst_strict"; +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 sfst_spair = thm "sfst_spair"; -val ssnd_spair = thm "ssnd_spair"; -val sfst_defined = thm "sfst_defined"; -val ssnd_defined = thm "ssnd_defined"; -val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; -val less_sprod = thm "less_sprod"; -val spair_less = thm "spair_less"; 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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Ssum.ML --- a/src/HOLCF/Ssum.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Ssum.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,35 +1,49 @@ (* legacy ML bindings *) -val Iwhen_def = thm "Iwhen_def"; -val Iwhen1 = thm "Iwhen1"; -val Iwhen2 = thm "Iwhen2"; -val Iwhen3 = thm "Iwhen3"; -val less_ssum_def = thm "less_Ssum_def"; -val sinl_def = thm "sinl_def"; -val sinr_def = thm "sinr_def"; -val sscase_def = thm "sscase_def"; +val beta_sscase = thm "beta_sscase"; val cont_Iwhen1 = thm "cont_Iwhen1"; val cont_Iwhen2 = thm "cont_Iwhen2"; val cont_Iwhen3 = thm "cont_Iwhen3"; -val sinl_strict = thm "sinl_strict"; -val sinr_strict = thm "sinr_strict"; +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 sinr_inject = thm "sinr_inject"; -val sinl_eq = thm "sinl_eq"; -val sinr_eq = thm "sinr_eq"; -val sinl_defined = thm "sinl_defined"; +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 Exh_Ssum1 = thm "Exh_Ssum1"; -val ssumE = thm "ssumE"; -val ssumE2 = thm "ssumE2"; -val sinl_less = thm "sinl_less"; +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 sinl_less_sinr = thm "sinl_less_sinr"; -val sinr_less_sinl = thm "sinr_less_sinl"; +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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Tr.ML --- a/src/HOLCF/Tr.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Tr.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,33 +1,32 @@ (* legacy ML bindings *) -val TT_def = thm "TT_def"; -val FF_def = thm "FF_def"; -val neg_def = thm "neg_def"; -val ifte_def = thm "ifte_def"; +val adm_nFF = thm "adm_nFF"; +val adm_nTT = thm "adm_nTT"; +val adm_trick_1 = thm "adm_trick_1"; +val adm_trick_2 = thm "adm_trick_2"; +val adm_tricks = thms "adm_tricks"; +val andalso_and = thm "andalso_and"; val andalso_def = thm "andalso_def"; -val orelse_def = thm "orelse_def"; -val If2_def = thm "If2_def"; -val Exh_tr = thm "Exh_tr"; -val trE = thm "trE"; -val tr_defs = thms "tr_defs"; -val dist_less_tr = thms "dist_less_tr"; -val dist_eq_tr = thms "dist_eq_tr"; -val ifte_thms = thms "ifte_thms"; +val andalso_or = thm "andalso_or"; val andalso_thms = thms "andalso_thms"; -val orelse_thms = thms "orelse_thms"; -val neg_thms = thms "neg_thms"; -val split_If2 = thm "split_If2"; -val andalso_or = thm "andalso_or"; -val andalso_and = thm "andalso_and"; 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 adm_trick_1 = thm "adm_trick_1"; -val adm_trick_2 = thm "adm_trick_2"; -val adm_tricks = thms "adm_tricks"; -val adm_nTT = thm "adm_nTT"; -val adm_nFF = thm "adm_nFF"; - +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 16094ed8ac6b -r 2128ac2aa5db src/HOLCF/Up.ML --- a/src/HOLCF/Up.ML Tue Jul 26 18:28:11 2005 +0200 +++ b/src/HOLCF/Up.ML Tue Jul 26 18:29:59 2005 +0200 @@ -1,27 +1,38 @@ (* legacy ML bindings *) -val less_up_def = thm "less_up_def"; -val refl_less_up = thm "refl_less_up"; val antisym_less_up = thm "antisym_less_up"; -val trans_less_up = thm "trans_less_up"; -val minimal_up = thm "minimal_up"; -val least_up = thm "least_up"; -val monofun_Ifup2 = thm "monofun_Ifup2"; -val up_lemma1 = thm "up_lemma1"; -val cpo_up = thm "cpo_up"; -val up_def = thm "up_def"; -val fup_def = thm "fup_def"; -val inst_up_pcpo = thm "inst_up_pcpo"; -val cont_Iup = thm "cont_Iup"; 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 up_inject = thm "up_inject"; -val up_eq = thm "up_eq"; -val up_defined = thm "up_defined"; -val up_less = thm "up_less"; -val upE = thm "upE"; 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"; +