introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'

--- a/src/HOLCF/Domain.thy	Fri Mar 05 14:05:25 2010 -0800
+++ b/src/HOLCF/Domain.thy	Fri Mar 05 14:50:37 2010 -0800
@@ -214,6 +214,102 @@
   ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
 
 
+subsection {* Take functions and finiteness *}
+
+lemma lub_ID_take_lemma:
+  assumes "chain t" and "(\<Squnion>n. t n) = ID"
+  assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
+proof -
+  have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
+    using assms(3) by simp
+  then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
+    using assms(1) by (simp add: lub_distribs)
+  then show "x = y"
+    using assms(2) by simp
+qed
+
+lemma lub_ID_reach:
+  assumes "chain t" and "(\<Squnion>n. t n) = ID"
+  shows "(\<Squnion>n. t n\<cdot>x) = x"
+using assms by (simp add: lub_distribs)
+
+text {*
+  Let a ``decisive'' function be a deflation that maps every input to
+  either itself or bottom.  Then if a domain's take functions are all
+  decisive, then all values in the domain are finite.
+*}
+
+definition
+  decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
+where
+  "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
+
+lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
+  unfolding decisive_def by simp
+
+lemma decisive_cases:
+  assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
+using assms unfolding decisive_def by auto
+
+lemma decisive_bottom: "decisive \<bottom>"
+  unfolding decisive_def by simp
+
+lemma decisive_ID: "decisive ID"
+  unfolding decisive_def by simp
+
+lemma decisive_ssum_map:
+  assumes f: "decisive f"
+  assumes g: "decisive g"
+  shows "decisive (ssum_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_sprod_map:
+  assumes f: "decisive f"
+  assumes g: "decisive g"
+  shows "decisive (sprod_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_abs_rep:
+  fixes abs rep
+  assumes iso: "iso abs rep"
+  assumes d: "decisive d"
+  shows "decisive (abs oo d oo rep)"
+apply (rule decisiveI)
+apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
+apply (simp add: iso.rep_iso [OF iso])
+apply (simp add: iso.abs_strict [OF iso])
+done
+
+lemma lub_ID_finite:
+  assumes chain: "chain d"
+  assumes lub: "(\<Squnion>n. d n) = ID"
+  assumes decisive: "\<And>n. decisive (d n)"
+  shows "\<exists>n. d n\<cdot>x = x"
+proof -
+  have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
+  have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
+  have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
+    using decisive unfolding decisive_def by simp
+  hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
+    by auto
+  hence "finite (range (\<lambda>n. d n\<cdot>x))"
+    by (rule finite_subset, simp)
+  with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
+    by (rule finite_range_imp_finch)
+  then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
+    unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
+  with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
+qed
+
+
 subsection {* Installing the domain package *}
 
 lemmas con_strict_rules =
@@ -253,23 +349,6 @@
   ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
   sprod_map_spair' sprod_map_strict u_map_up u_map_strict
 
-lemma lub_ID_take_lemma:
-  assumes "chain t" and "(\<Squnion>n. t n) = ID"
-  assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
-proof -
-  have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
-    using assms(3) by simp
-  then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
-    using assms(1) by (simp add: lub_distribs)
-  then show "x = y"
-    using assms(2) by simp
-qed
-
-lemma lub_ID_reach:
-  assumes "chain t" and "(\<Squnion>n. t n) = ID"
-  shows "(\<Squnion>n. t n\<cdot>x) = x"
-using assms by (simp add: lub_distribs)
-
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
 use "Tools/Domain/domain_library.ML"

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:05:25 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:50:37 2010 -0800
@@ -216,8 +216,13 @@
     fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
     fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
   in
+    val axs_rep_iso = map (ga "rep_iso") dnames;
+    val axs_abs_iso = map (ga "abs_iso") dnames;
     val axs_chain_take = map (ga "chain_take") dnames;
+    val lub_take_thms = map (ga "lub_take") dnames;
     val axs_finite_def = map (ga "finite_def") dnames;
+    val take_0_thms = map (ga "take_0") dnames;
+    val take_Suc_thms = map (ga "take_Suc") dnames;
     val cases = map (ga  "casedist" ) dnames;
     val con_rews  = maps (gts "con_rews" ) dnames;
   end;
@@ -318,75 +323,41 @@
   (
     if is_finite
     then (* finite case *)
-      let 
-        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
-        fun dname_lemma dn =
-          let
-            val prem1 = mk_trp (defined (%:"x"));
-            val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
-            val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
-            val concl = mk_trp (take_enough dn);
-            val goal = prem1 ===> prem2 ===> concl;
-            val tacs = [
-              etac disjE 1,
-              etac notE 1,
-              resolve_tac take_lemmas 1,
-              asm_simp_tac take_ss 1,
-              atac 1];
-          in pg [] goal (K tacs) end;
-        val _ = trace " Proving finite_lemmas1a";
-        val finite_lemmas1a = map dname_lemma dnames;
- 
-        val _ = trace " Proving finite_lemma1b";
-        val finite_lemma1b =
+      let
+        val decisive_lemma =
           let
-            fun mk_eqn n ((dn, args), _) =
-              let
-                val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
-                val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
-              in
-                mk_constrainall
-                  (x_name n, Type (dn,args), mk_disj (disj1, disj2))
-              end;
-            val goal =
-              mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
-            fun arg_tacs ctxt vn = [
-              eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
-              etac disjE 1,
-              asm_simp_tac (HOL_ss addsimps con_rews) 1,
-              asm_simp_tac take_ss 1];
-            fun con_tacs ctxt (con, args) =
-              asm_simp_tac take_ss 1 ::
-              maps (arg_tacs ctxt) (nonlazy_rec args);
-            fun foo_tacs ctxt n (cons, cases) =
-              simp_tac take_ss 1 ::
-              rtac allI 1 ::
-              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
-              asm_simp_tac take_ss 1 ::
-              maps (con_tacs ctxt) cons;
-            fun tacs ctxt =
-              rtac allI 1 ::
-              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
-              simp_tac take_ss 1 ::
-              TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
-              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
-          in pg [] goal tacs end;
-
-        fun one_finite (dn, l1b) =
+            val iso_locale_thms =
+                map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
+                axs_abs_iso axs_rep_iso;
+            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_name decisive} $ t;
+            fun f dn = mk_decisive (dc_take dn $ n);
+            val goal = mk_trp (foldr1 mk_conj (map f dnames));
+            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 tacs = [
+                rtac @{thm nat.induct} 1,
+                simp_tac (HOL_ss addsimps rules0) 1,
+                asm_simp_tac (HOL_ss addsimps rules1) 1];
+          in pg [] goal (K tacs) end;
+        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+        fun one_finite (dn, decisive_thm) =
           let
             val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
-            fun tacs ctxt = [
-                        (* FIXME! case_UU_tac *)
-              case_UU_tac ctxt take_rews 1 "x",
-              eresolve_tac finite_lemmas1a 1,
-              step_tac HOL_cs 1,
-              step_tac HOL_cs 1,
-              cut_facts_tac [l1b] 1,
-              fast_tac HOL_cs 1];
-          in pg axs_finite_def goal tacs end;
+            val tacs = [
+                rtac @{thm lub_ID_finite} 1,
+                resolve_tac axs_chain_take 1,
+                resolve_tac lub_take_thms 1,
+                rtac decisive_thm 1];
+          in pg axs_finite_def goal (K tacs) end;
 
         val _ = trace " Proving finites";
-        val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
+        val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
         val _ = trace " Proving ind";
         val ind =
           let