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