src/HOLCF/Tools/domain/domain_theorems.ML
changeset 25805 5df82bb5b982
parent 25132 dffe405b090d
child 25895 0eaadfa8889e
     1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Jan 03 16:53:27 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Jan 03 17:02:56 2008 +0100
     1.3 @@ -12,32 +12,53 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val adm_impl_admw = thm "adm_impl_admw";
     1.8 -val antisym_less_inverse = thm "antisym_less_inverse";
     1.9 -val beta_cfun = thm "beta_cfun";
    1.10 -val cfun_arg_cong = thm "cfun_arg_cong";
    1.11 -val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
    1.12 -val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
    1.13 -val chain_iterate = thm "chain_iterate";
    1.14 -val compact_ONE = thm "compact_ONE";
    1.15 -val compact_sinl = thm "compact_sinl";
    1.16 -val compact_sinr = thm "compact_sinr";
    1.17 -val compact_spair = thm "compact_spair";
    1.18 -val compact_up = thm "compact_up";
    1.19 -val contlub_cfun_arg = thm "contlub_cfun_arg";
    1.20 -val contlub_cfun_fun = thm "contlub_cfun_fun";
    1.21 -val fix_def2 = thm "fix_def2";
    1.22 -val injection_eq = thm "injection_eq";
    1.23 -val injection_less = thm "injection_less";
    1.24 -val lub_equal = thm "lub_equal";
    1.25 -val monofun_cfun_arg = thm "monofun_cfun_arg";
    1.26 -val retraction_strict = thm "retraction_strict";
    1.27 -val spair_eq = thm "spair_eq";
    1.28 -val spair_less = thm "spair_less";
    1.29 -val sscase1 = thm "sscase1";
    1.30 -val ssplit1 = thm "ssplit1";
    1.31 -val strictify1 = thm "strictify1";
    1.32 -val wfix_ind = thm "wfix_ind";
    1.33 +val adm_impl_admw = @{thm adm_impl_admw};
    1.34 +val adm_all2 = @{thm adm_all2};
    1.35 +val adm_conj = @{thm adm_conj};
    1.36 +val adm_subst = @{thm adm_subst};
    1.37 +val antisym_less_inverse = @{thm antisym_less_inverse};
    1.38 +val beta_cfun = @{thm beta_cfun};
    1.39 +val cfun_arg_cong = @{thm cfun_arg_cong};
    1.40 +val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
    1.41 +val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
    1.42 +val chain_iterate = @{thm chain_iterate};
    1.43 +val compact_ONE = @{thm compact_ONE};
    1.44 +val compact_sinl = @{thm compact_sinl};
    1.45 +val compact_sinr = @{thm compact_sinr};
    1.46 +val compact_spair = @{thm compact_spair};
    1.47 +val compact_up = @{thm compact_up};
    1.48 +val contlub_cfun_arg = @{thm contlub_cfun_arg};
    1.49 +val contlub_cfun_fun = @{thm contlub_cfun_fun};
    1.50 +val fix_def2 = @{thm fix_def2};
    1.51 +val injection_eq = @{thm injection_eq};
    1.52 +val injection_less = @{thm injection_less};
    1.53 +val lub_equal = @{thm lub_equal};
    1.54 +val monofun_cfun_arg = @{thm monofun_cfun_arg};
    1.55 +val retraction_strict = @{thm retraction_strict};
    1.56 +val spair_eq = @{thm spair_eq};
    1.57 +val spair_less = @{thm spair_less};
    1.58 +val sscase1 = @{thm sscase1};
    1.59 +val ssplit1 = @{thm ssplit1};
    1.60 +val strictify1 = @{thm strictify1};
    1.61 +val wfix_ind = @{thm wfix_ind};
    1.62 +
    1.63 +val iso_intro       = @{thm iso.intro};
    1.64 +val iso_abs_iso     = @{thm iso.abs_iso};
    1.65 +val iso_rep_iso     = @{thm iso.rep_iso};
    1.66 +val iso_abs_strict  = @{thm iso.abs_strict};
    1.67 +val iso_rep_strict  = @{thm iso.rep_strict};
    1.68 +val iso_abs_defin'  = @{thm iso.abs_defin'};
    1.69 +val iso_rep_defin'  = @{thm iso.rep_defin'};
    1.70 +val iso_abs_defined = @{thm iso.abs_defined};
    1.71 +val iso_rep_defined = @{thm iso.rep_defined};
    1.72 +val iso_compact_abs = @{thm iso.compact_abs};
    1.73 +val iso_compact_rep = @{thm iso.compact_rep};
    1.74 +val iso_iso_swap    = @{thm iso.iso_swap};
    1.75 +
    1.76 +val exh_start = @{thm exh_start};
    1.77 +val ex_defined_iffs = @{thms ex_defined_iffs};
    1.78 +val exh_casedist0 = @{thm exh_casedist0};
    1.79 +val exh_casedists = @{thms exh_casedists};
    1.80  
    1.81  open Domain_Library;
    1.82  infixr 0 ===>;
    1.83 @@ -203,7 +224,7 @@
    1.84    val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
    1.85    val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
    1.86    val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
    1.87 -  val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2;
    1.88 +  val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
    1.89  
    1.90    (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
    1.91    val tacs = [
    1.92 @@ -353,7 +374,7 @@
    1.93        val concl = mk_trp (defined (con_app con args));
    1.94        val goal = lift_defined %: (nonlazy args, concl);
    1.95        val tacs = [
    1.96 -        rtac rev_contrapos 1,
    1.97 +        rtac @{thm rev_contrapos} 1,
    1.98          eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
    1.99          asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   1.100      in pg [] goal tacs end;
   1.101 @@ -454,7 +475,7 @@
   1.102          val goal = lift_defined %: (nonlazy args1,
   1.103                          mk_trp (con_app con1 args1 ~<< con_app con2 args2));
   1.104          val tacs = [
   1.105 -          rtac rev_contrapos 1,
   1.106 +          rtac @{thm rev_contrapos} 1,
   1.107            eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
   1.108            @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
   1.109            @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];