move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
authorAndreas Lochbihler
Mon Sep 02 16:28:11 2013 +0200 (2013-09-02)
changeset 533611cb7d3c0cf31
parent 53358 b46e6cd75dc6
child 53362 735e078a64e7
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Complete_Partial_Order.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Partial_Function.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Sep 01 14:00:05 2013 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Sep 02 16:28:11 2013 +0200
     1.3 @@ -53,13 +53,6 @@
     1.4  (* If the compilation fails with an error "ambiguous implicit values",
     1.5     read \<section>7.1 in the Code Generation Manual *)
     1.6  
     1.7 -class ccpo_linorder = ccpo + linorder
     1.8 -
     1.9 -lemma [code]:
    1.10 -  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    1.11 -    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    1.12 -unfolding admissible_def by blast
    1.13 -
    1.14  lemma [code]:
    1.15    "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    1.16  unfolding gfp_def by blast
     2.1 --- a/src/HOL/Complete_Partial_Order.thy	Sun Sep 01 14:00:05 2013 +0200
     2.2 +++ b/src/HOL/Complete_Partial_Order.thy	Mon Sep 02 16:28:11 2013 +0200
     2.3 @@ -155,67 +155,72 @@
     2.4    qed (auto intro: ccpo_Sup_least)
     2.5  qed
     2.6  
     2.7 +end
     2.8  
     2.9  subsection {* Fixpoint induction *}
    2.10  
    2.11 -definition
    2.12 -  admissible :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    2.13 -where
    2.14 -  "admissible P = (\<forall>A. chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    2.15 +setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
    2.16 +
    2.17 +definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    2.18 +where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
    2.19  
    2.20  lemma admissibleI:
    2.21 -  assumes "\<And>A. chain (op \<le>) A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (Sup A)"
    2.22 -  shows "admissible P"
    2.23 -using assms unfolding admissible_def by fast
    2.24 +  assumes "\<And>A. chain ord A \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
    2.25 +  shows "ccpo.admissible lub ord P"
    2.26 +using assms unfolding ccpo.admissible_def by fast
    2.27  
    2.28  lemma admissibleD:
    2.29 -  assumes "admissible P"
    2.30 -  assumes "chain (op \<le>) A"
    2.31 +  assumes "ccpo.admissible lub ord P"
    2.32 +  assumes "chain ord A"
    2.33    assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
    2.34 -  shows "P (Sup A)"
    2.35 -using assms by (auto simp: admissible_def)
    2.36 +  shows "P (lub A)"
    2.37 +using assms by (auto simp: ccpo.admissible_def)
    2.38  
    2.39 -lemma fixp_induct:
    2.40 -  assumes adm: "admissible P"
    2.41 +setup {* Sign.map_naming Name_Space.parent_path *}
    2.42 +
    2.43 +lemma (in ccpo) fixp_induct:
    2.44 +  assumes adm: "ccpo.admissible Sup (op \<le>) P"
    2.45    assumes mono: "monotone (op \<le>) (op \<le>) f"
    2.46    assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
    2.47    shows "P (fixp f)"
    2.48  unfolding fixp_def using adm chain_iterates[OF mono]
    2.49 -proof (rule admissibleD)
    2.50 +proof (rule ccpo.admissibleD)
    2.51    fix x assume "x \<in> iterates f"
    2.52    thus "P x"
    2.53      by (induct rule: iterates.induct)
    2.54 -      (auto intro: step admissibleD adm)
    2.55 +      (auto intro: step ccpo.admissibleD adm)
    2.56  qed
    2.57  
    2.58 -lemma admissible_True: "admissible (\<lambda>x. True)"
    2.59 -unfolding admissible_def by simp
    2.60 +lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
    2.61 +unfolding ccpo.admissible_def by simp
    2.62  
    2.63 -lemma admissible_False: "\<not> admissible (\<lambda>x. False)"
    2.64 -unfolding admissible_def chain_def by simp
    2.65 +lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
    2.66 +unfolding ccpo.admissible_def chain_def by simp
    2.67  
    2.68 -lemma admissible_const: "admissible (\<lambda>x. t) = t"
    2.69 +lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t) = t"
    2.70  by (cases t, simp_all add: admissible_True admissible_False)
    2.71  
    2.72  lemma admissible_conj:
    2.73 -  assumes "admissible (\<lambda>x. P x)"
    2.74 -  assumes "admissible (\<lambda>x. Q x)"
    2.75 -  shows "admissible (\<lambda>x. P x \<and> Q x)"
    2.76 -using assms unfolding admissible_def by simp
    2.77 +  assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
    2.78 +  assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
    2.79 +  shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
    2.80 +using assms unfolding ccpo.admissible_def by simp
    2.81  
    2.82  lemma admissible_all:
    2.83 -  assumes "\<And>y. admissible (\<lambda>x. P x y)"
    2.84 -  shows "admissible (\<lambda>x. \<forall>y. P x y)"
    2.85 -using assms unfolding admissible_def by fast
    2.86 +  assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
    2.87 +  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
    2.88 +using assms unfolding ccpo.admissible_def by fast
    2.89  
    2.90  lemma admissible_ball:
    2.91 -  assumes "\<And>y. y \<in> A \<Longrightarrow> admissible (\<lambda>x. P x y)"
    2.92 -  shows "admissible (\<lambda>x. \<forall>y\<in>A. P x y)"
    2.93 -using assms unfolding admissible_def by fast
    2.94 +  assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
    2.95 +  shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
    2.96 +using assms unfolding ccpo.admissible_def by fast
    2.97  
    2.98 -lemma chain_compr: "chain (op \<le>) A \<Longrightarrow> chain (op \<le>) {x \<in> A. P x}"
    2.99 +lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
   2.100  unfolding chain_def by fast
   2.101  
   2.102 +context ccpo begin
   2.103 +
   2.104  lemma admissible_disj_lemma:
   2.105    assumes A: "chain (op \<le>)A"
   2.106    assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
   2.107 @@ -238,10 +243,10 @@
   2.108  
   2.109  lemma admissible_disj:
   2.110    fixes P Q :: "'a \<Rightarrow> bool"
   2.111 -  assumes P: "admissible (\<lambda>x. P x)"
   2.112 -  assumes Q: "admissible (\<lambda>x. Q x)"
   2.113 -  shows "admissible (\<lambda>x. P x \<or> Q x)"
   2.114 -proof (rule admissibleI)
   2.115 +  assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
   2.116 +  assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
   2.117 +  shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
   2.118 +proof (rule ccpo.admissibleI)
   2.119    fix A :: "'a set" assume A: "chain (op \<le>) A"
   2.120    assume "\<forall>x\<in>A. P x \<or> Q x"
   2.121    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)"
   2.122 @@ -250,8 +255,8 @@
   2.123      using admissible_disj_lemma [OF A] by fast
   2.124    thus "P (Sup A) \<or> Q (Sup A)"
   2.125      apply (rule disjE, simp_all)
   2.126 -    apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp)
   2.127 -    apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp)
   2.128 +    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp)
   2.129 +    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp)
   2.130      done
   2.131  qed
   2.132  
   2.133 @@ -271,6 +276,6 @@
   2.134      by (rule fixp_lowerbound [OF f'], subst lfp_unfold [OF f], rule order_refl)
   2.135  qed
   2.136  
   2.137 -hide_const (open) iterates fixp admissible
   2.138 +hide_const (open) iterates fixp
   2.139  
   2.140  end
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Sep 01 14:00:05 2013 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 02 16:28:11 2013 +0200
     3.3 @@ -432,7 +432,7 @@
     3.4  lemma heap_step_admissible: 
     3.5    "option.admissible
     3.6        (\<lambda>f:: 'a => ('b * 'c) option. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r)"
     3.7 -proof (rule ccpo.admissibleI[OF option.ccpo])
     3.8 +proof (rule ccpo.admissibleI)
     3.9    fix A :: "('a \<Rightarrow> ('b * 'c) option) set"
    3.10    assume ch: "Complete_Partial_Order.chain option.le_fun A"
    3.11      and IH: "\<forall>f\<in>A. \<forall>h h' r. f h = Some (r, h') \<longrightarrow> P x h h' r"
     4.1 --- a/src/HOL/Partial_Function.thy	Sun Sep 01 14:00:05 2013 +0200
     4.2 +++ b/src/HOL/Partial_Function.thy	Mon Sep 02 16:28:11 2013 +0200
     4.3 @@ -250,7 +250,7 @@
     4.4  lemma tailrec_admissible:
     4.5    "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord)
     4.6       (\<lambda>a. \<forall>x. a x \<noteq> undefined \<longrightarrow> P x (a x))"
     4.7 -proof(intro ccpo.admissibleI[OF tailrec.ccpo] strip)
     4.8 +proof(intro ccpo.admissibleI strip)
     4.9    fix A x
    4.10    assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A"
    4.11      and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> undefined \<longrightarrow> P x (f x)"
    4.12 @@ -290,13 +290,13 @@
    4.13    assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
    4.14    assumes inv: "\<And>x. f (g x) = x"
    4.15    shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P"
    4.16 -proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_image, fact pfun, fact inj, fact inv)
    4.17 +proof (rule ccpo.admissibleI)
    4.18    fix A assume "chain (img_ord f le) A"
    4.19     then have ch': "chain le (f ` A)"
    4.20        by (auto simp: img_ord_def intro: chainI dest: chainD)
    4.21    assume P_A: "\<forall>x\<in>A. P x"
    4.22 -  have "(P o g) (lub (f ` A))"
    4.23 -  proof (rule ccpo.admissibleD[OF ccpo, OF pfun adm ch'])
    4.24 +  have "(P o g) (lub (f ` A))" using adm ch'
    4.25 +  proof (rule ccpo.admissibleD)
    4.26      fix x assume "x \<in> f ` A"
    4.27      with P_A show "(P o g) x" by (auto simp: inj[OF inv])
    4.28    qed
    4.29 @@ -307,13 +307,13 @@
    4.30    assumes pfun: "partial_function_definitions le lub"
    4.31    assumes adm: "\<And>x. ccpo.admissible lub le (Q x)"
    4.32    shows "ccpo.admissible  (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))"
    4.33 -proof (rule ccpo.admissibleI, rule ccpo, rule partial_function_lift, rule pfun)
    4.34 +proof (rule ccpo.admissibleI)
    4.35    fix A :: "('b \<Rightarrow> 'a) set"
    4.36    assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)"
    4.37    assume ch: "chain (fun_ord le) A"
    4.38    show "\<forall>x. Q x (fun_lub lub A x)"
    4.39      unfolding fun_lub_def
    4.40 -    by (rule allI, rule ccpo.admissibleD[OF ccpo, OF pfun adm chain_fun[OF ch]])
    4.41 +    by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch]])
    4.42        (auto simp: Q)
    4.43  qed
    4.44  
    4.45 @@ -360,7 +360,7 @@
    4.46  
    4.47  lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option).
    4.48    (\<forall>x y. f x = Some y \<longrightarrow> P x y))"
    4.49 -proof (rule ccpo.admissibleI[OF option.ccpo])
    4.50 +proof (rule ccpo.admissibleI)
    4.51    fix A :: "('a \<Rightarrow> 'b option) set"
    4.52    assume ch: "chain option.le_fun A"
    4.53      and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y"