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