restrict admissibility to non-empty chains to allow more syntax-directed proof rules

--- a/src/HOL/Complete_Partial_Order.thy	Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Thu Dec 05 09:20:32 2013 +0100
@@ -50,6 +50,9 @@
   obtains "ord x y" | "ord y x"
 using assms unfolding chain_def by fast
 
+lemma chain_empty: "chain ord {}"
+by(simp add: chain_def)
+
 subsection {* Chain-complete partial orders *}
 
 text {*
@@ -119,6 +122,9 @@
   qed
 qed
 
+lemma bot_in_iterates: "Sup {} \<in> iterates f"
+by(auto intro: iterates.Sup simp add: chain_empty)
+
 subsection {* Fixpoint combinator *}
 
 definition
@@ -162,16 +168,17 @@
 setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
 
 definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
+where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
 
 lemma admissibleI:
-  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
+  assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
   shows "ccpo.admissible lub ord P"
 using assms unfolding ccpo.admissible_def by fast
 
 lemma admissibleD:
   assumes "ccpo.admissible lub ord P"
   assumes "chain ord A"
+  assumes "A \<noteq> {}"
   assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
   shows "P (lub A)"
 using assms by (auto simp: ccpo.admissible_def)
@@ -181,24 +188,26 @@
 lemma (in ccpo) fixp_induct:
   assumes adm: "ccpo.admissible Sup (op \<le>) P"
   assumes mono: "monotone (op \<le>) (op \<le>) f"
+  assumes bot: "P (Sup {})"
   assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
   shows "P (fixp f)"
 unfolding fixp_def using adm chain_iterates[OF mono]
 proof (rule ccpo.admissibleD)
+  show "iterates f \<noteq> {}" using bot_in_iterates by auto
   fix x assume "x \<in> iterates f"
   thus "P x"
     by (induct rule: iterates.induct)
-      (auto intro: step ccpo.admissibleD adm)
+      (case_tac "M = {}", auto intro: step bot ccpo.admissibleD adm)
 qed
 
 lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
 unfolding ccpo.admissible_def by simp
 
-lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
+(*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
 unfolding ccpo.admissible_def chain_def by simp
-
-lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
-by (cases t, simp_all add: admissible_True admissible_False)
+*)
+lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
+by(auto intro: ccpo.admissibleI)
 
 lemma admissible_conj:
   assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
@@ -248,15 +257,16 @@
   shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
 proof (rule ccpo.admissibleI)
   fix A :: "'a set" assume A: "chain (op \<le>) A"
-  assume "\<forall>x\<in>A. P x \<or> Q x"
-  hence "(\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
+  assume "A \<noteq> {}"
+    and "\<forall>x\<in>A. P x \<or> Q x"
+  hence "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
     using chainD[OF A] by blast
-  hence "Sup A = Sup {x \<in> A. P x} \<or> Sup A = Sup {x \<in> A. Q x}"
-    using admissible_disj_lemma [OF A] by fast
+  hence "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
+    using admissible_disj_lemma [OF A] by blast
   thus "P (Sup A) \<or> Q (Sup A)"
     apply (rule disjE, simp_all)
-    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
-    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
+    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp, simp)
+    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp, simp)
     done
 qed
 

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 05 09:20:32 2013 +0100
@@ -415,6 +415,9 @@
 definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
   "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
 
+lemma Heap_lub_empty: "Heap_lub {} = Heap Map.empty"
+by(simp add: Heap_lub_def img_lub_def fun_lub_def flat_lub_def)
+
 lemma heap_interpretation: "partial_function_definitions Heap_ord Heap_lub"
 proof -
   have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
@@ -427,7 +430,8 @@
 qed
 
 interpretation heap!: partial_function_definitions Heap_ord Heap_lub
-by (fact heap_interpretation)
+  where "Heap_lub {} \<equiv> Heap Map.empty"
+by (fact heap_interpretation)(simp add: Heap_lub_empty)
 
 lemma heap_step_admissible: 
   "option.admissible
@@ -473,6 +477,7 @@
   assumes defined: "effect (U f x) h h' r"
   shows "P x h h' r"
   using step defined heap.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_heap, of P]
