# HG changeset patch
# User huffman
# Date 1267317253 28800
# Node ID 34360a1e35372238a53fc7e50ce6820b25bfaa7d
# Parent  8cb42aa19358fe1a84a5d39dce22d4c52c56b311
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style

diff -r 8cb42aa19358 -r 34360a1e3537 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 15:32:42 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 16:34:13 2010 -0800
@@ -268,7 +268,8 @@
 
 (************************** miscellaneous functions ***************************)
 
-val simple_ss : simpset = HOL_basic_ss addsimps simp_thms;
+val simple_ss =
+  HOL_basic_ss addsimps simp_thms;
 
 val beta_ss =
   HOL_basic_ss
@@ -800,7 +801,10 @@
 fun add_discriminators
     (bindings : binding list)
     (spec : (term * (bool * typ) list) list)
+    (lhsT : typ)
+    (casedist : thm)
     (case_const : typ -> term)
+    (case_rews : thm list)
     (thy : theory) =
   let
 
@@ -835,8 +839,56 @@
           define_consts (map_index dis_eqn bindings) thy
     end;
 
+    (* prove discriminator strictness rules *)
+    local
+      fun dis_strict dis =
+        let val goal = mk_trp (mk_strict dis);
+        in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end;
+    in
+      val dis_stricts = map dis_strict dis_consts;
+    end;
+
+    (* prove discriminator/constructor rules *)
+    local
+      fun dis_app (i, dis) (j, (con, args)) =
+        let
+          val Ts = map snd args;
+          val ns = Datatype_Prop.make_tnames Ts;
+          val vs = map Free (ns ~~ Ts);
+          val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+          val lhs = dis ` list_ccomb (con, vs);
+          val rhs = if i = j then @{term TT} else @{term FF};
+          val assms = map (mk_trp o mk_defined) nonlazy;
+          val concl = mk_trp (mk_eq (lhs, rhs));
+          val goal = Logic.list_implies (assms, concl);
+          val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1];
+        in prove thy dis_defs goal (K tacs) end;
+      fun one_dis (i, dis) =
+          map_index (dis_app (i, dis)) spec;
+    in
+      val dis_apps = flat (map_index one_dis dis_consts);
+    end;
+
+    (* prove discriminator definedness rules *)
+    local
+      fun dis_defin dis =
+        let
+          val x = Free ("x", lhsT);
+          val simps = dis_apps @ @{thms dist_eq_tr};
+          val tacs =
+            [rtac @{thm iffI} 1,
+             asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2,
+             rtac casedist 1, atac 1,
+             DETERM_UNTIL_SOLVED (CHANGED
+               (asm_full_simp_tac (simple_ss addsimps simps) 1))];
+          val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x));
+        in prove thy [] goal (K tacs) end;
+    in
+      val dis_defins = map dis_defin dis_consts;
+    end;
+
   in
-    (dis_defs, thy)
+    (dis_stricts @ dis_defins @ dis_apps, thy)
   end;
 
 (******************************************************************************)
@@ -903,7 +955,8 @@
         fun prep_con c (b, args, mx) = (c, map prep_arg args);
         val dis_spec = map2 prep_con con_consts spec;
       in
-        add_discriminators bindings dis_spec case_const thy
+        add_discriminators bindings dis_spec lhsT
+          casedist case_const cases thy
       end
 
     (* restore original signature path *)
diff -r 8cb42aa19358 -r 34360a1e3537 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 15:32:42 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 16:34:13 2010 -0800
@@ -190,7 +190,7 @@
 val {sel_rews, ...} = result;
 val when_rews = #cases result;
 val when_strict = hd when_rews;
-val axs_dis_def = #dis_rews result;
+val dis_rews = #dis_rews result;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)
 
@@ -209,41 +209,6 @@
 (* ----- theorems concerning the constructors, discriminators and selectors - *)
 
 local
-  fun dis_strict (con, _, _) =
-    let
-      val goal = mk_trp (strict (%%:(dis_name con)));
-    in pg axs_dis_def goal (K [rtac when_strict 1]) end;
-
-  fun dis_app c (con, _, args) =
-    let
-      val lhs = %%:(dis_name c) ` con_app con args;
-      val rhs = if con = c then TT else FF;
-      val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
-      val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_dis_def goal (K tacs) end;
-
-  val _ = trace " Proving dis_apps...";
-  val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons;
-
-  fun dis_defin (con, _, args) =
-    let
-      val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
-      val tacs =
-        [rtac casedist 1,
-         contr_tac 1,
-         DETERM_UNTIL_SOLVED (CHANGED
-          (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
-    in pg [] goal (K tacs) end;
-
-  val _ = trace " Proving dis_stricts...";
-  val dis_stricts = map dis_strict cons;
-  val _ = trace " Proving dis_defins...";
-  val dis_defins = map dis_defin cons;
-in
-  val dis_rews = dis_stricts @ dis_defins @ dis_apps;
-end;
-
-local
   fun mat_strict (con, _, _) =
     let
       val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);