# HG changeset patch
# User huffman
# Date 1268076893 28800
# Node ID e8e4af6da8192a724a533fe180fa784140ce9798
# Parent  7a15e181bf3be5982b2fe9c2c8b4df45b8fae6f5
generate take_induct lemmas

diff -r 7a15e181bf3b -r e8e4af6da819 src/HOLCF/Domain_Aux.thy
--- a/src/HOLCF/Domain_Aux.thy	Mon Mar 08 09:37:03 2010 -0800
+++ b/src/HOLCF/Domain_Aux.thy	Mon Mar 08 11:34:53 2010 -0800
@@ -163,6 +163,15 @@
   shows "(\<Squnion>n. t n\<cdot>x) = x"
 using assms by (simp add: lub_distribs)
 
+lemma lub_ID_take_induct:
+  assumes "chain t" and "(\<Squnion>n. t n) = ID"
+  assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
+proof -
+  from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp
+  from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
+  with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
+qed
+
 
 subsection {* Finiteness *}
 
@@ -242,6 +251,11 @@
   with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
 qed
 
+lemma lub_ID_finite_take_induct:
+  assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)"
+  shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
+using lub_ID_finite [OF assms] by metis
+
 subsection {* ML setup *}
 
 use "Tools/Domain/domain_take_proofs.ML"
diff -r 7a15e181bf3b -r e8e4af6da819 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 09:37:03 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 11:34:53 2010 -0800
@@ -31,7 +31,7 @@
 
   val add_lub_take_theorems :
     (binding * iso_info) list -> take_info -> thm list ->
-    theory -> unit * theory
+    theory -> thm list * theory
 
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
@@ -429,6 +429,80 @@
     (result, thy)
   end;
 
+fun prove_finite_take_induct
+    (spec : (binding * iso_info) list)
+    (take_info : take_info)
+    (lub_take_thms : thm list)
+    (thy : theory) =
+  let
+    val dom_binds = map fst spec;
+    val iso_infos = map snd spec;
+    val absTs = map #absT iso_infos;
+    val dnames = map Binding.name_of dom_binds;
+    val {take_consts, ...} = take_info;
+    val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
+    val {finite_consts, finite_defs, ...} = take_info;
+
+    val decisive_lemma =
+      let
+        fun iso_locale info =
+            @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
+        val iso_locale_thms = map iso_locale iso_infos;
+        val decisive_abs_rep_thms =
+            map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms;
+        val n = Free ("n", @{typ nat});
+        fun mk_decisive t =
+            Const (@{const_name decisive}, fastype_of t --> boolT) $ t;
+        fun f take_const = mk_decisive (take_const $ n);
+        val goal = mk_trp (foldr1 mk_conj (map f take_consts));
+        val rules0 = @{thm decisive_bottom} :: take_0_thms;
+        val rules1 =
+            take_Suc_thms @ decisive_abs_rep_thms
+            @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
+        val tac = EVERY [
+            rtac @{thm nat.induct} 1,
+            simp_tac (HOL_ss addsimps rules0) 1,
+            asm_simp_tac (HOL_ss addsimps rules1) 1];
+      in Goal.prove_global thy [] [] goal (K tac) end;
+    fun conjuncts 1 thm = [thm]
+      | conjuncts n thm = let
+          val thmL = thm RS @{thm conjunct1};
+          val thmR = thm RS @{thm conjunct2};
+        in thmL :: conjuncts (n-1) thmR end;
+    val decisive_thms = conjuncts (length spec) decisive_lemma;
+
+    fun prove_finite_thm (absT, finite_const) =
+      let
+        val goal = mk_trp (finite_const $ Free ("x", absT));
+        val tac =
+            EVERY [
+            rewrite_goals_tac finite_defs,
+            rtac @{thm lub_ID_finite} 1,
+            resolve_tac chain_take_thms 1,
+            resolve_tac lub_take_thms 1,
+            resolve_tac decisive_thms 1];
+      in
+        Goal.prove_global thy [] [] goal (K tac)
+      end;
+    val finite_thms =
+        map prove_finite_thm (absTs ~~ finite_consts);
+
+    fun prove_take_induct ((ch_take, lub_take), decisive) =
+        Drule.export_without_context
+          (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]);
+    val take_induct_thms =
+        map prove_take_induct
+          (chain_take_thms ~~ lub_take_thms ~~ decisive_thms);
+
+    val thy = thy
+        |> fold (snd oo add_qualified_thm "finite")
+            (dnames ~~ finite_thms)
+        |> fold (snd oo add_qualified_thm "take_induct")
+            (dnames ~~ take_induct_thms);
+  in
+    ((finite_thms, take_induct_thms), thy)
+  end;
+
 fun add_lub_take_theorems
     (spec : (binding * iso_info) list)
     (take_info : take_info)
@@ -439,8 +513,10 @@
     (* retrieve components of spec *)
     val dom_binds = map fst spec;
     val iso_infos = map snd spec;
-    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
+    val absTs = map #absT iso_infos;
+    val repTs = map #repT iso_infos;
     val dnames = map Binding.name_of dom_binds;
+    val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
     val {chain_take_thms, deflation_take_thms, ...} = take_info;
 
     (* prove take lemmas *)
@@ -469,8 +545,41 @@
       fold_map prove_reach_lemma
         (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
 
-    val result = ();
+    (* test for finiteness of domain definitions *)
+    local
+      val types = [@{type_name ssum}, @{type_name sprod}];
+      fun finite d T = if T mem absTs then d else finite' d T
+      and finite' d (Type (c, Ts)) =
+          let val d' = d andalso c mem types;
+          in forall (finite d') Ts end
+        | finite' d _ = true;
+    in
+      val is_finite = forall (finite true) repTs;
+    end;
 
+    val ((finite_thms, take_induct_thms), thy) =
+      if is_finite
+      then
+        let
+          val ((finites, take_inducts), thy) =
+              prove_finite_take_induct spec take_info lub_take_thms thy;
+        in
+          ((SOME finites, take_inducts), thy)
+        end
+      else
+        let
+          fun prove_take_induct (chain_take, lub_take) =
+              Drule.export_without_context
+                (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
+          val take_inducts =
+              map prove_take_induct (chain_take_thms ~~ lub_take_thms);
+          val thy = fold (snd oo add_qualified_thm "take_induct")
+                         (dnames ~~ take_inducts) thy;
+        in
+          ((NONE, take_inducts), thy)
+        end;
+
+    val result = take_induct_thms;
   in
     (result, thy)
   end;