added rudimentary induction rule for partial_function (heap)
authorkrauss
Fri Mar 22 00:39:16 2013 +0100 (2013-03-22)
changeset 51485637aa1649ac7
parent 51484 49eb8d73ae10
child 51486 0a0c9a45d294
added rudimentary induction rule for partial_function (heap)
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Partial_Function.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Mar 22 00:39:14 2013 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Mar 22 00:39:16 2013 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4    using assms by (simp add: bind_def)
     1.5  
     1.6  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
     1.7 -  by (rule Heap_eqI) (simp add: execute_bind execute_simps)
     1.8 +  by (rule Heap_eqI) (simp add: execute_simps)
     1.9  
    1.10  lemma bind_return [simp]: "f \<guillemotright>= return = f"
    1.11    by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
    1.12 @@ -417,7 +417,7 @@
    1.13  definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
    1.14    "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
    1.15  
    1.16 -interpretation heap!: partial_function_definitions Heap_ord Heap_lub
    1.17 +lemma heap_interpretation: "partial_function_definitions Heap_ord Heap_lub"
    1.18  proof -
    1.19    have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
    1.20      by (rule partial_function_lift) (rule flat_interpretation)
    1.21 @@ -428,8 +428,57 @@
    1.22      by (simp only: Heap_ord_def Heap_lub_def)
    1.23  qed
    1.24  
    1.25 +interpretation heap!: partial_function_definitions Heap_ord Heap_lub
    1.26 +by (fact heap_interpretation)
    1.27 +
    1.28 +lemma heap_step_admissible: 
    1.29 +  "option.admissible
    1.30 +      (\<lambda>f:: 'a => ('b * 'c) option. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r)"
    1.31 +proof (rule ccpo.admissibleI[OF option.ccpo])
    1.32 +  fix A :: "('a \<Rightarrow> ('b * 'c) option) set"
    1.33 +  assume ch: "Complete_Partial_Order.chain option.le_fun A"
    1.34 +    and IH: "\<forall>f\<in>A. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r"
    1.35 +  from ch have ch': "\<And>x. Complete_Partial_Order.chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
    1.36 +  show "\<forall>h h' r. option.lub_fun A h = Some (r, h') \<longrightarrow> P x h h' r"
    1.37 +  proof (intro allI impI)
    1.38 +    fix h h' r assume "option.lub_fun A h = Some (r, h')"
    1.39 +    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
    1.40 +    have "Some (r, h') \<in> {y. \<exists>f\<in>A. y = f h}" by simp
    1.41 +    then have "\<exists>f\<in>A. f h = Some (r, h')" by auto
    1.42 +    with IH show "P x h h' r" by auto
    1.43 +  qed
    1.44 +qed
    1.45 +
    1.46 +lemma admissible_heap: 
    1.47 +  "heap.admissible (\<lambda>f. \<forall>x h h' r. effect (f x) h h' r \<longrightarrow> P x h h' r)"
    1.48 +proof (rule admissible_fun[OF heap_interpretation])
    1.49 +  fix x
    1.50 +  show "ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r. effect a h h' r \<longrightarrow> P x h h' r)"
    1.51 +    unfolding Heap_ord_def Heap_lub_def
    1.52 +  proof (intro admissible_image partial_function_lift flat_interpretation)
    1.53 +    show "option.admissible ((\<lambda>a. \<forall>h h' r. effect a h h' r \<longrightarrow> P x h h' r) \<circ> Heap)"
    1.54 +      unfolding comp_def effect_def execute.simps
    1.55 +      by (rule heap_step_admissible)
    1.56 +  qed (auto simp add: Heap_eqI)
    1.57 +qed
    1.58 +
    1.59 +lemma fixp_induct_heap:
    1.60 +  fixes F :: "'c \<Rightarrow> 'c" and
    1.61 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a Heap" and
    1.62 +    C :: "('b \<Rightarrow> 'a Heap) \<Rightarrow> 'c" and
    1.63 +    P :: "'b \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
    1.64 +  assumes mono: "\<And>x. monotone (fun_ord Heap_ord) Heap_ord (\<lambda>f. U (F (C f)) x)"
    1.65 +  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub Heap_lub) (fun_ord Heap_ord) (\<lambda>f. U (F (C f))))"
    1.66 +  assumes inverse2: "\<And>f. U (C f) = f"
    1.67 +  assumes step: "\<And>f x h h' r. (\<And>x h h' r. effect (U f x) h h' r \<Longrightarrow> P x h h' r) 
    1.68 +    \<Longrightarrow> effect (U (F f) x) h h' r \<Longrightarrow> P x h h' r"
    1.69 +  assumes defined: "effect (U f x) h h' r"
    1.70 +  shows "P x h h' r"
    1.71 +  using step defined heap.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_heap, of P]
    1.72 +  by blast
    1.73 +
    1.74  declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
    1.75 -  @{term heap.mono_body} @{thm heap.fixp_rule_uc} NONE *}
    1.76 +  @{term heap.mono_body} @{thm heap.fixp_rule_uc} (SOME @{thm fixp_induct_heap}) *}
    1.77  
    1.78  
    1.79  abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
     2.1 --- a/src/HOL/Partial_Function.thy	Fri Mar 22 00:39:14 2013 +0100
     2.2 +++ b/src/HOL/Partial_Function.thy	Fri Mar 22 00:39:16 2013 +0100
     2.3 @@ -284,6 +284,39 @@
     2.4    thus ?thesis using result defined by blast
     2.5  qed
     2.6  
     2.7 +lemma admissible_image:
     2.8 +  assumes pfun: "partial_function_definitions le lub"
     2.9 +  assumes adm: "ccpo.admissible lub le (P o g)"
    2.10 +  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
    2.11 +  assumes inv: "\<And>x. f (g x) = x"
    2.12 +  shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
    2.13 +proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_image, fact pfun, fact inj, fact inv)
    2.14 +  fix A assume "chain (img_ord f le) A"
    2.15 +   then have ch': "chain le (f ` A)"
    2.16 +      by (auto simp: img_ord_def intro: chainI dest: chainD)
    2.17 +  assume P_A: "\<forall>x\<in>A. P x"
    2.18 +  have "(P o g) (lub (f ` A))"
    2.19 +  proof (rule ccpo.admissibleD[OF ccpo, OF pfun adm ch'])
    2.20 +    fix x assume "x \<in> f ` A"
    2.21 +    with P_A show "(P o g) x" by (auto simp: inj[OF inv])
    2.22 +  qed
    2.23 +  thus "P (img_lub f g lub A)" unfolding img_lub_def by simp
    2.24 +qed
    2.25 +
    2.26 +lemma admissible_fun:
    2.27 +  assumes pfun: "partial_function_definitions le lub"
    2.28 +  assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
    2.29 +  shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
    2.30 +proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_lift, rule pfun)
    2.31 +  fix A :: "('b \<Rightarrow> 'a) set"
    2.32 +  assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
    2.33 +  assume ch: "chain (fun_ord le) A"
    2.34 +  show "\<forall>x. Q x (fun_lub lub A x)"
    2.35 +    unfolding fun_lub_def
    2.36 +    by (rule allI, rule ccpo.admissibleD[OF ccpo, OF pfun adm chain_fun[OF ch]])
    2.37 +      (auto simp: Q)
    2.38 +qed
    2.39 +
    2.40  
    2.41  abbreviation "option_ord \<equiv> flat_ord None"
    2.42  abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"