# HG changeset patch # User Andreas Lochbihler # Date 1386231632 -3600 # Node ID 9061af4d5ebcf78fe4cf67515614ebba7b24593b # Parent a692901ecdc2ed2ff1b85e81b6af2acb48ec667e restrict admissibility to non-empty chains to allow more syntax-directed proof rules diff -r a692901ecdc2 -r 9061af4d5ebc src/HOL/Complete_Partial_Order.thy --- 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 {} \ 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 \ 'a) \ ('a \ 'a \ bool) \ ('a \ bool) \ bool" -where "admissible lub ord P = (\A. chain ord A \ (\x\A. P x) \ P (lub A))" +where "admissible lub ord P = (\A. chain ord A \ (A \ {}) \ (\x\A. P x) \ P (lub A))" lemma admissibleI: - assumes "\A. chain ord A \ \x\A. P x \ P (lub A)" + assumes "\A. chain ord A \ A \ {} \ \x\A. P x \ 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 \ {}" assumes "\x. x \ A \ 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 \) P" assumes mono: "monotone (op \) (op \) f" + assumes bot: "P (Sup {})" assumes step: "\x. P x \ P (f x)" shows "P (fixp f)" unfolding fixp_def using adm chain_iterates[OF mono] proof (rule ccpo.admissibleD) + show "iterates f \ {}" using bot_in_iterates by auto fix x assume "x \ 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 (\x. True)" unfolding ccpo.admissible_def by simp -lemma admissible_False: "\ ccpo.admissible lub ord (\x. False)" +(*lemma admissible_False: "\ ccpo.admissible lub ord (\x. False)" unfolding ccpo.admissible_def chain_def by simp - -lemma admissible_const: "ccpo.admissible lub ord (\x. t) = t" -by (cases t, simp_all add: admissible_True admissible_False) +*) +lemma admissible_const: "ccpo.admissible lub ord (\x. t)" +by(auto intro: ccpo.admissibleI) lemma admissible_conj: assumes "ccpo.admissible lub ord (\x. P x)" @@ -248,15 +257,16 @@ shows "ccpo.admissible Sup (op \) (\x. P x \ Q x)" proof (rule ccpo.admissibleI) fix A :: "'a set" assume A: "chain (op \) A" - assume "\x\A. P x \ Q x" - hence "(\x\A. \y\A. x \ y \ P y) \ (\x\A. \y\A. x \ y \ Q y)" + assume "A \ {}" + and "\x\A. P x \ Q x" + hence "(\x\A. P x) \ (\x\A. \y\A. x \ y \ P y) \ (\x\A. Q x) \ (\x\A. \y\A. x \ y \ Q y)" using chainD[OF A] by blast - hence "Sup A = Sup {x \ A. P x} \ Sup A = Sup {x \ A. Q x}" - using admissible_disj_lemma [OF A] by fast + hence "(\x. x \ A \ P x) \ Sup A = Sup {x \ A. P x} \ (\x. x \ A \ Q x) \ Sup A = Sup {x \ A. Q x}" + using admissible_disj_lemma [OF A] by blast thus "P (Sup A) \ 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 diff -r a692901ecdc2 -r 9061af4d5ebc src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ '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 {} \ 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} diff -r a692901ecdc2 -r 9061af4d5ebc src/HOL/Partial_Function.thy --- 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 \ C (fixp_fun (\f. U (F (C f))))" assumes inverse: "\f. U (C f) = f" assumes adm: "ccpo.admissible lub_fun le_fun P" + and bot: "P (\_. lub {})" assumes step: "\f. P (U f) \ 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 {} \ 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 {} \ None" +by (rule flat_interpretation)(simp add: flat_lub_def) abbreviation "tailrec_ord \ flat_ord undefined" @@ -281,7 +284,7 @@ proof - have "\x y. U f x = y \ y \ c \ 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 \ {}" assume P_A: "\x\A. P x" have "(P o g) (lub (f ` A))" using adm ch' proof (rule ccpo.admissibleD) fix x assume "x \ f ` A" with P_A show "(P o g) x" by (auto simp: inj[OF inv]) - qed + qed(simp add: `A \ {}`) thus "P (img_lub f g lub A)" unfolding img_lub_def by simp qed @@ -312,9 +316,11 @@ fix A :: "('b \ 'a) set" assume Q: "\f\A. \x. Q x (f x)" assume ch: "chain (fun_ord le) A" + assume "A \ {}" + hence non_empty: "\a. {y. \f\A. y = f a} \ {}" by auto show "\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} diff -r a692901ecdc2 -r 9061af4d5ebc src/HOL/Product_Type.thy --- 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 (\x. c) = (\x y. c)" +by(simp add: fun_eq_iff) + text {* The composition-uncurry combinator. *} diff -r a692901ecdc2 -r 9061af4d5ebc src/HOL/Tools/Function/partial_function.ML --- 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}]))