# HG changeset patch
# User huffman
# Date 1267457714 28800
# Node ID d756837b708d112365ce3513e56342ebcfe125f0
# Parent  7bb9157507a90785a6d9f5682af24288236583b3
move proofs of pat_rews to domain_constructors.ML

diff -r 7bb9157507a9 -r d756837b708d src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Feb 28 20:56:28 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 07:35:14 2010 -0800
@@ -817,23 +817,27 @@
     (thy : theory) =
   let
 
+    (* utility functions *)
+    fun mk_pair_pat (p1, p2) =
+      let
+        val T1 = fastype_of p1;
+        val T2 = fastype_of p2;
+        val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
+        val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
+        val pat_typ = [T1, T2] --->
+            (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
+        val pat_const = Const (@{const_name cpair_pat}, pat_typ);
+      in
+        pat_const $ p1 $ p2
+      end;
+    fun mk_tuple_pat [] = return_const HOLogic.unitT
+      | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
+    fun branch_const (T,U,V) = 
+      Const (@{const_name branch},
+        (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
+
     (* define pattern combinators *)
     local
-      fun mk_pair_pat (p1, p2) =
-        let
-          val T1 = fastype_of p1;
-          val T2 = fastype_of p2;
-          val (U1, V1) = apsnd dest_matchT (dest_cfunT T1);
-          val (U2, V2) = apsnd dest_matchT (dest_cfunT T2);
-          val pat_typ = [T1, T2] --->
-              (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2)));
-          val pat_const = Const (@{const_name cpair_pat}, pat_typ);
-        in
-          pat_const $ p1 $ p2
-        end;
-      fun mk_tuple_pat [] = return_const HOLogic.unitT
-        | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
-
       val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
 
       fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
@@ -841,7 +845,7 @@
           val pat_bind = Binding.suffix_name "_pat" bind;
           val Ts = map snd args;
           val Vs =
-              (map (K "t") args)
+              (map (K "'t") args)
               |> Datatype_Prop.indexify_names
               |> Name.variant_list tns
               |> map (fn t => TFree (t, @{sort pcpo}));
@@ -902,8 +906,63 @@
       val thy = Sign.add_trrules_i trans_rules thy;
     end;
 
+    (* prove strictness and reduction rules of pattern combinators *)
+    local
+      val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+      val rn = Name.variant tns "'r";
+      val R = TFree (rn, @{sort pcpo});
+      fun pat_lhs (pat, args) =
+        let
+          val Ts = map snd args;
+          val Vs =
+              (map (K "'t") args)
+              |> Datatype_Prop.indexify_names
+              |> Name.variant_list (rn::tns)
+              |> map (fn t => TFree (t, @{sort pcpo}));
+          val patNs = Datatype_Prop.indexify_names (map (K "pat") args);
+          val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
+          val pats = map Free (patNs ~~ patTs);
+          val k = Free ("rhs", mk_tupleT Vs ->> R);
+          val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
+          val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
+          val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
+          val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
+          val taken = "rhs" :: patNs;
+        in (fun1, fun2, taken) end;
+      fun pat_strict (pat, (con, args)) =
+        let
+          val (fun1, fun2, taken) = pat_lhs (pat, args);
+          val defs = @{thm branch_def} :: pat_defs;
+          val goal = mk_trp (mk_strict fun1);
+          val rules = @{thm Fixrec.bind_strict} :: case_rews;
+          val tacs = [simp_tac (beta_ss addsimps rules) 1];
+        in prove thy defs goal (K tacs) end;
+      fun pat_apps (i, (pat, (con, args))) =
+        let
+          val (fun1, fun2, taken) = pat_lhs (pat, args);
+          fun pat_app (j, (con', args')) =
+            let
+              val Ts = map snd args';
+              val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts);
+              val vs = map Free (ns ~~ Ts);
+              val con_app = list_ccomb (con', vs);
+              val nonlazy = map snd (filter_out (fst o fst) (args' ~~ vs));
+              val assms = map (mk_trp o mk_defined) nonlazy;
+              val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
+              val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
+              val goal = Logic.list_implies (assms, concl);
+              val defs = @{thm branch_def} :: pat_defs;
+              val rules = @{thms bind_fail left_unit} @ case_rews;
+              val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
+            in prove thy defs goal (K tacs) end;
+        in map_index pat_app spec end;
+    in
+      val pat_stricts = map pat_strict (pat_consts ~~ spec);
+      val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
+    end;
+
   in
-    (pat_defs, thy)
+    (pat_stricts @ pat_apps, thy)
   end
 
 (******************************************************************************)
diff -r 7bb9157507a9 -r d756837b708d src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 28 20:56:28 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 01 07:35:14 2010 -0800
@@ -164,7 +164,7 @@
 val when_strict = hd when_rews;
 val dis_rews = #dis_rews result;
 val mat_rews = #match_rews result;
-val axs_pat_def = #pat_rews result;
+val pat_rews = #pat_rews result;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)
 
@@ -176,42 +176,6 @@
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
 
-(* ----- theorems concerning the constructors, discriminators and selectors - *)
-
-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));
-
-  fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
-    | pat_rhs (con,_,args) =
-        (mk_branch (mk_ctuple_pat (ps args)))
-          `(%:"rhs")`(mk_ctuple (map %# args));
-
-  fun pat_strict c =
-    let
-      val axs = @{thm branch_def} :: axs_pat_def;
-      val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
-      val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
-    in pg axs goal (K tacs) end;
-
-  fun pat_app c (con, _, args) =
-    let
-      val axs = @{thm branch_def} :: axs_pat_def;
-      val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
-      val rhs = if con = first c then pat_rhs c 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 goal (K tacs) end;
-
-  val _ = trace " Proving pat_stricts...";
-  val pat_stricts = map pat_strict cons;
-  val _ = trace " Proving pat_apps...";
-  val pat_apps = maps (fn c => map (pat_app c) cons) cons;
-in
-  val pat_rews = pat_stricts @ pat_apps;
-end;
-
 (* ----- theorems concerning one induction step ----------------------------- *)
 
 val copy_strict =