src/HOL/IMP/Abs_State.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46346 10c18630612a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     2
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     3
theory Abs_State
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     4
imports Abs_Int0_fun
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     5
  "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     6
  (* Library import merely to allow string lists to be sorted for output *)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     7
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     8
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     9
subsection "Abstract State with Computable Ordering"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    10
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    11
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    12
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45127
diff changeset
    13
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    14
46334
nipkow
parents: 46063
diff changeset
    15
fun "fun" where "fun (FunDom f xs) = f"
nipkow
parents: 46063
diff changeset
    16
fun dom where "dom (FunDom f xs) = xs"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    17
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    18
definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    19
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    20
definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    21
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    22
definition "show_acom = map_acom (Option.map show_st)"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    23
definition "show_acom_opt = Option.map show_acom"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    24
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    25
definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    26
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    27
definition "update F x y =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    28
  FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    29
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    30
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    31
by(rule ext)(auto simp: lookup_def update_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    32
46039
nipkow
parents: 45623
diff changeset
    33
definition "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(lookup F x)}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    34
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    35
instantiation st :: (SL_top) SL_top
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    36
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    37
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    39
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
definition
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    41
"join_st F G =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    42
 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    43
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    44
definition "\<top> = FunDom (\<lambda>x. \<top>) []"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    45
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    47
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    48
  case goal2 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    49
    apply(auto simp: le_st_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
    by (metis lookup_def preord_class.le_trans top)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
qed (auto simp: le_st_def lookup_def join_st_def Top_st_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    52
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    53
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    54
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    55
lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    56
by(auto simp add: lookup_def le_st_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    57
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    59
by(auto simp add: le_st_def lookup_def update_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    60
46346
10c18630612a removed duplicate definitions that made locale inconsistent
nipkow
parents: 46334
diff changeset
    61
locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    62
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    63
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
    64
abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
46039
nipkow
parents: 45623
diff changeset
    65
where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    66
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
    67
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
46039
nipkow
parents: 45623
diff changeset
    68
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    69
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
    70
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
46039
nipkow
parents: 45623
diff changeset
    71
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    72
46039
nipkow
parents: 45623
diff changeset
    73
lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
nipkow
parents: 45623
diff changeset
    74
by(auto simp: Top_st_def \<gamma>_st_def lookup_def)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    75
46039
nipkow
parents: 45623
diff changeset
    76
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    77
by (simp add: Top_option_def)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    78
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    79
(* FIXME (maybe also le \<rightarrow> sqle?) *)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    80
46039
nipkow
parents: 45623
diff changeset
    81
lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
nipkow
parents: 45623
diff changeset
    82
apply(simp add:\<gamma>_st_def subset_iff lookup_def le_st_def split: if_splits)
nipkow
parents: 45623
diff changeset
    83
by (metis UNIV_I mono_gamma gamma_Top subsetD)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    84
46039
nipkow
parents: 45623
diff changeset
    85
lemma mono_gamma_o:
nipkow
parents: 45623
diff changeset
    86
  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'"
nipkow
parents: 45623
diff changeset
    87
by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    88
46039
nipkow
parents: 45623
diff changeset
    89
lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
nipkow
parents: 45623
diff changeset
    90
by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45212
diff changeset
    91
46039
nipkow
parents: 45623
diff changeset
    92
lemma in_gamma_option_iff:
nipkow
parents: 45623
diff changeset
    93
  "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    94
by (cases u) auto
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    95
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    96
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    97
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    98
end