src/HOL/Bali/AxSem.thy
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Bali/AxSem.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -62,8 +62,9 @@
     1.4  translations
     1.5    (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     1.6  
     1.7 -definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
     1.8 - "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
     1.9 +definition
    1.10 +  assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
    1.11 +  where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
    1.12    
    1.13  lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
    1.14  apply (unfold assn_imp_def)
    1.15 @@ -75,8 +76,9 @@
    1.16  
    1.17  subsection "peek-and"
    1.18  
    1.19 -definition peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) where
    1.20 - "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
    1.21 +definition
    1.22 +  peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
    1.23 +  where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)"
    1.24  
    1.25  lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
    1.26  apply (unfold peek_and_def)
    1.27 @@ -114,8 +116,9 @@
    1.28  
    1.29  subsection "assn-supd"
    1.30  
    1.31 -definition assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) where
    1.32 - "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
    1.33 +definition
    1.34 +  assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
    1.35 +  where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)"
    1.36  
    1.37  lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
    1.38  apply (unfold assn_supd_def)
    1.39 @@ -124,8 +127,9 @@
    1.40  
    1.41  subsection "supd-assn"
    1.42  
    1.43 -definition supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) where
    1.44 - "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
    1.45 +definition
    1.46 +  supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
    1.47 +  where "(f .; P) = (\<lambda>Y s. P Y (f s))"
    1.48  
    1.49  
    1.50  lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
    1.51 @@ -143,8 +147,9 @@
    1.52  
    1.53  subsection "subst-res"
    1.54  
    1.55 -definition subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60) where
    1.56 - "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
    1.57 +definition
    1.58 +  subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60)
    1.59 +  where "P\<leftarrow>w = (\<lambda>Y. P w)"
    1.60  
    1.61  lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
    1.62  apply (unfold subst_res_def)
    1.63 @@ -178,8 +183,9 @@
    1.64  
    1.65  subsection "subst-Bool"
    1.66  
    1.67 -definition subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) where
    1.68 - "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
    1.69 +definition
    1.70 +  subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
    1.71 +  where "P\<leftarrow>=b = (\<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
    1.72  
    1.73  lemma subst_Bool_def2 [simp]: 
    1.74  "(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
    1.75 @@ -193,8 +199,9 @@
    1.76  
    1.77  subsection "peek-res"
    1.78  
    1.79 -definition peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
    1.80 - "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
    1.81 +definition
    1.82 +  peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
    1.83 +  where "peek_res Pf = (\<lambda>Y. Pf Y Y)"
    1.84  
    1.85  syntax
    1.86    "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
    1.87 @@ -221,8 +228,9 @@
    1.88  
    1.89  subsection "ign-res"
    1.90  
    1.91 -definition ign_res :: "        'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) where
    1.92 -  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
    1.93 +definition
    1.94 +  ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
    1.95 +  where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)"
    1.96  
    1.97  lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
    1.98  apply (unfold ign_res_def)
    1.99 @@ -252,8 +260,9 @@
   1.100  
   1.101  subsection "peek-st"
   1.102  
   1.103 -definition peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
   1.104 - "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
   1.105 +definition
   1.106 +  peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
   1.107 +  where "peek_st P = (\<lambda>Y s. P (store s) Y s)"
   1.108  
   1.109  syntax
   1.110    "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
   1.111 @@ -296,8 +305,9 @@
   1.112  
   1.113  subsection "ign-res-eq"
   1.114  
   1.115 -definition ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60) where
   1.116 - "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
   1.117 +definition
   1.118 +  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60)
   1.119 +  where "P\<down>=w \<equiv> (\<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w))"
   1.120  
   1.121  lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
   1.122  apply (unfold ign_res_eq_def)
   1.123 @@ -326,8 +336,9 @@
   1.124  
   1.125  subsection "RefVar"
   1.126  
   1.127 -definition RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) where
   1.128 - "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
   1.129 +definition
   1.130 +  RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13)
   1.131 +  where "(vf ..; P) = (\<lambda>Y s. let (v,s') = vf s in P (Var v) s')"
   1.132   
   1.133  lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
   1.134    P (Var (fst (vf s))) (snd (vf s))"
   1.135 @@ -337,12 +348,13 @@
   1.136  
   1.137  subsection "allocation"
   1.138  
   1.139 -definition Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   1.140 - "Alloc G otag P \<equiv> \<lambda>Y s Z.
   1.141 -                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
   1.142 +definition
   1.143 +  Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.144 +  where "Alloc G otag P = (\<lambda>Y s Z. \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
   1.145  
   1.146 -definition SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   1.147 - "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
   1.148 +definition
   1.149 +  SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.150 +  where "SXAlloc G P = (\<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
   1.151  
   1.152  
   1.153  lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
   1.154 @@ -359,11 +371,12 @@
   1.155  
   1.156  section "validity"
   1.157  
   1.158 -definition type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
   1.159 - "type_ok G t s \<equiv> 
   1.160 -    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
   1.161 -                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
   1.162 -              \<and> s\<Colon>\<preceq>(G,L)"
   1.163 +definition
   1.164 +  type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
   1.165 +  "type_ok G t s =
   1.166 +    (\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
   1.167 +                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
   1.168 +               \<and> s\<Colon>\<preceq>(G,L))"
   1.169  
   1.170  datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
   1.171  something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
   1.172 @@ -407,34 +420,35 @@
   1.173  
   1.174  definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
   1.175                  ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75) where
   1.176 - "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   1.177 + "{{P} tf-\<succ> {Q} | ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   1.178    
   1.179 -consts
   1.180 -
   1.181 - triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
   1.182 -                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
   1.183 -    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   1.184 -                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
   1.185 +definition
   1.186 +  triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple  \<Rightarrow> bool"  ("_\<Turnstile>_:_" [61,0, 58] 57)
   1.187 +  where
   1.188 +    "G\<Turnstile>n:t =
   1.189 +      (case t of {P} t\<succ> {Q} \<Rightarrow>
   1.190 +        \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   1.191 +        (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z))"
   1.192  
   1.193  abbreviation
   1.194 - triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   1.195 -                                                (  "_||=_:_" [61,0, 58] 57)
   1.196 - where "G||=n:ts == Ball ts (triple_valid G n)"
   1.197 +  triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"  (  "_||=_:_" [61,0, 58] 57)
   1.198 +  where "G||=n:ts == Ball ts (triple_valid G n)"
   1.199 +
   1.200 +notation (xsymbols)
   1.201 +  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57)
   1.202 +
   1.203 +
   1.204 +definition
   1.205 +  ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>_" [61,58,58] 57)
   1.206 +  where "(G,A|\<Turnstile>ts) = (\<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts)"
   1.207  
   1.208  abbreviation
   1.209 - ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   1.210 -                                                ( "_,_|=_"   [61,58,58] 57)
   1.211 - where "G,A |=t == G,A|\<Turnstile>{t}"
   1.212 +  ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"  ( "_,_|=_"   [61,58,58] 57)
   1.213 +  where "G,A |=t == G,A|\<Turnstile>{t}"
   1.214  
   1.215  notation (xsymbols)
   1.216 -  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
   1.217    ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
   1.218  
   1.219 -defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
   1.220 -                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   1.221 -                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
   1.222 -
   1.223 -defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
   1.224  
   1.225  lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
   1.226   (\<forall>Y s Z. P Y s Z 
   1.227 @@ -625,8 +639,9 @@
   1.228  axioms 
   1.229  *)
   1.230  
   1.231 -definition adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   1.232 -"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
   1.233 +definition
   1.234 +  adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.235 +  where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
   1.236  
   1.237  
   1.238  section "rules derived by induction"