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