src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35512 d1ef88d7de5a
parent 35497 979706bd5c16
child 35514 a2cfa413eaab
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:53:18 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 09:54:50 2010 -0800
     1.3 @@ -95,10 +95,6 @@
     1.4    InductTacs.case_tac ctxt (v^"=UU") i THEN
     1.5    asm_simp_tac (HOLCF_ss addsimps rews) i;
     1.6  
     1.7 -val chain_tac =
     1.8 -  REPEAT_DETERM o resolve_tac 
     1.9 -    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
    1.10 -
    1.11  (* ----- general proofs ----------------------------------------------------- *)
    1.12  
    1.13  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
    1.14 @@ -171,8 +167,6 @@
    1.15  
    1.16  val pg = pg' thy;
    1.17  
    1.18 -val dc_copy = %%:(dname^"_copy");
    1.19 -
    1.20  val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
    1.21  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    1.22  val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
    1.23 @@ -195,10 +189,6 @@
    1.24            else (%# arg);
    1.25        val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
    1.26        val rhs = con_app2 con one_rhs args;
    1.27 -      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
    1.28 -      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
    1.29 -      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
    1.30 -      val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    1.31        val goal = mk_trp (lhs === rhs);
    1.32        val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
    1.33        val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;