src/HOL/TLA/Action.thy
author wenzelm
Sat Dec 02 02:52:02 2006 +0100 (2006-12-02)
changeset 21624 6f79647cf536
parent 17309 c43ed29bd197
child 24180 9f818139951b
permissions -rw-r--r--
TLA: converted legacy ML scripts;
     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 local
   113   val action_rews = thms "action_rews";
   114   val actionD = thm "actionD";
   115 in
   116 
   117 fun action_unlift th =
   118   (rewrite_rule action_rews (th RS actionD))
   119     handle THM _ => int_unlift th;
   120 
   121 (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
   122 val action_rewrite = int_rewrite
   123 
   124 fun action_use th =
   125     case (concl_of th) of
   126       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   127               (flatten (action_unlift th) handle THM _ => th)
   128     | _ => th;
   129 
   130 end
   131 *}
   132 
   133 setup {*
   134   Attrib.add_attributes [
   135     ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
   136     ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
   137     ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
   138 *}
   139 
   140 
   141 (* =========================== square / angle brackets =========================== *)
   142 
   143 lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"
   144   by (simp add: square_def)
   145 
   146 lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
   147   by (simp add: square_def)
   148   
   149 lemma squareE [elim]:
   150   "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
   151   apply (unfold square_def action_rews)
   152   apply (erule disjE)
   153   apply simp_all
   154   done
   155 
   156 lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
   157   apply (unfold square_def action_rews)
   158   apply (rule disjCI)
   159   apply (erule (1) meta_mp)
   160   done
   161 
   162 lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
   163   by (simp add: angle_def)
   164 
   165 lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
   166   apply (unfold angle_def action_rews)
   167   apply (erule conjE)
   168   apply simp
   169   done
   170 
   171 lemma square_simulation:
   172    "!!f. [| |- unchanged f & ~B --> unchanged g;    
   173             |- A & ~unchanged g --> B               
   174          |] ==> |- [A]_f --> [B]_g"
   175   apply clarsimp
   176   apply (erule squareE)
   177   apply (auto simp add: square_def)
   178   done
   179 
   180 lemma not_square: "|- (~ [A]_v) = <~A>_v"
   181   by (auto simp: square_def angle_def)
   182 
   183 lemma not_angle: "|- (~ <A>_v) = [~A]_v"
   184   by (auto simp: square_def angle_def)
   185 
   186 
   187 (* ============================== Facts about ENABLED ============================== *)
   188 
   189 lemma enabledI: "|- A --> $Enabled A"
   190   by (auto simp add: enabled_def)
   191 
   192 lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
   193   apply (unfold enabled_def)
   194   apply (erule exE)
   195   apply simp
   196   done
   197 
   198 lemma notEnabledD: "|- ~$Enabled G --> ~ G"
   199   by (auto simp add: enabled_def)
   200 
   201 (* Monotonicity *)
   202 lemma enabled_mono:
   203   assumes min: "s |= Enabled F"
   204     and maj: "|- F --> G"
   205   shows "s |= Enabled G"
   206   apply (rule min [THEN enabledE])
   207   apply (rule enabledI [action_use])
   208   apply (erule maj [action_use])
   209   done
   210 
   211 (* stronger variant *)
   212 lemma enabled_mono2:
   213   assumes min: "s |= Enabled F"
   214     and maj: "!!t. F (s,t) ==> G (s,t)"
   215   shows "s |= Enabled G"
   216   apply (rule min [THEN enabledE])
   217   apply (rule enabledI [action_use])
   218   apply (erule maj)
   219   done
   220 
   221 lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)"
   222   by (auto elim!: enabled_mono)
   223 
   224 lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)"
   225   by (auto elim!: enabled_mono)
   226 
   227 lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F"
   228   by (auto elim!: enabled_mono)
   229 
   230 lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G"
   231   by (auto elim!: enabled_mono)
   232 
   233 lemma enabled_conjE:
   234     "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
   235   apply (frule enabled_conj1 [action_use])
   236   apply (drule enabled_conj2 [action_use])
   237   apply simp
   238   done
   239 
   240 lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G"
   241   by (auto simp add: enabled_def)
   242 
   243 lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)"
   244   apply clarsimp
   245   apply (rule iffI)
   246    apply (erule enabled_disjD [action_use])
   247   apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
   248   done
   249 
   250 lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
   251   by (force simp add: enabled_def)
   252 
   253 
   254 (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   255 lemma base_enabled:
   256     "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   257   apply (erule exE)
   258   apply (erule baseE)
   259   apply (rule enabledI [action_use])
   260   apply (erule allE)
   261   apply (erule mp)
   262   apply assumption
   263   done
   264 
   265 (* ======================= action_simp_tac ============================== *)
   266 
   267 ML {*
   268 (* A dumb simplification-based tactic with just a little first-order logic:
   269    should plug in only "very safe" rules that can be applied blindly.
   270    Note that it applies whatever simplifications are currently active.
   271 *)
   272 local
   273   val actionI = thm "actionI";
   274   val intI = thm "intI";
   275 in
   276 
   277 fun action_simp_tac ss intros elims =
   278     asm_full_simp_tac
   279          (ss setloop ((resolve_tac ((map action_use intros)
   280                                     @ [refl,impI,conjI,actionI,intI,allI]))
   281                       ORELSE' (eresolve_tac ((map action_use elims)
   282                                              @ [conjE,disjE,exE]))));
   283 
   284 (* default version without additional plug-in rules *)
   285 val Action_simp_tac = action_simp_tac (simpset()) [] []
   286 
   287 end
   288 *}
   289 
   290 (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
   291 
   292 ML {*
   293 (* "Enabled A" can be proven as follows:
   294    - Assume that we know which state variables are "base variables"
   295      this should be expressed by a theorem of the form "basevars (x,y,z,...)".
   296    - Resolve this theorem with baseE to introduce a constant for the value of the
   297      variables in the successor state, and resolve the goal with the result.
   298    - Resolve with enabledI and do some rewriting.
   299    - Solve for the unknowns using standard HOL reasoning.
   300    The following tactic combines these steps except the final one.
   301 *)
   302 local
   303   val base_enabled = thm "base_enabled";
   304 in
   305 
   306 fun enabled_tac base_vars =
   307   clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
   308 
   309 end
   310 *}
   311 
   312 (* Example *)
   313 
   314 lemma
   315   assumes "basevars (x,y,z)"
   316   shows "|- x --> Enabled ($x & (y$ = #False))"
   317   apply (tactic {* enabled_tac (thm "assms") 1 *})
   318   apply auto
   319   done
   320 
   321 end