src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35482 d756837b708d
parent 35481 7bb9157507a9
child 35486 c91854705b1d
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 20:56:28 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 01 07:35:14 2010 -0800
     1.3 @@ -164,7 +164,7 @@
     1.4  val when_strict = hd when_rews;
     1.5  val dis_rews = #dis_rews result;
     1.6  val mat_rews = #match_rews result;
     1.7 -val axs_pat_def = #pat_rews result;
     1.8 +val pat_rews = #pat_rews result;
     1.9  
    1.10  (* ----- theorems concerning the isomorphism -------------------------------- *)
    1.11  
    1.12 @@ -176,42 +176,6 @@
    1.13  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    1.14  val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
    1.15  
    1.16 -(* ----- theorems concerning the constructors, discriminators and selectors - *)
    1.17 -
    1.18 -local
    1.19 -  fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
    1.20 -
    1.21 -  fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
    1.22 -
    1.23 -  fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
    1.24 -    | pat_rhs (con,_,args) =
    1.25 -        (mk_branch (mk_ctuple_pat (ps args)))
    1.26 -          `(%:"rhs")`(mk_ctuple (map %# args));
    1.27 -
    1.28 -  fun pat_strict c =
    1.29 -    let
    1.30 -      val axs = @{thm branch_def} :: axs_pat_def;
    1.31 -      val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
    1.32 -      val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
    1.33 -    in pg axs goal (K tacs) end;
    1.34 -
    1.35 -  fun pat_app c (con, _, args) =
    1.36 -    let
    1.37 -      val axs = @{thm branch_def} :: axs_pat_def;
    1.38 -      val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
    1.39 -      val rhs = if con = first c then pat_rhs c else mk_fail;
    1.40 -      val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    1.41 -      val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.42 -    in pg axs goal (K tacs) end;
    1.43 -
    1.44 -  val _ = trace " Proving pat_stricts...";
    1.45 -  val pat_stricts = map pat_strict cons;
    1.46 -  val _ = trace " Proving pat_apps...";
    1.47 -  val pat_apps = maps (fn c => map (pat_app c) cons) cons;
    1.48 -in
    1.49 -  val pat_rews = pat_stricts @ pat_apps;
    1.50 -end;
    1.51 -
    1.52  (* ----- theorems concerning one induction step ----------------------------- *)
    1.53  
    1.54  val copy_strict =