wneuper/isa: src/HOL/TLA/Action.thy@0040bafffdef

     1 (*  Title:      HOL/TLA/Action.thy

     2     Author:     Stephan Merz

     3     Copyright:  1998 University of Munich

     4 *)

     6 header {* The action level of TLA as an Isabelle theory *}

     8 theory Action

     9 imports Stfun

    10 begin

    13 (** abstract syntax **)

    15 types

    16   'a trfun = "(state * state) => 'a"

    17   action   = "bool trfun"

    19 arities prod :: (world, world) world

    21 consts

    22   (** abstract syntax **)

    23   before        :: "'a stfun => 'a trfun"

    24   after         :: "'a stfun => 'a trfun"

    25   unch          :: "'a stfun => action"

    27   SqAct         :: "[action, 'a stfun] => action"

    28   AnAct         :: "[action, 'a stfun] => action"

    29   enabled       :: "action => stpred"

    31 (** concrete syntax **)

    33 syntax

    34   (* Syntax for writing action expressions in arbitrary contexts *)

    35   "_ACT"        :: "lift => 'a"                      ("(ACT _)")

    37   "_before"     :: "lift => lift"                    ("($_)"  [100] 99)

    38   "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)

    39   "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)

    41   (*** Priming: same as "after" ***)

    42   "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)

    44   "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)

    45   "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)

    46   "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)

    48 translations

    49   "ACT A"            =>   "(A::state*state => _)"

    50   "_before"          ==   "CONST before"

    51   "_after"           ==   "CONST after"

    52   "_prime"           =>   "_after"

    53   "_unchanged"       ==   "CONST unch"

    54   "_SqAct"           ==   "CONST SqAct"

    55   "_AnAct"           ==   "CONST AnAct"

    56   "_Enabled"         ==   "CONST enabled"

    57   "w |= [A]_v"       <=   "_SqAct A v w"

    58   "w |= <A>_v"       <=   "_AnAct A v w"

    59   "s |= Enabled A"   <=   "_Enabled A s"

    60   "w |= unchanged f" <=   "_unchanged f w"

    62 axioms

    63   unl_before:    "(ACT $v) (s,t) == v s"

    64   unl_after:     "(ACT v$) (s,t) == v t"

    66   unchanged_def: "(s,t) |= unchanged v == (v t = v s)"

    67   square_def:    "ACT [A]_v == ACT (A | unchanged v)"

    68   angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"

    70   enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"

    73 (* The following assertion specializes "intI" for any world type

    74    which is a pair, not just for "state * state".

    75 *)

    77 lemma actionI [intro!]:

    78   assumes "!!s t. (s,t) |= A"

    79   shows "|- A"

    80   apply (rule assms intI prod.induct)+

    81   done

    83 lemma actionD [dest]: "|- A ==> (s,t) |= A"

    84   apply (erule intD)

    85   done

    87 lemma pr_rews [int_rewrite]:

    88   "|- (#c)` = #c"

    89   "!!f. |- f<x>` = f<x` >"

    90   "!!f. |- f<x,y>` = f<x`,y` >"

    91   "!!f. |- f<x,y,z>` = f<x`,y`,z` >"

    92   "|- (! x. P x)` = (! x. (P x)`)"

    93   "|- (? x. P x)` = (? x. (P x)`)"

    94   by (rule actionI, unfold unl_after intensional_rews, rule refl)+

    97 lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews

    99 lemmas action_rews = act_rews intensional_rews

   102 (* ================ Functions to "unlift" action theorems into HOL rules ================ *)

   104 ML {*

   105 (* The following functions are specialized versions of the corresponding

   106    functions defined in Intensional.ML in that they introduce a

   107    "world" parameter of the form (s,t) and apply additional rewrites.

   108 *)

   110 fun action_unlift th =

   111   (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))

   112     handle THM _ => int_unlift th;

   114 (* Turn  |- A = B  into meta-level rewrite rule  A == B *)

   115 val action_rewrite = int_rewrite

   117 fun action_use th =

   118     case (concl_of th) of

   119       Const _ $ (Const ("Intensional.Valid", _) $ _) =>

   120               (flatten (action_unlift th) handle THM _ => th)

   121     | _ => th;

   122 *}

   124 attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""

   125 attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""

   126 attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""

   129 (* =========================== square / angle brackets =========================== *)

   131 lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"

   132   by (simp add: square_def)

   134 lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"

   135   by (simp add: square_def)

   137 lemma squareE [elim]:

   138   "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"

   139   apply (unfold square_def action_rews)

   140   apply (erule disjE)

   141   apply simp_all

   142   done

   144 lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"

   145   apply (unfold square_def action_rews)

   146   apply (rule disjCI)

   147   apply (erule (1) meta_mp)

   148   done

   150 lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"

   151   by (simp add: angle_def)

   153 lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"

   154   apply (unfold angle_def action_rews)

   155   apply (erule conjE)

   156   apply simp

   157   done

   159 lemma square_simulation:

   160    "!!f. [| |- unchanged f & ~B --> unchanged g;

   161             |- A & ~unchanged g --> B

   162          |] ==> |- [A]_f --> [B]_g"

   163   apply clarsimp

   164   apply (erule squareE)

   165   apply (auto simp add: square_def)

   166   done

   168 lemma not_square: "|- (~ [A]_v) = <~A>_v"

   169   by (auto simp: square_def angle_def)

   171 lemma not_angle: "|- (~ <A>_v) = [~A]_v"

   172   by (auto simp: square_def angle_def)

   175 (* ============================== Facts about ENABLED ============================== *)

   177 lemma enabledI: "|- A --> $Enabled A"

   178   by (auto simp add: enabled_def)

   180 lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"

   181   apply (unfold enabled_def)

   182   apply (erule exE)

   183   apply simp

   184   done

   186 lemma notEnabledD: "|- ~$Enabled G --> ~ G"

   187   by (auto simp add: enabled_def)

   189 (* Monotonicity *)

   190 lemma enabled_mono:

   191   assumes min: "s |= Enabled F"

   192     and maj: "|- F --> G"

   193   shows "s |= Enabled G"

   194   apply (rule min [THEN enabledE])

   195   apply (rule enabledI [action_use])

   196   apply (erule maj [action_use])

   197   done

   199 (* stronger variant *)

   200 lemma enabled_mono2:

   201   assumes min: "s |= Enabled F"

   202     and maj: "!!t. F (s,t) ==> G (s,t)"

   203   shows "s |= Enabled G"

   204   apply (rule min [THEN enabledE])

   205   apply (rule enabledI [action_use])

   206   apply (erule maj)

   207   done

   209 lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)"

   210   by (auto elim!: enabled_mono)

   212 lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)"

   213   by (auto elim!: enabled_mono)

   215 lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F"

   216   by (auto elim!: enabled_mono)

   218 lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G"

   219   by (auto elim!: enabled_mono)

   221 lemma enabled_conjE:

   222     "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"

   223   apply (frule enabled_conj1 [action_use])

   224   apply (drule enabled_conj2 [action_use])

   225   apply simp

   226   done

   228 lemma enabled_disjD: "|- Enabled (F | G) --> Enabled F | Enabled G"

   229   by (auto simp add: enabled_def)

   231 lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)"

   232   apply clarsimp

   233   apply (rule iffI)

   234    apply (erule enabled_disjD [action_use])

   235   apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+

   236   done

   238 lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"

   239   by (force simp add: enabled_def)

   242 (* A rule that combines enabledI and baseE, but generates fewer instantiations *)

   243 lemma base_enabled:

   244     "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"

   245   apply (erule exE)

   246   apply (erule baseE)

   247   apply (rule enabledI [action_use])

   248   apply (erule allE)

   249   apply (erule mp)

   250   apply assumption

   251   done

   253 (* ======================= action_simp_tac ============================== *)

   255 ML {*

   256 (* A dumb simplification-based tactic with just a little first-order logic:

   257    should plug in only "very safe" rules that can be applied blindly.

   258    Note that it applies whatever simplifications are currently active.

   259 *)

   260 fun action_simp_tac ss intros elims =

   261     asm_full_simp_tac

   262          (ss setloop ((resolve_tac ((map action_use intros)

   263                                     @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))

   264                       ORELSE' (eresolve_tac ((map action_use elims)

   265                                              @ [conjE,disjE,exE]))));

   266 *}

   268 (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)

   270 ML {*

   271 (* "Enabled A" can be proven as follows:

   272    - Assume that we know which state variables are "base variables"

   273      this should be expressed by a theorem of the form "basevars (x,y,z,...)".

   274    - Resolve this theorem with baseE to introduce a constant for the value of the

   275      variables in the successor state, and resolve the goal with the result.

   276    - Resolve with enabledI and do some rewriting.

   277    - Solve for the unknowns using standard HOL reasoning.

   278    The following tactic combines these steps except the final one.

   279 *)

   281 fun enabled_tac (cs, ss) base_vars =

   282   clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);

   283 *}

   285 (* Example *)

   287 lemma

   288   assumes "basevars (x,y,z)"

   289   shows "|- x --> Enabled ($x & (y$ = #False))"

   290   apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})

   291   apply auto

   292   done

   294 end

author	haftmann
	Thu, 01 Jul 2010 16:54:44 +0200
changeset 37678	0040bafffdef
parent 35355	2e8dc3c64430
child 42889	878f33040280
permissions	-rw-r--r--