admissibility on option type
authorkrauss
Tue May 31 11:11:17 2011 +0200 (2011-05-31)
changeset 430811a39c9898ae6
parent 43080 73a1d6a7ef1d
child 43082 8d0c44de9773
admissibility on option type
src/HOL/Partial_Function.thy
     1.1 --- a/src/HOL/Partial_Function.thy	Mon May 23 21:34:37 2011 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Tue May 31 11:11:17 2011 +0200
     1.3 @@ -23,6 +23,17 @@
     1.4  definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
     1.5  definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
     1.6  
     1.7 +lemma chain_fun: 
     1.8 +  assumes A: "chain (fun_ord ord) A"
     1.9 +  shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    1.10 +proof (rule chainI)
    1.11 +  fix x y assume "x \<in> ?C" "y \<in> ?C"
    1.12 +  then obtain f g where fg: "f \<in> A" "g \<in> A" 
    1.13 +    and [simp]: "x = f a" "y = g a" by blast
    1.14 +  from chainD[OF A fg]
    1.15 +  show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    1.16 +qed
    1.17 +
    1.18  lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
    1.19  by (rule monotoneI) (auto simp: fun_ord_def)
    1.20  
    1.21 @@ -53,17 +64,6 @@
    1.22  proof -
    1.23    interpret partial_function_definitions ord lb by fact
    1.24  
    1.25 -  { fix A a assume A: "chain ?ordf A"
    1.26 -    have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
    1.27 -    proof (rule chainI)
    1.28 -      fix x y assume "x \<in> ?C" "y \<in> ?C"
    1.29 -      then obtain f g where fg: "f \<in> A" "g \<in> A" 
    1.30 -        and [simp]: "x = f a" "y = g a" by blast
    1.31 -      from chainD[OF A fg]
    1.32 -      show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
    1.33 -    qed }
    1.34 -  note chain_fun = this
    1.35 -
    1.36    show ?thesis
    1.37    proof
    1.38      fix x show "?ordf x x"
    1.39 @@ -75,7 +75,7 @@
    1.40    next
    1.41      fix x y assume "?ordf x y" "?ordf y x"
    1.42      thus "x = y" unfolding fun_ord_def
    1.43 -      by (force intro!: ext dest: leq_antisym)
    1.44 +      by (force intro!: dest: leq_antisym)
    1.45    next
    1.46      fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
    1.47      thus "?ordf f (?lubf A)"
    1.48 @@ -129,6 +129,7 @@
    1.49  abbreviation "lub_fun \<equiv> fun_lub lub"
    1.50  abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
    1.51  abbreviation "mono_body \<equiv> monotone le_fun leq"
    1.52 +abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
    1.53  
    1.54  text {* Interpret manually, to avoid flooding everything with facts about
    1.55    orders *}
    1.56 @@ -251,6 +252,43 @@
    1.57    show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
    1.58  qed
    1.59  
    1.60 +lemma flat_lub_in_chain:
    1.61 +  assumes ch: "chain (flat_ord b) A "
    1.62 +  assumes lub: "flat_lub b A = a"
    1.63 +  shows "a = b \<or> a \<in> A"
    1.64 +proof (cases "A \<subseteq> {b}")
    1.65 +  case True
    1.66 +  then have "flat_lub b A = b" unfolding flat_lub_def by simp
    1.67 +  with lub show ?thesis by simp
    1.68 +next
    1.69 +  case False
    1.70 +  then obtain c where "c \<in> A" and "c \<noteq> b" by auto
    1.71 +  { fix z assume "z \<in> A"
    1.72 +    from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b"
    1.73 +      unfolding flat_ord_def using `c \<noteq> b` by auto }
    1.74 +  with False have "A - {b} = {c}" by auto
    1.75 +  with False have "flat_lub b A = c" by (auto simp: flat_lub_def)
    1.76 +  with `c \<in> A` lub show ?thesis by simp
    1.77 +qed
    1.78 +
    1.79 +lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
    1.80 +  (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
    1.81 +proof (rule ccpo.admissibleI[OF option.ccpo])
    1.82 +  fix A :: "('a \<Rightarrow> 'b option) set"
    1.83 +  assume ch: "chain option.le_fun A"
    1.84 +    and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"
    1.85 +  from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun)
    1.86 +  show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y"
    1.87 +  proof (intro allI impI)
    1.88 +    fix x y assume "option.lub_fun A x = Some y"
    1.89 +    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
    1.90 +    have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp
    1.91 +    then have "\<exists>f\<in>A. f x = Some y" by auto
    1.92 +    with IH show "P x y" by auto
    1.93 +  qed
    1.94 +qed
    1.95 +
    1.96 +
    1.97  hide_const (open) chain
    1.98  
    1.99  end