src/HOL/IMP/Abs_State.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61430 1efe2f3728a6
child 67399 eab6ce8368fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_State
     4 imports Abs_Int0
     5 begin
     6 
     7 type_synonym 'a st_rep = "(vname * 'a) list"
     8 
     9 fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
    10 "fun_rep [] = (\<lambda>x. \<top>)" |
    11 "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
    12 
    13 lemma fun_rep_map_of[code]: --"original def is too slow"
    14   "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
    15 by(induction ps rule: fun_rep.induct) auto
    16 
    17 definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
    18 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
    19 
    20 hide_type st  --"hide previous def to avoid long names"
    21 declare [[typedef_overloaded]] --"allow quotient types to depend on classes"
    22 
    23 quotient_type 'a st = "('a::top) st_rep" / eq_st
    24 morphisms rep_st St
    25 by (metis eq_st_def equivpI reflpI sympI transpI)
    26 
    27 lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
    28   is "\<lambda>ps x a. (x,a)#ps"
    29 by(auto simp: eq_st_def)
    30 
    31 lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
    32 by(simp add: eq_st_def)
    33 
    34 definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
    35 "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
    36 
    37 definition "show_acom C = map_acom (map_option (show_st (vars(strip C)))) C"
    38 definition "show_acom_opt = map_option show_acom"
    39 
    40 lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    41 by transfer auto
    42 
    43 definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
    44 "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
    45 
    46 instantiation st :: (order_top) order
    47 begin
    48 
    49 definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
    50 "less_eq_st_rep ps1 ps2 =
    51   ((\<forall>x \<in> set(map fst ps1) \<union> set(map fst ps2). fun_rep ps1 x \<le> fun_rep ps2 x))"
    52 
    53 lemma less_eq_st_rep_iff:
    54   "less_eq_st_rep r1 r2 = (\<forall>x. fun_rep r1 x \<le> fun_rep r2 x)"
    55 apply(auto simp: less_eq_st_rep_def fun_rep_map_of split: option.split)
    56 apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
    57 apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
    58 done
    59 
    60 corollary less_eq_st_rep_iff_fun:
    61   "less_eq_st_rep r1 r2 = (fun_rep r1 \<le> fun_rep r2)"
    62 by (metis less_eq_st_rep_iff le_fun_def)
    63 
    64 lift_definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" is less_eq_st_rep
    65 by(auto simp add: eq_st_def less_eq_st_rep_iff)
    66 
    67 definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
    68 
    69 instance
    70 proof (standard, goal_cases)
    71   case 1 show ?case by(rule less_st_def)
    72 next
    73   case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
    74 next
    75   case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
    76 next
    77   case 4 thus ?case
    78     by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
    79 qed
    80 
    81 end
    82 
    83 lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
    84 by transfer (rule less_eq_st_rep_iff)
    85 
    86 fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
    87 "map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
    88 "map2_st_rep f ((x,y)#ps1) ps2 =
    89   (let y2 = fun_rep ps2 x
    90    in (x,f y y2) # map2_st_rep f ps1 ps2)"
    91 
    92 lemma fun_rep_map2_rep[simp]: "f \<top> \<top> = \<top> \<Longrightarrow>
    93   fun_rep (map2_st_rep f ps1 ps2) = (\<lambda>x. f (fun_rep ps1 x) (fun_rep ps2 x))"
    94 apply(induction f ps1 ps2 rule: map2_st_rep.induct)
    95 apply(simp add: fun_rep_map_of map_of_map fun_eq_iff split: option.split)
    96 apply(fastforce simp: fun_rep_map_of fun_eq_iff split:option.splits)
    97 done
    98 
    99 instantiation st :: (semilattice_sup_top) semilattice_sup_top
   100 begin
   101 
   102 lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
   103 by (simp add: eq_st_def)
   104 
   105 lift_definition top_st :: "'a st" is "[]" .
   106 
   107 instance
   108 proof (standard, goal_cases)
   109   case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
   110 next
   111   case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
   112 next
   113   case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
   114 next
   115   case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
   116 qed
   117 
   118 end
   119 
   120 lemma fun_top: "fun \<top> = (\<lambda>x. \<top>)"
   121 by transfer simp
   122 
   123 lemma mono_update[simp]:
   124   "a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
   125 by transfer (auto simp add: less_eq_st_rep_def)
   126 
   127 lemma mono_fun: "S1 \<le> S2 \<Longrightarrow> fun S1 x \<le> fun S2 x"
   128 by transfer (simp add: less_eq_st_rep_iff)
   129 
   130 locale Gamma_semilattice = Val_semilattice where \<gamma>=\<gamma>
   131   for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
   132 begin
   133 
   134 abbreviation \<gamma>\<^sub>s :: "'av st \<Rightarrow> state set"
   135 where "\<gamma>\<^sub>s == \<gamma>_st \<gamma>"
   136 
   137 abbreviation \<gamma>\<^sub>o :: "'av st option \<Rightarrow> state set"
   138 where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>s"
   139 
   140 abbreviation \<gamma>\<^sub>c :: "'av st option acom \<Rightarrow> state set acom"
   141 where "\<gamma>\<^sub>c == map_acom \<gamma>\<^sub>o"
   142 
   143 lemma gamma_s_top[simp]: "\<gamma>\<^sub>s \<top> = UNIV"
   144 by(auto simp: \<gamma>_st_def fun_top)
   145 
   146 lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o \<top> = UNIV"
   147 by (simp add: top_option_def)
   148 
   149 lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^sub>s f \<subseteq> \<gamma>\<^sub>s g"
   150 by(simp add:\<gamma>_st_def le_st_iff subset_iff) (metis mono_gamma subsetD)
   151 
   152 lemma mono_gamma_o:
   153   "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^sub>o S1 \<subseteq> \<gamma>\<^sub>o S2"
   154 by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
   155 
   156 lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^sub>c C1 \<le> \<gamma>\<^sub>c C2"
   157 by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
   158 
   159 lemma in_gamma_option_iff:
   160   "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
   161 by (cases u) auto
   162 
   163 end
   164 
   165 end