author krauss Tue May 31 11:11:17 2011 +0200 (2011-05-31) changeset 43081 1a39c9898ae6 parent 43080 73a1d6a7ef1d child 43082 8d0c44de9773
admissibility on option type
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.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.21 @@ -53,17 +64,6 @@
1.22  proof -
1.23    interpret partial_function_definitions ord lb by fact
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.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.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.99  end