src/HOL/TLA/Action.thy
changeset 21624 6f79647cf536
parent 17309 c43ed29bd197
child 24180 9f818139951b
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Dec 01 17:22:33 2006 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Sat Dec 02 02:52:02 2006 +0100
     1.3 @@ -3,12 +3,9 @@
     1.4      ID:          $Id$
     1.5      Author:      Stephan Merz
     1.6      Copyright:   1998 University of Munich
     1.7 +*)
     1.8  
     1.9 -    Theory Name: Action
    1.10 -    Logic Image: HOL
    1.11 -
    1.12 -Define the action level of TLA as an Isabelle theory.
    1.13 -*)
    1.14 +header {* The action level of TLA as an Isabelle theory *}
    1.15  
    1.16  theory Action
    1.17  imports Stfun
    1.18 @@ -75,6 +72,250 @@
    1.19  
    1.20    enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    1.21  
    1.22 -ML {* use_legacy_bindings (the_context ()) *}
    1.23 +
    1.24 +(* The following assertion specializes "intI" for any world type
    1.25 +   which is a pair, not just for "state * state".
    1.26 +*)
    1.27 +
    1.28 +lemma actionI [intro!]:
    1.29 +  assumes "!!s t. (s,t) |= A"
    1.30 +  shows "|- A"
    1.31 +  apply (rule assms intI prod_induct)+
    1.32 +  done
    1.33 +
    1.34 +lemma actionD [dest]: "|- A ==> (s,t) |= A"
    1.35 +  apply (erule intD)
    1.36 +  done
    1.37 +
    1.38 +lemma pr_rews [int_rewrite]:
    1.39 +  "|- (#c)` = #c"
    1.40 +  "!!f. |- f<x>` = f<x` >"
    1.41 +  "!!f. |- f<x,y>` = f<x`,y` >"
    1.42 +  "!!f. |- f<x,y,z>` = f<x`,y`,z` >"
    1.43 +  "|- (! x. P x)` = (! x. (P x)`)"
    1.44 +  "|- (? x. P x)` = (? x. (P x)`)"
    1.45 +  by (rule actionI, unfold unl_after intensional_rews, rule refl)+
    1.46 +
    1.47 +
    1.48 +lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews
    1.49 +
    1.50 +lemmas action_rews = act_rews intensional_rews
    1.51 +
    1.52 +
    1.53 +(* ================ Functions to "unlift" action theorems into HOL rules ================ *)
    1.54 +
    1.55 +ML {*
    1.56 +(* The following functions are specialized versions of the corresponding
    1.57 +   functions defined in Intensional.ML in that they introduce a
    1.58 +   "world" parameter of the form (s,t) and apply additional rewrites.
    1.59 +*)
    1.60 +local
    1.61 +  val action_rews = thms "action_rews";
    1.62 +  val actionD = thm "actionD";
    1.63 +in
    1.64 +
    1.65 +fun action_unlift th =
    1.66 +  (rewrite_rule action_rews (th RS actionD))
    1.67 +    handle THM _ => int_unlift th;
    1.68 +
    1.69 +(* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    1.70 +val action_rewrite = int_rewrite
    1.71 +
    1.72 +fun action_use th =
    1.73 +    case (concl_of th) of
    1.74 +      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    1.75 +              (flatten (action_unlift th) handle THM _ => th)
    1.76 +    | _ => th;
    1.77  
    1.78  end
    1.79 +*}
    1.80 +
    1.81 +setup {*
    1.82 +  Attrib.add_attributes [
    1.83 +    ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
    1.84 +    ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
    1.85 +    ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
    1.86 +*}
    1.87 +
    1.88 +
    1.89 +(* =========================== square / angle brackets =========================== *)
    1.90 +
    1.91 +lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"
    1.92 +  by (simp add: square_def)
    1.93 +
    1.94 +lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
    1.95 +  by (simp add: square_def)
    1.96 +  
    1.97 +lemma squareE [elim]:
    1.98 +  "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
    1.99 +  apply (unfold square_def action_rews)
   1.100 +  apply (erule disjE)
   1.101 +  apply simp_all
   1.102 +  done
   1.103 +
   1.104 +lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
   1.105 +  apply (unfold square_def action_rews)
   1.106 +  apply (rule disjCI)
   1.107 +  apply (erule (1) meta_mp)
   1.108 +  done
   1.109 +
   1.110 +lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
   1.111 +  by (simp add: angle_def)
   1.112 +
   1.113 +lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
   1.114 +  apply (unfold angle_def action_rews)
   1.115 +  apply (erule conjE)
   1.116 +  apply simp
   1.117 +  done
   1.118 +
   1.119 +lemma square_simulation:
   1.120 +   "!!f. [| |- unchanged f & ~B --> unchanged g;    
   1.121 +            |- A & ~unchanged g --> B               
   1.122 +         |] ==> |- [A]_f --> [B]_g"
   1.123 +  apply clarsimp
   1.124 +  apply (erule squareE)
   1.125 +  apply (auto simp add: square_def)
   1.126 +  done
   1.127 +
   1.128 +lemma not_square: "|- (~ [A]_v) = <~A>_v"
   1.129 +  by (auto simp: square_def angle_def)
   1.130 +
   1.131 +lemma not_angle: "|- (~ <A>_v) = [~A]_v"
   1.132 +  by (auto simp: square_def angle_def)
   1.133 +
   1.134 +
   1.135 +(* ============================== Facts about ENABLED ============================== *)
   1.136 +
   1.137 +lemma enabledI: "|- A --> $Enabled A"
   1.138 +  by (auto simp add: enabled_def)
   1.139 +
   1.140 +lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
   1.141 +  apply (unfold enabled_def)
   1.142 +  apply (erule exE)
   1.143 +  apply simp
   1.144 +  done
   1.145 +
   1.146 +lemma notEnabledD: "|- ~$Enabled G --> ~ G"
   1.147 +  by (auto simp add: enabled_def)
   1.148 +
   1.149 +(* Monotonicity *)
   1.150 +lemma enabled_mono:
   1.151 +  assumes min: "s |= Enabled F"
   1.152 +    and maj: "|- F --> G"
   1.153 +  shows "s |= Enabled G"
   1.154 +  apply (rule min [THEN enabledE])
   1.155 +  apply (rule enabledI [action_use])
   1.156 +  apply (erule maj [action_use])
   1.157 +  done
   1.158 +
   1.159 +(* stronger variant *)
   1.160 +lemma enabled_mono2:
   1.161 +  assumes min: "s |= Enabled F"
   1.162 +    and maj: "!!t. F (s,t) ==> G (s,t)"
   1.163 +  shows "s |= Enabled G"
   1.164 +  apply (rule min [THEN enabledE])
   1.165 +  apply (rule enabledI [action_use])
   1.166 +  apply (erule maj)
   1.167 +  done
   1.168 +
   1.169 +lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)"
   1.170 +  by (auto elim!: enabled_mono)
   1.171 +
   1.172 +lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)"
   1.173 +  by (auto elim!: enabled_mono)
   1.174 +
   1.175 +lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F"
   1.176 +  by (auto elim!: enabled_mono)
   1.177 +
   1.178 +lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G"
   1.179 +  by (auto elim!: enabled_mono)
   1.180 +
   1.181 +lemma enabled_conjE:
   1.182 +    "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
   1.183 +  apply (frule enabled_conj1 [action_use])
   1.184 +  apply (drule enabled_conj2 [action_use])
   1.185 +  apply simp
   1.186 +  done
   1.187 +
   1.188 +lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G"
   1.189 +  by (auto simp add: enabled_def)
   1.190 +
   1.191 +lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)"
   1.192 +  apply clarsimp
   1.193 +  apply (rule iffI)
   1.194 +   apply (erule enabled_disjD [action_use])
   1.195 +  apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
   1.196 +  done
   1.197 +
   1.198 +lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
   1.199 +  by (force simp add: enabled_def)
   1.200 +
   1.201 +
   1.202 +(* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   1.203 +lemma base_enabled:
   1.204 +    "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   1.205 +  apply (erule exE)
   1.206 +  apply (erule baseE)
   1.207 +  apply (rule enabledI [action_use])
   1.208 +  apply (erule allE)
   1.209 +  apply (erule mp)
   1.210 +  apply assumption
   1.211 +  done
   1.212 +
   1.213 +(* ======================= action_simp_tac ============================== *)
   1.214 +
   1.215 +ML {*
   1.216 +(* A dumb simplification-based tactic with just a little first-order logic:
   1.217 +   should plug in only "very safe" rules that can be applied blindly.
   1.218 +   Note that it applies whatever simplifications are currently active.
   1.219 +*)
   1.220 +local
   1.221 +  val actionI = thm "actionI";
   1.222 +  val intI = thm "intI";
   1.223 +in
   1.224 +
   1.225 +fun action_simp_tac ss intros elims =
   1.226 +    asm_full_simp_tac
   1.227 +         (ss setloop ((resolve_tac ((map action_use intros)
   1.228 +                                    @ [refl,impI,conjI,actionI,intI,allI]))
   1.229 +                      ORELSE' (eresolve_tac ((map action_use elims)
   1.230 +                                             @ [conjE,disjE,exE]))));
   1.231 +
   1.232 +(* default version without additional plug-in rules *)
   1.233 +val Action_simp_tac = action_simp_tac (simpset()) [] []
   1.234 +
   1.235 +end
   1.236 +*}
   1.237 +
   1.238 +(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
   1.239 +
   1.240 +ML {*
   1.241 +(* "Enabled A" can be proven as follows:
   1.242 +   - Assume that we know which state variables are "base variables"
   1.243 +     this should be expressed by a theorem of the form "basevars (x,y,z,...)".
   1.244 +   - Resolve this theorem with baseE to introduce a constant for the value of the
   1.245 +     variables in the successor state, and resolve the goal with the result.
   1.246 +   - Resolve with enabledI and do some rewriting.
   1.247 +   - Solve for the unknowns using standard HOL reasoning.
   1.248 +   The following tactic combines these steps except the final one.
   1.249 +*)
   1.250 +local
   1.251 +  val base_enabled = thm "base_enabled";
   1.252 +in
   1.253 +
   1.254 +fun enabled_tac base_vars =
   1.255 +  clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
   1.256 +
   1.257 +end
   1.258 +*}
   1.259 +
   1.260 +(* Example *)
   1.261 +
   1.262 +lemma
   1.263 +  assumes "basevars (x,y,z)"
   1.264 +  shows "|- x --> Enabled ($x & (y$ = #False))"
   1.265 +  apply (tactic {* enabled_tac (thm "assms") 1 *})
   1.266 +  apply auto
   1.267 +  done
   1.268 +
   1.269 +end