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