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