# HG changeset patch
# User huffman
# Date 1267332979 28800
# Node ID 9fcfd57631811b7ff1f7d38085a55656565fb261
# Parent  064bb6e9ace0904a5a94b7e50cb1a235dd71d102
move proofs of match_rews to domain_constructors.ML

diff -r 064bb6e9ace0 -r 9fcfd5763181 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 20:04:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 20:56:19 2010 -0800
@@ -955,11 +955,45 @@
       val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy;
     end;
 
+    (* prove strictness of match combinators *)
+    local
+      fun match_strict mat =
+        let
+          val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat));
+          val k = Free ("k", U);
+          val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V));
+          val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1];
+        in prove thy match_defs goal (K tacs) end;
+    in
+      val match_stricts = map match_strict match_consts;
+    end;
+
+    (* prove match/constructor rules *)
+    local
+      val fail = mk_fail resultT;
+      fun match_app (i, mat) (j, (con, args)) =
+        let
+          val Ts = map snd args;
+          val ns = Name.variant_list ["k"] (Datatype_Prop.make_tnames Ts);
+          val vs = map Free (ns ~~ Ts);
+          val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+          val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat));
+          val k = Free ("k", kT);
+          val lhs = mat ` list_ccomb (con, vs) ` k;
+          val rhs = if i = j then list_ccomb (k, vs) else fail;
+          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 match_defs goal (K tacs) end;
+      fun one_match (i, mat) =
+          map_index (match_app (i, mat)) spec;
+    in
+      val match_apps = flat (map_index one_match match_consts);
+    end;
+
   in
-    (match_defs, thy)
-(*
     (match_stricts @ match_apps, thy)
-*)
   end;
 
 (******************************************************************************)
diff -r 064bb6e9ace0 -r 9fcfd5763181 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 20:04:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 20:56:19 2010 -0800
@@ -156,7 +156,7 @@
 val when_rews = #cases result;
 val when_strict = hd when_rews;
 val dis_rews = #dis_rews result;
-val axs_mat_def = #match_rews result;
+val mat_rews = #match_rews result;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)
 
@@ -171,34 +171,6 @@
 (* ----- theorems concerning the constructors, discriminators and selectors - *)
 
 local
-  fun mat_strict (con, _, _) =
-    let
-      val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
-      val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
-    in pg axs_mat_def goal (K tacs) end;
-
-  val _ = trace " Proving mat_stricts...";
-  val mat_stricts = map mat_strict cons;
-
-  fun one_mat c (con, _, args) =
-    let
-      val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
-      val rhs =
-        if con = c
-        then list_ccomb (%:"rhs", map %# args)
-        else mk_fail;
-      val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
-      val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_mat_def goal (K tacs) end;
-
-  val _ = trace " Proving mat_apps...";
-  val mat_apps =
-    maps (fn (c,_,_) => map (one_mat c) cons) cons;
-in
-  val mat_rews = mat_stricts @ mat_apps;
-end;
-
-local
   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
 
   fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));