src/HOL/IMP/Abs_State.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 45623 f682f3f7b726
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@45111
     1
(* Author: Tobias Nipkow *)
nipkow@45111
     2
nipkow@45111
     3
theory Abs_State
nipkow@45111
     4
imports Abs_Int0_fun
nipkow@45111
     5
  "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
nipkow@45111
     6
  (* Library import merely to allow string lists to be sorted for output *)
nipkow@45111
     7
begin
nipkow@45111
     8
nipkow@45111
     9
subsection "Abstract State with Computable Ordering"
nipkow@45111
    10
nipkow@45111
    11
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
nipkow@45111
    12
nipkow@45212
    13
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
nipkow@45111
    14
nipkow@45111
    15
fun "fun" where "fun (FunDom f _) = f"
nipkow@45111
    16
fun dom where "dom (FunDom _ A) = A"
nipkow@45111
    17
nipkow@45111
    18
definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
nipkow@45111
    19
nipkow@45111
    20
definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
nipkow@45111
    21
nipkow@45111
    22
fun show_st_up where
nipkow@45111
    23
"show_st_up Bot = Bot" |
nipkow@45111
    24
"show_st_up (Up S) = Up(show_st S)"
nipkow@45111
    25
nipkow@45111
    26
definition "show_acom = map_acom show_st_up"
nipkow@45127
    27
definition "show_acom_opt = Option.map show_acom"
nipkow@45111
    28
nipkow@45111
    29
definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
nipkow@45111
    30
nipkow@45111
    31
definition "update F x y =
nipkow@45111
    32
  FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
nipkow@45111
    33
nipkow@45111
    34
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
nipkow@45111
    35
by(rule ext)(auto simp: lookup_def update_def)
nipkow@45111
    36
nipkow@45111
    37
definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"
nipkow@45111
    38
nipkow@45111
    39
instantiation st :: (SL_top) SL_top
nipkow@45111
    40
begin
nipkow@45111
    41
nipkow@45111
    42
definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
nipkow@45111
    43
nipkow@45111
    44
definition
nipkow@45111
    45
"join_st F G =
nipkow@45111
    46
 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
nipkow@45111
    47
nipkow@45111
    48
definition "\<top> = FunDom (\<lambda>x. \<top>) []"
nipkow@45111
    49
nipkow@45111
    50
instance
nipkow@45111
    51
proof
nipkow@45111
    52
  case goal2 thus ?case
nipkow@45111
    53
    apply(auto simp: le_st_def)
nipkow@45111
    54
    by (metis lookup_def preord_class.le_trans top)
nipkow@45111
    55
qed (auto simp: le_st_def lookup_def join_st_def Top_st_def)
nipkow@45111
    56
nipkow@45111
    57
end
nipkow@45111
    58
nipkow@45111
    59
lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x"
nipkow@45111
    60
by(auto simp add: lookup_def le_st_def)
nipkow@45111
    61
nipkow@45111
    62
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
nipkow@45111
    63
by(auto simp add: le_st_def lookup_def update_def)
nipkow@45111
    64
nipkow@45127
    65
context Val_abs
nipkow@45111
    66
begin
nipkow@45111
    67
nipkow@45127
    68
abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
nipkow@45111
    69
"s <:f S == s \<in> rep_st rep S"
nipkow@45111
    70
nipkow@45111
    71
notation fun_in_rep (infix "<:\<^sub>f" 50)
nipkow@45111
    72
nipkow@45111
    73
lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
nipkow@45111
    74
apply(auto simp add: rep_st_def le_st_def dest: le_rep)
nipkow@45111
    75
by (metis in_rep_Top le_rep lookup_def subsetD)
nipkow@45111
    76
nipkow@45127
    77
abbreviation in_rep_up :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
nipkow@45111
    78
where "s <:up S == s : rep_up (rep_st rep) S"
nipkow@45111
    79
nipkow@45111
    80
notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)
nipkow@45111
    81
nipkow@45111
    82
lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
nipkow@45111
    83
by (cases S) (auto intro:fun_in_rep_le)
nipkow@45111
    84
nipkow@45111
    85
lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
nipkow@45111
    86
by (cases u) auto
nipkow@45111
    87
nipkow@45111
    88
lemma in_rep_Top_fun: "s <:f \<top>"
nipkow@45111
    89
by(simp add: rep_st_def lookup_def Top_st_def)
nipkow@45111
    90
nipkow@45111
    91
lemma in_rep_Top_up: "s <:up \<top>"
nipkow@45111
    92
by(simp add: Top_up_def in_rep_Top_fun)
nipkow@45111
    93
nipkow@45111
    94
end
nipkow@45111
    95
nipkow@45111
    96
end