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 =
```