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);