src/HOLCF/Tools/Domain/domain_theorems.ML
 changeset 35461 34360a1e3537 parent 35460 8cb42aa19358 child 35462 f5461b02d754
```     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 15:32:42 2010 -0800
1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 16:34:13 2010 -0800
1.3 @@ -190,7 +190,7 @@
1.4  val {sel_rews, ...} = result;
1.5  val when_rews = #cases result;
1.6  val when_strict = hd when_rews;
1.7 -val axs_dis_def = #dis_rews result;
1.8 +val dis_rews = #dis_rews result;
1.9
1.10  (* ----- theorems concerning the isomorphism -------------------------------- *)
1.11
1.12 @@ -209,41 +209,6 @@
1.13  (* ----- theorems concerning the constructors, discriminators and selectors - *)
1.14
1.15  local
1.16 -  fun dis_strict (con, _, _) =
1.17 -    let
1.18 -      val goal = mk_trp (strict (%%:(dis_name con)));
1.19 -    in pg axs_dis_def goal (K [rtac when_strict 1]) end;
1.20 -
1.21 -  fun dis_app c (con, _, args) =
1.22 -    let
1.23 -      val lhs = %%:(dis_name c) ` con_app con args;
1.24 -      val rhs = if con = c then TT else FF;
1.25 -      val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
1.26 -      val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
1.27 -    in pg axs_dis_def goal (K tacs) end;
1.28 -
1.29 -  val _ = trace " Proving dis_apps...";
1.30 -  val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons;
1.31 -
1.32 -  fun dis_defin (con, _, args) =
1.33 -    let
1.34 -      val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
1.35 -      val tacs =
1.36 -        [rtac casedist 1,
1.37 -         contr_tac 1,
1.38 -         DETERM_UNTIL_SOLVED (CHANGED
1.39 -          (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
1.40 -    in pg [] goal (K tacs) end;
1.41 -
1.42 -  val _ = trace " Proving dis_stricts...";
1.43 -  val dis_stricts = map dis_strict cons;
1.44 -  val _ = trace " Proving dis_defins...";
1.45 -  val dis_defins = map dis_defin cons;
1.46 -in
1.47 -  val dis_rews = dis_stricts @ dis_defins @ dis_apps;
1.48 -end;
1.49 -
1.50 -local
1.51    fun mat_strict (con, _, _) =
1.52      let
1.53        val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
```