src/HOL/TLA/Action.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 6255 db63752140c7
child 7881 1b1db39a110b
permissions -rw-r--r--
expandshort
     1 (* 
     2     File:	 Action.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6 Lemmas and tactics for TLA actions.
     7 *)
     8 
     9 (* The following assertion specializes "intI" for any world type 
    10    which is a pair, not just for "state * state".
    11 *)
    12 qed_goal "actionI" Action.thy "(!!s t. (s,t) |= A) ==> |- A"
    13   (fn [prem] => [REPEAT (resolve_tac [prem,intI,prod_induct] 1)]);
    14 
    15 qed_goal "actionD" Action.thy "|- A ==> (s,t) |= A"
    16   (fn [prem] => [rtac (prem RS intD) 1]);
    17 
    18 local
    19   fun prover s = prove_goal Action.thy s 
    20                     (fn _ => [rtac actionI 1, 
    21                               rewrite_goals_tac (unl_after::intensional_rews),
    22                               rtac refl 1])
    23 in
    24   val pr_rews = map (int_rewrite o prover)
    25     [ "|- (#c)` = #c",
    26       "|- f<x>` = f<x`>",
    27       "|- f<x,y>` = f<x`,y`>",
    28       "|- f<x,y,z>` = f<x`,y`,z`>",
    29       "|- (! x. P x)` = (! x. (P x)`)",
    30       "|- (? x. P x)` = (? x. (P x)`)"
    31     ]
    32 end;
    33 
    34 val act_rews = [unl_before,unl_after,unchanged_def] @ pr_rews;
    35 Addsimps act_rews;
    36 
    37 val action_rews = act_rews @ intensional_rews;
    38 
    39 (* ================ Functions to "unlift" action theorems into HOL rules ================ *)
    40 
    41 (* The following functions are specialized versions of the corresponding
    42    functions defined in Intensional.ML in that they introduce a
    43    "world" parameter of the form (s,t) and apply additional rewrites.
    44 *)
    45 fun action_unlift th = 
    46     (rewrite_rule action_rews (th RS actionD)) 
    47     handle _ => int_unlift th;
    48 
    49 (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    50 val action_rewrite = int_rewrite;
    51 
    52 fun action_use th =
    53     case (concl_of th) of
    54       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    55               ((flatten (action_unlift th)) handle _ => th)
    56     | _ => th;
    57 
    58 (* ===================== Update simpset and classical prover ============================= *)
    59 
    60 (***
    61 (* Make the simplifier use action_use rather than int_use
    62    when action simplifications are added.
    63 *)
    64 
    65 let
    66   val ss = simpset_ref()
    67   fun try_rewrite th = 
    68       (action_rewrite th) handle _ => (action_use th) handle _ => th
    69 in
    70   ss := !ss setmksimps ((mksimps mksimps_pairs) o try_rewrite)
    71 end;
    72 ***)
    73 
    74 AddSIs [actionI];
    75 AddDs  [actionD];
    76 
    77 (* =========================== square / angle brackets =========================== *)
    78 
    79 qed_goalw "idle_squareI" Action.thy [square_def]
    80    "!!s t. (s,t) |= unchanged v ==> (s,t) |= [A]_v"
    81    (fn _ => [ Asm_full_simp_tac 1 ]);
    82 
    83 qed_goalw "busy_squareI" Action.thy [square_def]
    84    "!!s t. (s,t) |= A ==> (s,t) |= [A]_v"
    85    (fn _ => [ Asm_simp_tac 1 ]);
    86 
    87 qed_goal "squareE" Action.thy
    88   "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
    89   (fn prems => [cut_facts_tac prems 1,
    90                 rewrite_goals_tac (square_def::action_rews),
    91                 etac disjE 1,
    92                 REPEAT (eresolve_tac prems 1)]);
    93 
    94 qed_goalw "squareCI" Action.thy (square_def::action_rews)
    95   "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
    96   (fn prems => [rtac disjCI 1,
    97                 eresolve_tac prems 1]);
    98 
    99 qed_goalw "angleI" Action.thy [angle_def]
   100   "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
   101   (fn _ => [ Asm_simp_tac 1 ]);
   102 
   103 qed_goalw "angleE" Action.thy (angle_def::action_rews)
   104   "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
   105   (fn prems => [cut_facts_tac prems 1,
   106                 etac conjE 1,
   107                 REPEAT (ares_tac prems 1)]);
   108 
   109 AddIs [angleI, squareCI];
   110 AddEs [angleE, squareE];
   111 
   112 qed_goal "square_simulation" Action.thy
   113    "!!f. [| |- unchanged f & ~B --> unchanged g;   \
   114 \           |- A & ~unchanged g --> B              \
   115 \        |] ==> |- [A]_f --> [B]_g"
   116    (fn _ => [Clarsimp_tac 1,
   117              etac squareE 1,
   118              auto_tac (claset(), simpset() addsimps [square_def])
   119             ]);
   120 
   121 qed_goalw "not_square" Action.thy [square_def,angle_def]
   122    "|- (~ [A]_v) = <~A>_v"
   123    (fn _ => [ Auto_tac ]);
   124 
   125 qed_goalw "not_angle" Action.thy [square_def,angle_def]
   126    "|- (~ <A>_v) = [~A]_v"
   127    (fn _ => [ Auto_tac ]);
   128 
   129 (* ============================== Facts about ENABLED ============================== *)
   130 
   131 qed_goal "enabledI" Action.thy
   132   "|- A --> $Enabled A"
   133   (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
   134 
   135 qed_goalw "enabledE" Action.thy [enabled_def]
   136   "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
   137   (fn prems => [cut_facts_tac prems 1,
   138                 etac exE 1,
   139                 resolve_tac prems 1, atac 1
   140                ]);
   141 
   142 qed_goal "notEnabledD" Action.thy
   143   "|- ~$Enabled G --> ~ G"
   144   (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
   145 
   146 (* Monotonicity *)
   147 qed_goal "enabled_mono" Action.thy
   148   "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G"
   149   (fn [min,maj] => [rtac (min RS enabledE) 1,
   150                     rtac (action_use enabledI) 1,
   151                     etac (action_use maj) 1
   152                    ]);
   153 
   154 (* stronger variant *)
   155 qed_goal "enabled_mono2" Action.thy
   156    "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G"
   157    (fn [min,maj] => [rtac (min RS enabledE) 1,
   158 		     rtac (action_use enabledI) 1,
   159 		     etac maj 1
   160 		    ]);
   161 
   162 qed_goal "enabled_disj1" Action.thy
   163   "|- Enabled F --> Enabled (F | G)"
   164   (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
   165 
   166 qed_goal "enabled_disj2" Action.thy
   167   "|- Enabled G --> Enabled (F | G)"
   168   (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
   169 
   170 qed_goal "enabled_conj1" Action.thy
   171   "|- Enabled (F & G) --> Enabled F"
   172   (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
   173 
   174 qed_goal "enabled_conj2" Action.thy
   175   "|- Enabled (F & G) --> Enabled G"
   176   (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
   177 
   178 qed_goal "enabled_conjE" Action.thy
   179   "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
   180   (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
   181                 etac (action_use enabled_conj1) 1, 
   182 		etac (action_use enabled_conj2) 1
   183 	       ]);
   184 
   185 qed_goal "enabled_disjD" Action.thy
   186   "|- Enabled (F | G) --> Enabled F | Enabled G"
   187   (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
   188 
   189 qed_goal "enabled_disj" Action.thy
   190   "|- Enabled (F | G) = (Enabled F | Enabled G)"
   191   (fn _ => [Clarsimp_tac 1,
   192 	    rtac iffI 1,
   193             etac (action_use enabled_disjD) 1,
   194             REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1)
   195            ]);
   196 
   197 qed_goal "enabled_ex" Action.thy
   198   "|- Enabled (? x. F x) = (? x. Enabled (F x))"
   199   (fn _ => [ force_tac (claset(), simpset() addsimps [enabled_def]) 1 ]);
   200 
   201 
   202 (* A rule that combines enabledI and baseE, but generates fewer possible instantiations *)
   203 qed_goal "base_enabled" Action.thy
   204   "[| basevars vs; !!u. vs u = c s ==> A (s,u) |] ==> s |= Enabled A"
   205   (fn prems => [cut_facts_tac prems 1,
   206 		etac baseE 1, rtac (action_use enabledI) 1,
   207 		REPEAT (ares_tac prems 1)]);
   208 
   209 
   210 (* ================================ action_simp_tac ================================== *)
   211 
   212 (* A dumb simplification-based tactic with just a little first-order logic:
   213    should plug in only "very safe" rules that can be applied blindly.
   214    Note that it applies whatever simplifications are currently active.
   215 *)
   216 fun action_simp_tac ss intros elims =
   217     asm_full_simp_tac 
   218          (ss setloop ((resolve_tac ((map action_use intros)
   219                                     @ [refl,impI,conjI,actionI,intI,allI]))
   220 		      ORELSE' (eresolve_tac ((map action_use elims) 
   221                                              @ [conjE,disjE,exE]))));
   222 
   223 (* default version without additional plug-in rules *)
   224 val Action_simp_tac = action_simp_tac (simpset()) [] [];
   225 
   226 
   227 
   228 (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
   229 (* "Enabled A" can be proven as follows:
   230    - Assume that we know which state variables are "base variables";
   231      this should be expressed by a theorem of the form "basevars (x,y,z,...)".
   232    - Resolve this theorem with baseE to introduce a constant for the value of the
   233      variables in the successor state, and resolve the goal with the result.
   234    - Resolve with enabledI and do some rewriting.
   235    - Solve for the unknowns using standard HOL reasoning.
   236    The following tactic combines these steps except the final one.
   237 *)
   238 (*** old version
   239 fun enabled_tac base_vars i =
   240     EVERY [(* apply actionI (plus rewriting) if the goal is of the form $(Enabled A),
   241 	      do nothing if it is of the form s |= Enabled A *)
   242 	   TRY ((resolve_tac [actionI,intI] i) 
   243                 THEN (SELECT_GOAL (rewrite_goals_tac action_rews) i)),
   244 	   clarify_tac (claset() addSIs [base_vars RS base_enabled]) i,
   245 	   (SELECT_GOAL (rewrite_goals_tac action_rews) i)
   246 	  ];
   247 ***)
   248 
   249 fun enabled_tac base_vars =
   250     clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
   251 
   252 (* Example:
   253 
   254 val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
   255 by (enabled_tac prem 1);
   256 by Auto_tac;
   257 
   258 *)