src/HOL/IMP/Abs_State.thy
changeset 51359 00b45c7e831f
parent 51036 e7b54119c436
child 51389 8a9f0503b1c0
     1.1 --- a/src/HOL/IMP/Abs_State.thy	Wed Mar 06 14:10:07 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_State.thy	Wed Mar 06 16:10:56 2013 +0100
     1.3 @@ -60,21 +60,21 @@
     1.4  end
     1.5  
     1.6  class semilatticeL = join + L +
     1.7 -fixes top :: "vname set \<Rightarrow> 'a"
     1.8 -assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
     1.9 -and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
    1.10 -and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    1.11 -and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
    1.12 -and top_in_L[simp]: "top X \<in> L X"
    1.13 +fixes Top :: "vname set \<Rightarrow> 'a"
    1.14 +assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
    1.15 +and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
    1.16 +and join_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
    1.17 +and Top[simp]: "x \<in> L X \<Longrightarrow> x \<le> Top X"
    1.18 +and Top_in_L[simp]: "Top X \<in> L X"
    1.19  and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
    1.20  
    1.21 -notation (input) top ("\<top>\<^bsub>_\<^esub>")
    1.22 -notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
    1.23 +notation (input) Top ("\<top>\<^bsub>_\<^esub>")
    1.24 +notation (latex output) Top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
    1.25  
    1.26  instantiation option :: (semilatticeL)semilatticeL
    1.27  begin
    1.28  
    1.29 -definition top_option where "top c = Some(top c)"
    1.30 +definition Top_option where "Top c = Some(Top c)"
    1.31  
    1.32  instance proof
    1.33    case goal1 thus ?case by(cases x, simp, cases y, simp_all)
    1.34 @@ -83,9 +83,9 @@
    1.35  next
    1.36    case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
    1.37  next
    1.38 -  case goal4 thus ?case by(cases x, simp_all add: top_option_def)
    1.39 +  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
    1.40  next
    1.41 -  case goal5 thus ?case by(simp add: top_option_def)
    1.42 +  case goal5 thus ?case by(simp add: Top_option_def)
    1.43  next
    1.44    case goal6 thus ?case by(simp add: L_option_def split: option.splits)
    1.45  qed
    1.46 @@ -97,41 +97,77 @@
    1.47  
    1.48  hide_type  st  --"to avoid long names"
    1.49  
    1.50 -text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    1.51 +text{* A concrete type of state with computable @{text"\<le>"}: *}
    1.52 +
    1.53 +fun st :: "(vname \<Rightarrow> 'a) * vname set \<Rightarrow> bool" where
    1.54 +"st (f,X) = (\<forall>x. x \<notin> X \<longrightarrow> f x = undefined)"
    1.55  
    1.56 -datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
    1.57 +typedef 'a st = "{p :: (vname \<Rightarrow> 'a) * vname set. st p}"
    1.58 +proof
    1.59 +  show "(\<lambda>x. undefined,{}) \<in> {p. st p}" by simp
    1.60 +qed
    1.61 +
    1.62 +setup_lifting type_definition_st
    1.63 +
    1.64 +lift_definition St :: "(vname \<Rightarrow> 'a) \<Rightarrow> vname set \<Rightarrow> 'a st" is
    1.65 +  "\<lambda>f X. (\<lambda>x. if x \<in> X then f x else undefined, X)"
    1.66 +by(simp)
    1.67  
    1.68 -fun "fun" where "fun (FunDom f X) = f"
    1.69 -fun dom where "dom (FunDom f X) = X"
    1.70 +lift_definition update :: "'a st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st" is
    1.71 +  "\<lambda>(f,X) x a. (f(x := a), insert x X)"
    1.72 +by(auto)
    1.73 +
    1.74 +lift_definition "fun" :: "'a st \<Rightarrow> vname \<Rightarrow> 'a" is fst ..
    1.75 +
    1.76 +lift_definition dom :: "'a st \<Rightarrow> vname set" is snd ..
    1.77  
    1.78 -definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
    1.79 +lemma dom_St[simp]: "dom(St f X) = X"
    1.80 +by(simp add: St.rep_eq dom.rep_eq)
    1.81  
    1.82 -value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
    1.83 +lemma fun_St[simp]: "fun(St f X) = (\<lambda>x. if x \<in> X then f x else undefined)"
    1.84 +by(simp add: St.rep_eq fun.rep_eq)
    1.85 +
    1.86 +definition show_st :: "'a st \<Rightarrow> (vname * 'a)set" where
    1.87 +"show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
    1.88  
    1.89  definition "show_acom = map_acom (Option.map show_st)"
    1.90  definition "show_acom_opt = Option.map show_acom"
    1.91  
    1.92 -definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
    1.93 +lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    1.94 +by transfer auto
    1.95  
    1.96 -lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    1.97 -by(rule ext)(auto simp: update_def)
    1.98 +lemma dom_update[simp]: "dom (update S x y) = insert x (dom S)"
    1.99 +by transfer auto
   1.100 +
   1.101 +definition \<gamma>_st :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
   1.102 +"\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom  F. f x \<in> \<gamma>(fun F x)}"
   1.103  
   1.104 -lemma dom_update[simp]: "dom (update S x y) = dom S"
   1.105 -by(simp add: update_def)
   1.106 +lemma ext_st: "dom F = dom G \<Longrightarrow> \<forall>x \<in> dom G. fun F x = fun G x \<Longrightarrow> F=G"
   1.107 +apply(induct F rule:Abs_st_induct)
   1.108 +apply(induct G rule:Abs_st_induct)
   1.109 +apply (auto simp:Abs_st_inject fun_def dom_def Abs_st_inverse simp del: st.simps)
   1.110 +apply(rule ext)
   1.111 +apply auto
   1.112 +done
   1.113  
   1.114 -definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
   1.115 -
   1.116 -
   1.117 -instantiation st :: (preord) preord
   1.118 +instantiation st :: (order) order
   1.119  begin
   1.120  
   1.121 -definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
   1.122 -"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"
   1.123 +definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
   1.124 +"F \<le> (G::'a st) = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<le> fun G x))"
   1.125 +
   1.126 +definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
   1.127  
   1.128  instance
   1.129  proof
   1.130 -  case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)
   1.131 -qed (auto simp: le_st_def)
   1.132 +  case goal1 show ?case by(rule less_st_def)
   1.133 +next
   1.134 +  case goal2 show ?case by(auto simp: less_eq_st_def)
   1.135 +next
   1.136 +  case goal3 thus ?case by(fastforce simp: less_eq_st_def)
   1.137 +next
   1.138 +  case goal4 thus ?case by (metis less_eq_st_def antisym ext_st)
   1.139 +qed
   1.140  
   1.141  end
   1.142  
   1.143 @@ -139,7 +175,7 @@
   1.144  begin
   1.145  
   1.146  definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
   1.147 -"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
   1.148 +"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
   1.149  
   1.150  instance ..
   1.151  
   1.152 @@ -149,7 +185,7 @@
   1.153  begin
   1.154  
   1.155  definition L_st :: "vname set \<Rightarrow> 'a st set" where
   1.156 -"L X = {F. dom F = X}"
   1.157 +"L(X::vname set) = {F. dom F = X}"
   1.158  
   1.159  instance ..
   1.160  
   1.161 @@ -158,11 +194,10 @@
   1.162  instantiation st :: (semilattice) semilatticeL
   1.163  begin
   1.164  
   1.165 -definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
   1.166 +definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
   1.167  
   1.168  instance
   1.169 -proof
   1.170 -qed (auto simp: le_st_def join_st_def top_st_def L_st_def)
   1.171 +proof qed(auto simp add: less_eq_st_def join_st_def Top_st_def L_st_def)
   1.172  
   1.173  end
   1.174  
   1.175 @@ -175,12 +210,12 @@
   1.176     But L is not executable. This looping defn makes it look as if it were. *)
   1.177  
   1.178  
   1.179 -lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
   1.180 -by(auto simp: le_st_def)
   1.181 +lemma mono_fun: "F \<le> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<le> fun G x"
   1.182 +by(auto simp: less_eq_st_def)
   1.183  
   1.184  lemma mono_update[simp]:
   1.185 -  "a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"
   1.186 -by(auto simp add: le_st_def update_def)
   1.187 +  "a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
   1.188 +by(auto simp add: less_eq_st_def)
   1.189  
   1.190  
   1.191  locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
   1.192 @@ -195,22 +230,22 @@
   1.193  abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
   1.194  where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
   1.195  
   1.196 -lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
   1.197 -by(auto simp: top_st_def \<gamma>_st_def)
   1.198 +lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (Top X) = UNIV"
   1.199 +by(auto simp: Top_st_def \<gamma>_st_def)
   1.200  
   1.201 -lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
   1.202 -by (simp add: top_option_def)
   1.203 +lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (Top X) = UNIV"
   1.204 +by (simp add: Top_option_def)
   1.205  
   1.206 -lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
   1.207 -apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
   1.208 +lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
   1.209 +apply(simp add:\<gamma>_st_def subset_iff less_eq_st_def split: if_splits)
   1.210  by (metis mono_gamma subsetD)
   1.211  
   1.212  lemma mono_gamma_o:
   1.213 -  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   1.214 -by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
   1.215 +  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   1.216 +by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
   1.217  
   1.218 -lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   1.219 -by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
   1.220 +lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   1.221 +by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
   1.222  
   1.223  lemma in_gamma_option_iff:
   1.224    "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"