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