1(* Title: HOL/TLA/Action.thy 2 Author: Stephan Merz 3 Copyright: 1998 University of Munich 4*) 5 6section \<open>The action level of TLA as an Isabelle theory\<close> 7 8theory Action 9imports Stfun 10begin 11 12type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a" 13type_synonym action = "bool trfun" 14 15instance prod :: (world, world) world .. 16 17definition enabled :: "action \<Rightarrow> stpred" 18 where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A" 19 20 21consts 22 before :: "'a stfun \<Rightarrow> 'a trfun" 23 after :: "'a stfun \<Rightarrow> 'a trfun" 24 unch :: "'a stfun \<Rightarrow> action" 25 26syntax 27 (* Syntax for writing action expressions in arbitrary contexts *) 28 "_ACT" :: "lift \<Rightarrow> 'a" ("(ACT _)") 29 30 "_before" :: "lift \<Rightarrow> lift" ("($_)" [100] 99) 31 "_after" :: "lift \<Rightarrow> lift" ("(_$)" [100] 99) 32 "_unchanged" :: "lift \<Rightarrow> lift" ("(unchanged _)" [100] 99) 33 34 (*** Priming: same as "after" ***) 35 "_prime" :: "lift \<Rightarrow> lift" ("(_`)" [100] 99) 36 37 "_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [100] 100) 38 39translations 40 "ACT A" => "(A::state*state \<Rightarrow> _)" 41 "_before" == "CONST before" 42 "_after" == "CONST after" 43 "_prime" => "_after" 44 "_unchanged" == "CONST unch" 45 "_Enabled" == "CONST enabled" 46 "s \<Turnstile> Enabled A" <= "_Enabled A s" 47 "w \<Turnstile> unchanged f" <= "_unchanged f w" 48 49axiomatization where 50 unl_before: "(ACT $v) (s,t) \<equiv> v s" and 51 unl_after: "(ACT v$) (s,t) \<equiv> v t" and 52 unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)" 53 54 55definition SqAct :: "[action, 'a stfun] \<Rightarrow> action" 56 where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)" 57 58definition AnAct :: "[action, 'a stfun] \<Rightarrow> action" 59 where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)" 60 61syntax 62 "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0, 1000] 99) 63 "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0, 1000] 99) 64translations 65 "_SqAct" == "CONST SqAct" 66 "_AnAct" == "CONST AnAct" 67 "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w" 68 "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w" 69 70 71(* The following assertion specializes "intI" for any world type 72 which is a pair, not just for "state * state". 73*) 74 75lemma actionI [intro!]: 76 assumes "\<And>s t. (s,t) \<Turnstile> A" 77 shows "\<turnstile> A" 78 apply (rule assms intI prod.induct)+ 79 done 80 81lemma actionD [dest]: "\<turnstile> A \<Longrightarrow> (s,t) \<Turnstile> A" 82 apply (erule intD) 83 done 84 85lemma pr_rews [int_rewrite]: 86 "\<turnstile> (#c)` = #c" 87 "\<And>f. \<turnstile> f<x>` = f<x` >" 88 "\<And>f. \<turnstile> f<x,y>` = f<x`,y` >" 89 "\<And>f. \<turnstile> f<x,y,z>` = f<x`,y`,z` >" 90 "\<turnstile> (\<forall>x. P x)` = (\<forall>x. (P x)`)" 91 "\<turnstile> (\<exists>x. P x)` = (\<exists>x. (P x)`)" 92 by (rule actionI, unfold unl_after intensional_rews, rule refl)+ 93 94 95lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews 96 97lemmas action_rews = act_rews intensional_rews 98 99 100(* ================ Functions to "unlift" action theorems into HOL rules ================ *) 101 102ML \<open> 103(* The following functions are specialized versions of the corresponding 104 functions defined in Intensional.ML in that they introduce a 105 "world" parameter of the form (s,t) and apply additional rewrites. 106*) 107 108fun action_unlift ctxt th = 109 (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD})) 110 handle THM _ => int_unlift ctxt th; 111 112(* Turn \<turnstile> A = B into meta-level rewrite rule A == B *) 113val action_rewrite = int_rewrite 114 115fun action_use ctxt th = 116 case Thm.concl_of th of 117 Const _ $ (Const (\<^const_name>\<open>Valid\<close>, _) $ _) => 118 (flatten (action_unlift ctxt th) handle THM _ => th) 119 | _ => th; 120\<close> 121 122attribute_setup action_unlift = 123 \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close> 124attribute_setup action_rewrite = 125 \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close> 126attribute_setup action_use = 127 \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close> 128 129 130(* =========================== square / angle brackets =========================== *) 131 132lemma idle_squareI: "(s,t) \<Turnstile> unchanged v \<Longrightarrow> (s,t) \<Turnstile> [A]_v" 133 by (simp add: square_def) 134 135lemma busy_squareI: "(s,t) \<Turnstile> A \<Longrightarrow> (s,t) \<Turnstile> [A]_v" 136 by (simp add: square_def) 137 138lemma squareE [elim]: 139 "\<lbrakk> (s,t) \<Turnstile> [A]_v; A (s,t) \<Longrightarrow> B (s,t); v t = v s \<Longrightarrow> B (s,t) \<rbrakk> \<Longrightarrow> B (s,t)" 140 apply (unfold square_def action_rews) 141 apply (erule disjE) 142 apply simp_all 143 done 144 145lemma squareCI [intro]: "\<lbrakk> v t \<noteq> v s \<Longrightarrow> A (s,t) \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> [A]_v" 146 apply (unfold square_def action_rews) 147 apply (rule disjCI) 148 apply (erule (1) meta_mp) 149 done 150 151lemma angleI [intro]: "\<And>s t. \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> <A>_v" 152 by (simp add: angle_def) 153 154lemma angleE [elim]: "\<lbrakk> (s,t) \<Turnstile> <A>_v; \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 155 apply (unfold angle_def action_rews) 156 apply (erule conjE) 157 apply simp 158 done 159 160lemma square_simulation: 161 "\<And>f. \<lbrakk> \<turnstile> unchanged f \<and> \<not>B \<longrightarrow> unchanged g; 162 \<turnstile> A \<and> \<not>unchanged g \<longrightarrow> B 163 \<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g" 164 apply clarsimp 165 apply (erule squareE) 166 apply (auto simp add: square_def) 167 done 168 169lemma not_square: "\<turnstile> (\<not> [A]_v) = <\<not>A>_v" 170 by (auto simp: square_def angle_def) 171 172lemma not_angle: "\<turnstile> (\<not> <A>_v) = [\<not>A]_v" 173 by (auto simp: square_def angle_def) 174 175 176(* ============================== Facts about ENABLED ============================== *) 177 178lemma enabledI: "\<turnstile> A \<longrightarrow> $Enabled A" 179 by (auto simp add: enabled_def) 180 181lemma enabledE: "\<lbrakk> s \<Turnstile> Enabled A; \<And>u. A (s,u) \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" 182 apply (unfold enabled_def) 183 apply (erule exE) 184 apply simp 185 done 186 187lemma notEnabledD: "\<turnstile> \<not>$Enabled G \<longrightarrow> \<not> G" 188 by (auto simp add: enabled_def) 189 190(* Monotonicity *) 191lemma enabled_mono: 192 assumes min: "s \<Turnstile> Enabled F" 193 and maj: "\<turnstile> F \<longrightarrow> G" 194 shows "s \<Turnstile> Enabled G" 195 apply (rule min [THEN enabledE]) 196 apply (rule enabledI [action_use]) 197 apply (erule maj [action_use]) 198 done 199 200(* stronger variant *) 201lemma enabled_mono2: 202 assumes min: "s \<Turnstile> Enabled F" 203 and maj: "\<And>t. F (s,t) \<Longrightarrow> G (s,t)" 204 shows "s \<Turnstile> Enabled G" 205 apply (rule min [THEN enabledE]) 206 apply (rule enabledI [action_use]) 207 apply (erule maj) 208 done 209 210lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)" 211 by (auto elim!: enabled_mono) 212 213lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F \<or> G)" 214 by (auto elim!: enabled_mono) 215 216lemma enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F" 217 by (auto elim!: enabled_mono) 218 219lemma enabled_conj2: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled G" 220 by (auto elim!: enabled_mono) 221 222lemma enabled_conjE: 223 "\<lbrakk> s \<Turnstile> Enabled (F \<and> G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" 224 apply (frule enabled_conj1 [action_use]) 225 apply (drule enabled_conj2 [action_use]) 226 apply simp 227 done 228 229lemma enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G" 230 by (auto simp add: enabled_def) 231 232lemma enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)" 233 apply clarsimp 234 apply (rule iffI) 235 apply (erule enabled_disjD [action_use]) 236 apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+ 237 done 238 239lemma enabled_ex: "\<turnstile> Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))" 240 by (force simp add: enabled_def) 241 242 243(* A rule that combines enabledI and baseE, but generates fewer instantiations *) 244lemma base_enabled: 245 "\<lbrakk> basevars vs; \<exists>c. \<forall>u. vs u = c \<longrightarrow> A(s,u) \<rbrakk> \<Longrightarrow> s \<Turnstile> Enabled A" 246 apply (erule exE) 247 apply (erule baseE) 248 apply (rule enabledI [action_use]) 249 apply (erule allE) 250 apply (erule mp) 251 apply assumption 252 done 253 254(* ======================= action_simp_tac ============================== *) 255 256ML \<open> 257(* A dumb simplification-based tactic with just a little first-order logic: 258 should plug in only "very safe" rules that can be applied blindly. 259 Note that it applies whatever simplifications are currently active. 260*) 261fun action_simp_tac ctxt intros elims = 262 asm_full_simp_tac 263 (ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros) 264 @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) 265 ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims) 266 @ [conjE,disjE,exE])))); 267\<close> 268 269(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) 270 271ML \<open> 272(* "Enabled A" can be proven as follows: 273 - Assume that we know which state variables are "base variables" 274 this should be expressed by a theorem of the form "basevars (x,y,z,...)". 275 - Resolve this theorem with baseE to introduce a constant for the value of the 276 variables in the successor state, and resolve the goal with the result. 277 - Resolve with enabledI and do some rewriting. 278 - Solve for the unknowns using standard HOL reasoning. 279 The following tactic combines these steps except the final one. 280*) 281 282fun enabled_tac ctxt base_vars = 283 clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]); 284\<close> 285 286method_setup enabled = \<open> 287 Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th)) 288\<close> 289 290(* Example *) 291 292lemma 293 assumes "basevars (x,y,z)" 294 shows "\<turnstile> x \<longrightarrow> Enabled ($x \<and> (y$ = #False))" 295 apply (enabled assms) 296 apply auto 297 done 298 299end 300