+  unfolding effect_def execute.simps
   by blast
 
 declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}

--- a/src/HOL/Partial_Function.thy	Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Partial_Function.thy	Thu Dec 05 09:20:32 2013 +0100
@@ -176,11 +176,12 @@
   assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
   assumes inverse: "\<And>f. U (C f) = f"
   assumes adm: "ccpo.admissible lub_fun le_fun P"
+  and bot: "P (\<lambda>_. lub {})"
   assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
   shows "P (U f)"
 unfolding eq inverse
 apply (rule ccpo.fixp_induct[OF ccpo adm])
-apply (insert mono, auto simp: monotone_def fun_ord_def)[1]
+apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
 by (rule_tac f="C x" in step, simp add: inverse)
 
 
@@ -237,11 +238,13 @@
 
 interpretation tailrec!:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
-by (rule flat_interpretation)
+  where "flat_lub undefined {} \<equiv> undefined"
+by (rule flat_interpretation)(simp add: flat_lub_def)
 
 interpretation option!:
   partial_function_definitions "flat_ord None" "flat_lub None"
-by (rule flat_interpretation)
+  where "flat_lub None {} \<equiv> None"
+by (rule flat_interpretation)(simp add: flat_lub_def)
 
 
 abbreviation "tailrec_ord \<equiv> flat_ord undefined"
@@ -281,7 +284,7 @@
 proof -
   have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
     by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
-      (auto intro: step tailrec_admissible)
+      (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
   thus ?thesis using result defined by blast
 qed
 
@@ -293,14 +296,15 @@
   shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
 proof (rule ccpo.admissibleI)
   fix A assume "chain (img_ord f le) A"
-   then have ch': "chain le (f ` A)"
-      by (auto simp: img_ord_def intro: chainI dest: chainD)
+  then have ch': "chain le (f ` A)"
+    by (auto simp: img_ord_def intro: chainI dest: chainD)
+  assume "A \<noteq> {}"
   assume P_A: "\<forall>x\<in>A. P x"
   have "(P o g) (lub (f ` A))" using adm ch'
   proof (rule ccpo.admissibleD)
     fix x assume "x \<in> f ` A"
     with P_A show "(P o g) x" by (auto simp: inj[OF inv])
-  qed
+  qed(simp add: `A \<noteq> {}`)
   thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
 qed
 
@@ -312,9 +316,11 @@
   fix A :: "('b \<Rightarrow> 'a) set"
   assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
   assume ch: "chain (fun_ord le) A"
+  assume "A \<noteq> {}"
+  hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto
   show "\<forall>x. Q x (fun_lub lub A x)"
     unfolding fun_lub_def
-    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch]])
+    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
       (auto simp: Q)
 qed
 
@@ -388,7 +394,7 @@
   assumes defined: "U f x = Some y"
   shows "P x y"
   using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
-  by blast
+  unfolding fun_lub_def flat_lub_def by(auto 9 2)
 
 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
   @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}

--- a/src/HOL/Product_Type.thy	Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Product_Type.thy	Thu Dec 05 09:20:32 2013 +0100
@@ -729,6 +729,9 @@
 lemma split_curry [simp]: "split (curry f) = f"
   by (simp add: curry_def split_def)
 
+lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
+by(simp add: fun_eq_iff)
+
 text {*
   The composition-uncurry combinator.
 *}

--- a/src/HOL/Tools/Function/partial_function.ML	Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Dec 05 09:20:32 2013 +0100
@@ -168,6 +168,9 @@
   simpset_of (put_simpset HOL_basic_ss @{context}
     addsimps [@{thm Product_Type.split_conv}]);
 
+val curry_K_ss =
+  simpset_of (put_simpset HOL_basic_ss @{context}
+    addsimps [@{thm Product_Type.curry_K}]);
 
 (* instantiate generic fixpoint induction and eliminate the canonical assumptions;
   curry induction predicate *)
@@ -181,7 +184,8 @@
     |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
     |> Tactic.rule_by_tactic ctxt
       (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
-       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 4) (* simplify induction step *)
+       THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
+       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
     |> (fn thm => thm OF [mono_thm, f_def])
     |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
          (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}]))