src/HOLCF/Lift.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 31076 99fe356cbbc2 child 32149 ef59550a55d3 permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
```     1 (*  Title:      HOLCF/Lift.thy
```
```     2     Author:     Olaf Mueller
```
```     3 *)
```
```     4
```
```     5 header {* Lifting types of class type to flat pcpo's *}
```
```     6
```
```     7 theory Lift
```
```     8 imports Discrete Up Countable
```
```     9 begin
```
```    10
```
```    11 defaultsort type
```
```    12
```
```    13 pcpodef 'a lift = "UNIV :: 'a discr u set"
```
```    14 by simp_all
```
```    15
```
```    16 instance lift :: (finite) finite_po
```
```    17 by (rule typedef_finite_po [OF type_definition_lift])
```
```    18
```
```    19 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
```
```    20
```
```    21 definition
```
```    22   Def :: "'a \<Rightarrow> 'a lift" where
```
```    23   "Def x = Abs_lift (up\<cdot>(Discr x))"
```
```    24
```
```    25 subsection {* Lift as a datatype *}
```
```    26
```
```    27 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
```
```    28 apply (induct y)
```
```    29 apply (rule_tac p=y in upE)
```
```    30 apply (simp add: Abs_lift_strict)
```
```    31 apply (case_tac x)
```
```    32 apply (simp add: Def_def)
```
```    33 done
```
```    34
```
```    35 rep_datatype "\<bottom>\<Colon>'a lift" Def
```
```    36   by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
```
```    37
```
```    38 lemmas lift_distinct1 = lift.distinct(1)
```
```    39 lemmas lift_distinct2 = lift.distinct(2)
```
```    40 lemmas Def_not_UU = lift.distinct(2)
```
```    41 lemmas Def_inject = lift.inject
```
```    42
```
```    43
```
```    44 text {* @{term UU} and @{term Def} *}
```
```    45
```
```    46 lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
```
```    47   by (induct x) simp_all
```
```    48
```
```    49 lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
```
```    50   by (insert Lift_exhaust) blast
```
```    51
```
```    52 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
```
```    53   by (cases x) simp_all
```
```    54
```
```    55 lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
```
```    56   by (cases x) simp_all
```
```    57
```
```    58 text {*
```
```    59   For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
```
```    60   x} by @{text "Def a"} in conclusion. *}
```
```    61
```
```    62 method_setup defined = {*
```
```    63   Scan.succeed (fn ctxt => SIMPLE_METHOD'
```
```    64     (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
```
```    65 *} ""
```
```    66
```
```    67 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
```
```    68   by simp
```
```    69
```
```    70 lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
```
```    71   by simp
```
```    72
```
```    73 lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
```
```    74 by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
```
```    75
```
```    76 lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
```
```    77 by (induct y, simp, simp add: Def_below_Def)
```
```    78
```
```    79
```
```    80 subsection {* Lift is flat *}
```
```    81
```
```    82 instance lift :: (type) flat
```
```    83 proof
```
```    84   fix x y :: "'a lift"
```
```    85   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
```
```    86     by (induct x) auto
```
```    87 qed
```
```    88
```
```    89 text {*
```
```    90   \medskip Two specific lemmas for the combination of LCF and HOL
```
```    91   terms.
```
```    92 *}
```
```    93
```
```    94 lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
```
```    95 by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
```
```    96
```
```    97 lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
```
```    98 by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
```
```    99
```
```   100 subsection {* Further operations *}
```
```   101
```
```   102 definition
```
```   103   flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
```
```   104   "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
```
```   105
```
```   106 definition
```
```   107   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
```
```   108   "flift2 f = (FLIFT x. Def (f x))"
```
```   109
```
```   110 subsection {* Continuity Proofs for flift1, flift2 *}
```
```   111
```
```   112 text {* Need the instance of @{text flat}. *}
```
```   113
```
```   114 lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
```
```   115 apply (induct x)
```
```   116 apply simp
```
```   117 apply simp
```
```   118 apply (rule cont_id [THEN cont2cont_fun])
```
```   119 done
```
```   120
```
```   121 lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
```
```   122 apply (rule flatdom_strict2cont)
```
```   123 apply simp
```
```   124 done
```
```   125
```
```   126 lemma cont_flift1: "cont flift1"
```
```   127 unfolding flift1_def
```
```   128 apply (rule cont2cont_LAM)
```
```   129 apply (rule cont_lift_case2)
```
```   130 apply (rule cont_lift_case1)
```
```   131 done
```
```   132
```
```   133 lemma FLIFT_mono:
```
```   134   "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
```
```   135 apply (rule monofunE [where f=flift1])
```
```   136 apply (rule cont2mono [OF cont_flift1])
```
```   137 apply (simp add: below_fun_ext)
```
```   138 done
```
```   139
```
```   140 lemma cont2cont_flift1 [simp]:
```
```   141   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
```
```   142 apply (rule cont_flift1 [THEN cont2cont_app3])
```
```   143 apply simp
```
```   144 done
```
```   145
```
```   146 lemma cont2cont_lift_case [simp]:
```
```   147   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
```
```   148 apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
```
```   149 apply (simp add: flift1_def cont_lift_case2)
```
```   150 apply simp
```
```   151 done
```
```   152
```
```   153 text {* rewrites for @{term flift1}, @{term flift2} *}
```
```   154
```
```   155 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
```
```   156 by (simp add: flift1_def cont_lift_case2)
```
```   157
```
```   158 lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
```
```   159 by (simp add: flift2_def)
```
```   160
```
```   161 lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
```
```   162 by (simp add: flift1_def cont_lift_case2)
```
```   163
```
```   164 lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
```
```   165 by (simp add: flift2_def)
```
```   166
```
```   167 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
```
```   168 by (erule lift_definedE, simp)
```
```   169
```
```   170 lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
```
```   171 by (cases x, simp_all)
```
```   172
```
```   173 text {*
```
```   174   \medskip Extension of @{text cont_tac} and installation of simplifier.
```
```   175 *}
```
```   176
```
```   177 lemmas cont_lemmas_ext =
```
```   178   cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
```
```   179   cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
```
```   180
```
```   181 ML {*
```
```   182 local
```
```   183   val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext";
```
```   184   val flift1_def = thm "flift1_def";
```
```   185 in
```
```   186
```
```   187 fun cont_tac  i = resolve_tac cont_lemmas2 i;
```
```   188 fun cont_tacR i = REPEAT (cont_tac i);
```
```   189
```
```   190 fun cont_tacRs ss i =
```
```   191   simp_tac ss i THEN
```
```   192   REPEAT (cont_tac i)
```
```   193 end;
```
```   194 *}
```
```   195
```
```   196 subsection {* Lifted countable types are bifinite *}
```
```   197
```
```   198 instantiation lift :: (countable) bifinite
```
```   199 begin
```
```   200
```
```   201 definition
```
```   202   approx_lift_def:
```
```   203     "approx = (\<lambda>n. FLIFT x. if to_nat x < n then Def x else \<bottom>)"
```
```   204
```
```   205 instance proof
```
```   206   fix x :: "'a lift"
```
```   207   show "chain (approx :: nat \<Rightarrow> 'a lift \<rightarrow> 'a lift)"
```
```   208     unfolding approx_lift_def
```
```   209     by (rule chainI, simp add: FLIFT_mono)
```
```   210 next
```
```   211   fix x :: "'a lift"
```
```   212   show "(\<Squnion>i. approx i\<cdot>x) = x"
```
```   213     unfolding approx_lift_def
```
```   214     apply (cases x, simp)
```
```   215     apply (rule thelubI)
```
```   216     apply (rule is_lubI)
```
```   217      apply (rule ub_rangeI, simp)
```
```   218     apply (drule ub_rangeD)
```
```   219     apply (erule rev_below_trans)
```
```   220     apply simp
```
```   221     apply (rule lessI)
```
```   222     done
```
```   223 next
```
```   224   fix i :: nat and x :: "'a lift"
```
```   225   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
```
```   226     unfolding approx_lift_def
```
```   227     by (cases x, simp, simp)
```
```   228 next
```
```   229   fix i :: nat
```
```   230   show "finite {x::'a lift. approx i\<cdot>x = x}"
```
```   231   proof (rule finite_subset)
```
```   232     let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
```
```   233     show "{x::'a lift. approx i\<cdot>x = x} \<subseteq> ?S"
```
```   234       unfolding approx_lift_def
```
```   235       by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
```
```   236     show "finite ?S"
```
```   237       by (simp add: finite_vimageI)
```
```   238   qed
```
```   239 qed
```
```   240
```
```   241 end
```
```   242
```
```   243 end
```