restrict admissibility to non-empty chains to allow more syntax-directed proof rules
authorAndreas Lochbihler
Thu Dec 05 09:20:32 2013 +0100 (2013-12-05)
changeset 546309061af4d5ebc
parent 54629 a692901ecdc2
child 54631 da88a625cce1
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
src/HOL/Complete_Partial_Order.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Partial_Function.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Tue Dec 03 02:51:20 2013 +0100
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Thu Dec 05 09:20:32 2013 +0100
     1.3 @@ -50,6 +50,9 @@
     1.4    obtains "ord x y" | "ord y x"
     1.5  using assms unfolding chain_def by fast
     1.6  
     1.7 +lemma chain_empty: "chain ord {}"
     1.8 +by(simp add: chain_def)
     1.9 +
    1.10  subsection {* Chain-complete partial orders *}
    1.11  
    1.12  text {*
    1.13 @@ -119,6 +122,9 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +lemma bot_in_iterates: "Sup {} \<in> iterates f"
    1.18 +by(auto intro: iterates.Sup simp add: chain_empty)
    1.19 +
    1.20  subsection {* Fixpoint combinator *}
    1.21  
    1.22  definition
    1.23 @@ -162,16 +168,17 @@
    1.24  setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
    1.25  
    1.26  definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.27 -where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    1.28 +where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    1.29  
    1.30  lemma admissibleI:
    1.31 -  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    1.32 +  assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    1.33    shows "ccpo.admissible lub ord P"
    1.34  using assms unfolding ccpo.admissible_def by fast
    1.35  
    1.36  lemma admissibleD:
    1.37    assumes "ccpo.admissible lub ord P"
    1.38    assumes "chain ord A"
    1.39 +  assumes "A \<noteq> {}"
    1.40    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
    1.41    shows "P (lub A)"
    1.42  using assms by (auto simp: ccpo.admissible_def)
    1.43 @@ -181,24 +188,26 @@
    1.44  lemma (in ccpo) fixp_induct:
    1.45    assumes adm: "ccpo.admissible Sup (op \<le>) P"
    1.46    assumes mono: "monotone (op \<le>) (op \<le>) f"
    1.47 +  assumes bot: "P (Sup {})"
    1.48    assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
    1.49    shows "P (fixp f)"
    1.50  unfolding fixp_def using adm chain_iterates[OF mono]
    1.51  proof (rule ccpo.admissibleD)
    1.52 +  show "iterates f \<noteq> {}" using bot_in_iterates by auto
    1.53    fix x assume "x \<in> iterates f"
    1.54    thus "P x"
    1.55      by (induct rule: iterates.induct)
    1.56 -      (auto intro: step ccpo.admissibleD adm)
    1.57 +      (case_tac "M = {}", auto intro: step bot ccpo.admissibleD adm)
    1.58  qed
    1.59  
    1.60  lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
    1.61  unfolding ccpo.admissible_def by simp
    1.62  
    1.63 -lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    1.64 +(*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    1.65  unfolding ccpo.admissible_def chain_def by simp
    1.66 -
    1.67 -lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
    1.68 -by (cases t, simp_all add: admissible_True admissible_False)
    1.69 +*)
    1.70 +lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
    1.71 +by(auto intro: ccpo.admissibleI)
    1.72  
    1.73  lemma admissible_conj:
    1.74    assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
    1.75 @@ -248,15 +257,16 @@
    1.76    shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
    1.77  proof (rule ccpo.admissibleI)
    1.78    fix A :: "'a set" assume A: "chain (op \<le>) A"
    1.79 -  assume "\<forall>x\<in>A. P x \<or> Q x"
    1.80 -  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)"
    1.81 +  assume "A \<noteq> {}"
    1.82 +    and "\<forall>x\<in>A. P x \<or> Q x"
    1.83 +  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)"
    1.84      using chainD[OF A] by blast
    1.85 -  hence "Sup A = Sup {x \<in> A. P x} \<or> Sup A = Sup {x \<in> A. Q x}"
    1.86 -    using admissible_disj_lemma [OF A] by fast
    1.87 +  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}"
    1.88 +    using admissible_disj_lemma [OF A] by blast
    1.89    thus "P (Sup A) \<or> Q (Sup A)"
    1.90      apply (rule disjE, simp_all)
    1.91 -    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
    1.92 -    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
    1.93 +    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp, simp)
    1.94 +    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp, simp)
    1.95      done
    1.96  qed
    1.97  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Dec 03 02:51:20 2013 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 05 09:20:32 2013 +0100
     2.3 @@ -415,6 +415,9 @@
     2.4  definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
     2.5    "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
     2.6  
     2.7 +lemma Heap_lub_empty: "Heap_lub {} = Heap Map.empty"
     2.8 +by(simp add: Heap_lub_def img_lub_def fun_lub_def flat_lub_def)
     2.9 +
    2.10  lemma heap_interpretation: "partial_function_definitions Heap_ord Heap_lub"
    2.11  proof -
    2.12    have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
    2.13 @@ -427,7 +430,8 @@
    2.14  qed
    2.15  
    2.16  interpretation heap!: partial_function_definitions Heap_ord Heap_lub
    2.17 -by (fact heap_interpretation)
    2.18 +  where "Heap_lub {} \<equiv> Heap Map.empty"
    2.19 +by (fact heap_interpretation)(simp add: Heap_lub_empty)
    2.20  
    2.21  lemma heap_step_admissible: 
    2.22    "option.admissible
    2.23 @@ -473,6 +477,7 @@
    2.24    assumes defined: "effect (U f x) h h' r"
    2.25    shows "P x h h' r"
    2.26    using step defined heap.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_heap, of P]
    2.27 +  unfolding effect_def execute.simps
    2.28    by blast
    2.29  
    2.30  declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
     3.1 --- a/src/HOL/Partial_Function.thy	Tue Dec 03 02:51:20 2013 +0100
     3.2 +++ b/src/HOL/Partial_Function.thy	Thu Dec 05 09:20:32 2013 +0100
     3.3 @@ -176,11 +176,12 @@
     3.4    assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
     3.5    assumes inverse: "\<And>f. U (C f) = f"
     3.6    assumes adm: "ccpo.admissible lub_fun le_fun P"
     3.7 +  and bot: "P (\<lambda>_. lub {})"
     3.8    assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
     3.9    shows "P (U f)"
    3.10  unfolding eq inverse
    3.11  apply (rule ccpo.fixp_induct[OF ccpo adm])
    3.12 -apply (insert mono, auto simp: monotone_def fun_ord_def)[1]
    3.13 +apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
    3.14  by (rule_tac f="C x" in step, simp add: inverse)
    3.15  
    3.16  
    3.17 @@ -237,11 +238,13 @@
    3.18  
    3.19  interpretation tailrec!:
    3.20    partial_function_definitions "flat_ord undefined" "flat_lub undefined"
    3.21 -by (rule flat_interpretation)
    3.22 +  where "flat_lub undefined {} \<equiv> undefined"
    3.23 +by (rule flat_interpretation)(simp add: flat_lub_def)
    3.24  
    3.25  interpretation option!:
    3.26    partial_function_definitions "flat_ord None" "flat_lub None"
    3.27 -by (rule flat_interpretation)
    3.28 +  where "flat_lub None {} \<equiv> None"
    3.29 +by (rule flat_interpretation)(simp add: flat_lub_def)
    3.30  
    3.31  
    3.32  abbreviation "tailrec_ord \<equiv> flat_ord undefined"
    3.33 @@ -281,7 +284,7 @@
    3.34  proof -
    3.35    have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
    3.36      by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
    3.37 -      (auto intro: step tailrec_admissible)
    3.38 +      (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def)
    3.39    thus ?thesis using result defined by blast
    3.40  qed
    3.41  
    3.42 @@ -293,14 +296,15 @@
    3.43    shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
    3.44  proof (rule ccpo.admissibleI)
    3.45    fix A assume "chain (img_ord f le) A"
    3.46 -   then have ch': "chain le (f ` A)"
    3.47 -      by (auto simp: img_ord_def intro: chainI dest: chainD)
    3.48 +  then have ch': "chain le (f ` A)"
    3.49 +    by (auto simp: img_ord_def intro: chainI dest: chainD)
    3.50 +  assume "A \<noteq> {}"
    3.51    assume P_A: "\<forall>x\<in>A. P x"
    3.52    have "(P o g) (lub (f ` A))" using adm ch'
    3.53    proof (rule ccpo.admissibleD)
    3.54      fix x assume "x \<in> f ` A"
    3.55      with P_A show "(P o g) x" by (auto simp: inj[OF inv])
    3.56 -  qed
    3.57 +  qed(simp add: `A \<noteq> {}`)
    3.58    thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
    3.59  qed
    3.60  
    3.61 @@ -312,9 +316,11 @@
    3.62    fix A :: "('b \<Rightarrow> 'a) set"
    3.63    assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
    3.64    assume ch: "chain (fun_ord le) A"
    3.65 +  assume "A \<noteq> {}"
    3.66 +  hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto
    3.67    show "\<forall>x. Q x (fun_lub lub A x)"
    3.68      unfolding fun_lub_def
    3.69 -    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch]])
    3.70 +    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty])
    3.71        (auto simp: Q)
    3.72  qed
    3.73  
    3.74 @@ -388,7 +394,7 @@
    3.75    assumes defined: "U f x = Some y"
    3.76    shows "P x y"
    3.77    using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
    3.78 -  by blast
    3.79 +  unfolding fun_lub_def flat_lub_def by(auto 9 2)
    3.80  
    3.81  declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
    3.82    @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
     4.1 --- a/src/HOL/Product_Type.thy	Tue Dec 03 02:51:20 2013 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Thu Dec 05 09:20:32 2013 +0100
     4.3 @@ -729,6 +729,9 @@
     4.4  lemma split_curry [simp]: "split (curry f) = f"
     4.5    by (simp add: curry_def split_def)
     4.6  
     4.7 +lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
     4.8 +by(simp add: fun_eq_iff)
     4.9 +
    4.10  text {*
    4.11    The composition-uncurry combinator.
    4.12  *}
     5.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Dec 03 02:51:20 2013 +0100
     5.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Dec 05 09:20:32 2013 +0100
     5.3 @@ -168,6 +168,9 @@
     5.4    simpset_of (put_simpset HOL_basic_ss @{context}
     5.5      addsimps [@{thm Product_Type.split_conv}]);
     5.6  
     5.7 +val curry_K_ss =
     5.8 +  simpset_of (put_simpset HOL_basic_ss @{context}
     5.9 +    addsimps [@{thm Product_Type.curry_K}]);
    5.10  
    5.11  (* instantiate generic fixpoint induction and eliminate the canonical assumptions;
    5.12    curry induction predicate *)
    5.13 @@ -181,7 +184,8 @@
    5.14      |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
    5.15      |> Tactic.rule_by_tactic ctxt
    5.16        (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
    5.17 -       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 4) (* simplify induction step *)
    5.18 +       THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
    5.19 +       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
    5.20      |> (fn thm => thm OF [mono_thm, f_def])
    5.21      |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
    5.22           (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}]))