store map_ID thms in theory data; automate proofs of reach lemmas

--- a/src/HOLCF/Representable.thy	Thu Nov 19 21:44:37 2009 -0800
+++ b/src/HOLCF/Representable.thy	Thu Nov 19 22:25:11 2009 -0800
@@ -1038,28 +1038,28 @@
 setup {*
   fold Domain_Isomorphism.add_type_constructor
     [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
-        @{thm REP_cfun}, @{thm isodefl_cfun}),
+        @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}),
 
      (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
-        @{thm REP_ssum}, @{thm isodefl_ssum}),
+        @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
 
      (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
-        @{thm REP_sprod}, @{thm isodefl_sprod}),
+        @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
 
      (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
-        @{thm REP_cprod}, @{thm isodefl_cprod}),
+        @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
 
      (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
-        @{thm REP_up}, @{thm isodefl_u}),
+        @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}),
 
      (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
-        @{thm REP_upper}, @{thm isodefl_upper}),
+        @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
 
      (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
-        @{thm REP_lower}, @{thm isodefl_lower}),
+        @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
 
      (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
-        @{thm REP_convex}, @{thm isodefl_convex})]
+        @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
 *}
 
 end

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 21:44:37 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 22:25:11 2009 -0800
@@ -150,7 +150,7 @@
                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
   in (dnam,
-      (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+      (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
       (if definitional then [when_def] else [when_def, copy_def]) @
       con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
       [take_def, finite_def])

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 21:44:37 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 22:25:11 2009 -0800
@@ -11,7 +11,7 @@
   val domain_isomorphism_cmd:
     (string list * binding * mixfix * string) list -> theory -> theory
   val add_type_constructor:
-    (string * term * string * thm  * thm) -> theory -> theory
+    (string * term * string * thm  * thm * thm) -> theory -> theory
   val get_map_tab:
     theory -> string Symtab.table
 end;
@@ -63,12 +63,21 @@
   val merge = Thm.merge_thms;
 );
 
+structure MapIdData = Theory_Data
+(
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  val merge = Thm.merge_thms;
+);
+
 fun add_type_constructor
-  (tname, defl_const, map_name, REP_thm, isodefl_thm) =
+  (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) =
     DeflData.map (Symtab.insert (K true) (tname, defl_const))
     #> MapData.map (Symtab.insert (K true) (tname, map_name))
     #> RepData.map (Thm.add_thm REP_thm)
-    #> IsodeflData.map (Thm.add_thm isodefl_thm);
+    #> IsodeflData.map (Thm.add_thm isodefl_thm)
+    #> MapIdData.map (Thm.add_thm map_ID_thm);
 
 val get_map_tab = MapData.get;
 
@@ -558,6 +567,7 @@
     val (_, thy) = thy |>
       (PureThy.add_thms o map Thm.no_attributes)
         (map_ID_binds ~~ map_ID_thms);
+    val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
 
     (* define copy combinators *)
     val new_dts =
@@ -568,7 +578,7 @@
       let fun mk_copy_args [] t = []
             | mk_copy_args (_::[]) t = [t]
             | mk_copy_args (_::xs) t =
-              HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t);
+                mk_fst t :: mk_copy_args xs (mk_snd t);
       in mk_copy_args doms copy_arg end;
     fun copy_of_dtyp (T, dt) =
         if DatatypeAux.is_rec_type dt
@@ -628,6 +638,46 @@
             ||> Sign.parent_path;
         in ((c_const, c_def_thms), thy) end;
 
+    (* fixed-point lemma for combined copy combinator *)
+    val fix_copy_lemma =
+      let
+        fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) =
+          Library.foldl mk_capply (map_const, map ID_const Ts);
+        val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
+        val goal = mk_eqs (mk_fix c_const, rhs);
+        val rules =
+          [@{thm pair_collapse}, @{thm split_def}]
+          @ map_apply_thms
+          @ c_def_thms @ copy_defs
+          @ MapIdData.get thy;
+        val tac = simp_tac (beta_ss addsimps rules) 1;
+      in
+        Goal.prove_global thy [] [] goal (K tac)
+      end;
+
+    (* prove reach lemmas *)
+    val reach_thm_projs =
+      let fun mk_projs (x::[]) t = [(x, t)]
+            | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+      in mk_projs dom_binds (mk_fix c_const) end;
+    fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy =
+      let
+        val x = Free ("x", lhsT);
+        val goal = mk_eqs (mk_capply (t, x), x);
+        val rules =
+          fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1};
+        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+        val reach_thm = Goal.prove_global thy [] [] goal (K tac);
+      in
+        thy
+        |> Sign.add_path (Binding.name_of bind)
+        |> yield_singleton (PureThy.add_thms o map Thm.no_attributes)
+            (Binding.name "reach", reach_thm)
+        ||> Sign.parent_path
+      end;
+    val (reach_thms, thy) = thy |>
+      fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
+
   in
     thy
   end;