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