# HG changeset patch # User wenzelm # Date 876304233 -7200 # Node ID 82a99b090d9de864fb8a3ecf6742dc87f464bb06 # Parent f371115aed37f7a2edb4769e1d1130d17f9ae625 A formalization of TLA in HOL -- by Stephan Merz; diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Action.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Action.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,356 @@ +(* + File: Action.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Lemmas and tactics for TLA actions. +*) + +val act_rews = [pairSF_def RS eq_reflection,unl_before,unl_after,unchanged_def, + pr_con,pr_before,pr_lift,pr_lift2,pr_lift3,pr_all,pr_ex]; + +val action_rews = act_rews @ intensional_rews; + +qed_goal "actionI" Action.thy "(!!s t. ([[s,t]] |= A)) ==> A" + (fn [prem] => [REPEAT (resolve_tac [prem,intI,state2_ext] 1)]); + +qed_goal "actionD" Action.thy "A ==> ([[s,t]] |= A)" + (fn [prem] => [REPEAT (resolve_tac [prem,intD] 1)]); + + + +(* ================ Functions to "unlift" action theorems into HOL rules ================ *) + +(* Basic unlifting introduces a world parameter and applies basic rewrites, e.g. + A .= B gets ([[s,t]] |= A) = ([[s,t]] |= B) + A .-> B gets ([[s,t]] |= A) --> ([[s,t]] |= B) +*) +fun action_unlift th = rewrite_rule action_rews (th RS actionD); + +(* A .-> B becomes A [[s,t]] ==> B [[s,t]] *) +fun action_mp th = zero_var_indexes ((action_unlift th) RS mp); + +(* A .-> B becomes [| A[[s,t]]; B[[s,t]] ==> R |] ==> R + so that it can be used as an elimination rule +*) +fun action_impE th = zero_var_indexes ((action_unlift th) RS impE); + +(* A .& B .-> C becomes [| A[[s,t]]; B[[s,t]] |] ==> C[[s,t]] *) +fun action_conjmp th = zero_var_indexes (conjI RS (action_mp th)); + +(* A .& B .-> C becomes [| A[[s,t]]; B[[s,t]]; (C[[s,t]] ==> R) |] ==> R *) +fun action_conjimpE th = zero_var_indexes (conjI RS (action_impE th)); + +(* Turn A .= B into meta-level rewrite rule A == B *) +fun action_rewrite th = (rewrite_rule action_rews (th RS inteq_reflection)); + +(* ===================== Update simpset and classical prover ============================= *) + +(* Make the simplifier use action_unlift rather than int_unlift + when action simplifications are added. +*) +fun maybe_unlift th = + (case concl_of th of + Const("TrueInt",_) $ p + => (action_unlift th + handle _ => int_unlift th) + | _ => th); + +simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift); + +(* make act_rews be always active -- intensional_rews has been added before *) +Addsimps act_rews; + +use "cladata.ML"; (* local version! *) + +(* ================================ action_simp_tac ================================== *) + +(* A dumb simplification tactic with just a little first-order logic: + should plug in only "very safe" rules that can be applied blindly. + Note that it applies whatever simplifications are currently active. +*) +fun action_simp_tac ss intros elims i = + (asm_full_simp_tac + (ss setloop ((resolve_tac (intros @ [refl,impI,conjI,actionI,allI])) + ORELSE' (eresolve_tac (elims @ [conjE,disjE,exE_prop])))) + i); +(* default version without additional plug-in rules *) +fun Action_simp_tac i = (action_simp_tac (!simpset) [] [] i); + + +(* ==================== Simplification of abstractions ==================== *) + +(* Somewhat obscure simplifications, rarely necessary to get rid + of abstractions that may be introduced by higher-order unification. +*) + +qed_goal "pr_con_abs" Action.thy "(%w. c)` .= #c" + (fn _ => [rtac actionI 1, + rewrite_goals_tac (con_abs::action_rews), + rtac refl 1 + ]); + +qed_goal "pr_lift_abs" Action.thy "(%w. f(x w))` .= f[x`]" + (fn _ => [rtac actionI 1, + (* give all rewrites to the engine and it loops! *) + rewrite_goals_tac intensional_rews, + rewtac lift_abs, + rewtac pr_lift, + rewtac unl_lift, + rtac refl 1 + ]); + +qed_goal "pr_lift2_abs" Action.thy "(%w. f(x w) (y w))` .= f[x`,y`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift2_abs, + rewtac pr_lift2, + rewtac unl_lift2, + rtac refl 1 + ]); + +qed_goal "pr_lift2_abs_con1" Action.thy "(%w. f x (y w))` .= f[#x, y`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift2_abs_con1, + rewtac pr_lift2, + rewtac unl_lift2, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift2_abs_con2" Action.thy "(%w. f (x w) y)` .= f[x`, #y]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift2_abs_con2, + rewtac pr_lift2, + rewtac unl_lift2, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs" Action.thy "(%w. f(x w) (y w) (z w))` .= f[x`,y`,z`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs, + rewtac pr_lift3, + rewtac unl_lift3, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con1" Action.thy "(%w. f x (y w) (z w))` .= f[#x, y`, z`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con1, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con2" Action.thy "(%w. f (x w) y (z w))` .= f[x`, #y, z`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con2, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con3" Action.thy "(%w. f (x w) (y w) z)` .= f[x`, y`, #z]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con3, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con12" Action.thy "(%w. f x y (z w))` .= f[#x, #y, z`]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con12, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con13" Action.thy "(%w. f x (y w) z)` .= f[#x, y`, #z]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con13, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +qed_goal "pr_lift3_abs_con23" Action.thy "(%w. f (x w) y z)` .= f[x`, #y, #z]" + (fn _ => [rtac actionI 1, + rewrite_goals_tac intensional_rews, + rewtac lift3_abs_con23, + rewtac pr_lift3, + rewtac unl_lift3, + rewtac pr_con, + rewtac unl_con, + rtac refl 1 + ]); + +(* We don't add these as default rewrite rules, because they are + rarely needed and may slow down automatic proofs. +*) +val pr_abs_rews = map (fn th => th RS inteq_reflection) + [pr_con_abs, + pr_lift_abs,pr_lift2_abs,pr_lift2_abs_con1,pr_lift2_abs_con2, + pr_lift3_abs,pr_lift3_abs_con1,pr_lift3_abs_con2,pr_lift3_abs_con3, + pr_lift3_abs_con12,pr_lift3_abs_con13,pr_lift3_abs_con23]; + +(* =========================== square / angle brackets =========================== *) + +qed_goalw "idle_squareI" Action.thy [square_def] + "!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)" + (fn _ => [ Auto_tac() ]); + +qed_goalw "busy_squareI" Action.thy [square_def] + "!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)" + (fn _ => [ Auto_tac() ]); + +qed_goalw "square_simulation" Action.thy [square_def] + "[| unchanged f .& .~B .-> unchanged g; \ +\ A .& .~unchanged g .-> B \ +\ |] ==> [A]_f .-> [B]_g" + (fn [p1,p2] => [Auto_tac(), + etac (action_conjimpE p2) 1, + etac swap 3, etac (action_conjimpE p1) 3, + ALLGOALS atac + ]); + +qed_goalw "not_square" Action.thy [square_def,angle_def] + "(.~ [A]_v) .= <.~A>_v" + (fn _ => [ Auto_tac() ]); + +qed_goalw "not_angle" Action.thy [square_def,angle_def] + "(.~ _v) .= [.~A]_v" + (fn _ => [ Auto_tac() ]); + +(* ============================== Facts about ENABLED ============================== *) + +qed_goalw "enabledI" Action.thy [enabled_def] + "A [[s,t]] ==> (Enabled A) s" + (fn prems => [ REPEAT (resolve_tac (exI::prems) 1) ]); + +qed_goalw "enabledE" Action.thy [enabled_def] + "[| (Enabled A) s; !!u. A[[s,u]] ==> PROP R |] ==> PROP R" + (fn prems => [cut_facts_tac prems 1, + etac exE_prop 1, + resolve_tac prems 1, atac 1 + ]); + +qed_goal "notEnabledD" Action.thy + "!!G. ~ (Enabled G s) ==> ~ G [[s,t]]" + (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]); + +(* Monotonicity *) +qed_goal "enabled_mono" Action.thy + "[| (Enabled F) s; F .-> G |] ==> (Enabled G) s" + (fn [min,maj] => [rtac (min RS enabledE) 1, + rtac enabledI 1, + etac (action_mp maj) 1 + ]); + +(* stronger variant *) +qed_goal "enabled_mono2" Action.thy + "[| (Enabled F) s; !!t. (F [[s,t]] ==> G[[s,t]] ) |] ==> (Enabled G) s" + (fn [min,maj] => [rtac (min RS enabledE) 1, + rtac enabledI 1, + etac maj 1 + ]); + +qed_goal "enabled_disj1" Action.thy + "!!s. (Enabled F) s ==> (Enabled (F .| G)) s" + (fn _ => [etac enabled_mono 1, Auto_tac() + ]); + +qed_goal "enabled_disj2" Action.thy + "!!s. (Enabled G) s ==> (Enabled (F .| G)) s" + (fn _ => [etac enabled_mono 1, Auto_tac() + ]); + +qed_goal "enabled_conj1" Action.thy + "!!s. (Enabled (F .& G)) s ==> (Enabled F) s" + (fn _ => [etac enabled_mono 1, Auto_tac() + ]); + +qed_goal "enabled_conj2" Action.thy + "!!s. (Enabled (F .& G)) s ==> (Enabled G) s" + (fn _ => [etac enabled_mono 1, Auto_tac() + ]); + +qed_goal "enabled_conjE" Action.thy + "[| (Enabled (F .& G)) s; [| (Enabled F) s; (Enabled G) s |] ==> PROP R |] ==> PROP R" + (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1, + etac enabled_conj1 1, etac enabled_conj2 1]); + +qed_goal "enabled_disjD" Action.thy + "!!s. (Enabled (F .| G)) s ==> ((Enabled F) s) | ((Enabled G) s)" + (fn _ => [etac enabledE 1, + auto_tac (action_css addSDs2 [notEnabledD] addSEs2 [enabledI]) + ]); + +qed_goal "enabled_disj" Action.thy + "(Enabled (F .| G)) s = ( (Enabled F) s | (Enabled G) s )" + (fn _ => [rtac iffI 1, + etac enabled_disjD 1, + REPEAT (eresolve_tac [disjE,enabled_disj1,enabled_disj2] 1) + ]); + +qed_goal "enabled_ex" Action.thy + "(Enabled (REX x. F x)) s = (EX x. (Enabled (F x)) s)" + (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]); + + +(* A rule that combines enabledI and baseE, but generates fewer possible instantiations *) +qed_goal "base_enabled" Action.thy + "[| base_var(v); !!u. v u = c s ==> A [[s,u]] |] ==> Enabled A s" + (fn prems => [cut_facts_tac prems 1, + etac baseE 1, rtac enabledI 1, + REPEAT (ares_tac prems 1)]); + + +(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) +(* "Enabled A" can be proven as follows: + - Assume that we know which state variables are "base variables"; + this should be expressed by a theorem of the form "base_var ". + - Resolve this theorem with baseE to introduce a constant for the value of the + variables in the successor state, and resolve the goal with the result. + - E-resolve with PairVarE so that we have one constant per variable. + - Resolve with enabledI and do some rewriting. + - Solve for the unknowns using standard HOL reasoning. + The following tactic combines these steps except the final one. +*) + +fun enabled_tac base_vars i = + EVERY [(* apply actionI (plus rewriting) if the goal is of the form $(Enabled A), + do nothing if it is of the form (Enabled A) s *) + TRY ((rtac actionI i) THEN (SELECT_GOAL (rewrite_goals_tac action_rews) i)), + rtac (base_vars RS base_enabled) i, + REPEAT_DETERM (etac PairVarE i), + (SELECT_GOAL (rewrite_goals_tac action_rews) i) + ]; + +(* Example of use: + +val [prem] = goal Action.thy "base_var ==> $x .-> $Enabled ($x .& (y$ .= #False))"; +by (REPEAT ((CHANGED (Action_simp_tac 1)) ORELSE (enabled_tac prem 1))); + +*) diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Action.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Action.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,60 @@ +(* + File: TLA/Action.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Action + Logic Image: HOL + +Define the action level of TLA as an Isabelle theory. +*) + +Action = Intensional + Stfun + + +types + state2 (* intention: pair of states *) + 'a trfct = "('a, state2) term" + action = "state2 form" + +arities + state2 :: world + +consts + mkstate2 :: "[state,state] => state2" ("([[_,_]])") + + (* lift state variables to transition functions *) + before :: "'a stfun => 'a trfct" ("($_)" [100] 99) + after :: "'a stfun => 'a trfct" ("(_$)" [100] 99) + unchanged :: "'a stfun => action" + + (* Priming *) + prime :: "'a trfct => 'a trfct" ("(_`)" [90] 89) + + SqAct :: "[action, 'a stfun] => action" ("([_]'_(_))" [0,60] 59) + AnAct :: "[action, 'a stfun] => action" ("(<_>'_(_))" [0,60] 59) + Enabled :: "action => stpred" + +rules + (* The following says that state2 is generated by mkstate2 *) + state2_ext "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A" + + unl_before "($v) [[s,t]] == v s" + unl_after "(v$) [[s,t]] == v t" + + pr_con "(#c)` == #c" + pr_before "($v)` == v$" + (* no corresponding rule for "after"! *) + pr_lift "(F[x])` == F[x`]" + pr_lift2 "(F[x,y])` == F[x`,y`]" + pr_lift3 "(F[x,y,z])` == F[x`,y`,z`]" + pr_all "(RALL x. P(x))` == (RALL x. P(x)`)" + pr_ex "(REX x. P(x))` == (REX x. P(x)`)" + + unchanged_def "(unchanged v) [[s,t]] == (v t = v s)" + square_def "[A]_v == A .| unchanged v" + angle_def "_v == A .& .~ unchanged v" + + enabled_def "(Enabled A) s == EX u. A[[s,u]]" +end + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Buffer/Buffer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Buffer/Buffer.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,48 @@ +(* + File: Buffer.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + Simple FIFO buffer (theorems and proofs) +*) + +(* ---------------------------- Data lemmas ---------------------------- *) + +goal List.thy "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys"; +by (auto_tac (!claset, !simpset addsimps [tl_append,neq_Nil_conv])); +qed_spec_mp "tl_append2"; +Addsimps [tl_append2]; + +goal List.thy "xs ~= [] --> tl xs ~= xs"; +by (auto_tac (!claset, !simpset addsimps [neq_Nil_conv])); +qed_spec_mp "tl_not_self"; +Addsimps [tl_not_self]; + +goal List.thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)"; +by (induct_tac "xs" 1); +by (Simp_tac 1); +by (REPEAT (rtac allI 1)); +by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1); +by (Asm_full_simp_tac 1); +by (Blast_tac 1); +qed_spec_mp "append_same_eq"; +AddIffs [append_same_eq]; + +(* ---------------------------- Action lemmas ---------------------------- *) + +(* Dequeue is visible *) +goal Buffer.thy "_ .= Deq ic q oc"; +by (auto_tac (!claset, !simpset addsimps [angle_def,Deq_def])); +qed "Deq_visible"; + +(* Enabling condition for dequeue -- NOT NEEDED *) +goalw Buffer.thy [temp_rewrite Deq_visible] + "!!q. base_var ==> $Enabled (_) .= ($q .~= .[])"; +by (auto_tac (!claset addSEs [base_enabled,enabledE], !simpset addsimps [Deq_def])); +qed "Deq_enabled"; + +(* For the left-to-right implication, we don't need the base variable stuff *) +goalw Buffer.thy [temp_rewrite Deq_visible] + "$Enabled (_) .-> ($q .~= .[])"; +by (auto_tac (!claset addSEs [enabledE], !simpset addsimps [Deq_def])); +qed "Deq_enabledE"; diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Buffer/Buffer.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Buffer/Buffer.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,57 @@ +(* + File: Buffer.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Buffer + Logic Image: TLA + + A simple FIFO buffer (synchronous communication, interleaving) +*) + +Buffer = TLA + List + + +consts + (* infix syntax for list operations *) + "IntNil" :: 'w::world => 'a list (".[]") + "IntCons" :: ['w::world => 'a, 'w => 'a list] => ('w => 'a list) ("(_ .#/ _)" [65,66] 65) + "IntApp" :: ['w::world => 'a list, 'w => 'a list] => ('w => 'a list) ("(_ .@/ _)" [65,66] 65) + + (* actions *) + BInit :: "'a stfun => 'a list stfun => 'a stfun => action" + Enq :: "'a stfun => 'a list stfun => 'a stfun => action" + Deq :: "'a stfun => 'a list stfun => 'a stfun => action" + Next :: "'a stfun => 'a list stfun => 'a stfun => action" + + (* temporal formulas *) + IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal" + Buffer :: "'a stfun => 'a stfun => temporal" + +syntax + "@listInt" :: args => ('a list, 'w) term (".[(_)]") + +translations + ".[]" == "con []" + "x .# xs" == "lift2 (op #) x xs" + "xs .@ ys" == "lift2 (op @) xs ys" + ".[ x, xs ]" == "x .# .[xs]" + ".[ x ]" == "x .# .[]" + +rules + BInit_def "BInit ic q oc == $q .= .[]" + Enq_def "Enq ic q oc == (ic$ .~= $ic) + .& (q$ .= $q .@ .[ ic$ ]) + .& (oc$ .= $oc)" + Deq_def "Deq ic q oc == ($q .~= .[]) + .& (oc$ .= hd[ $q ]) + .& (q$ .= tl[ $q ]) + .& (ic$ .= $ic)" + Next_def "Next ic q oc == Enq ic q oc .| Deq ic q oc" + IBuffer_def "IBuffer ic q oc == Init (BInit ic q oc) + .& [][Next ic q oc]_ + .& WF(Deq ic q oc)_" + Buffer_def "Buffer ic oc == EEX q. IBuffer ic q oc" +end + + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Buffer/DBuffer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Buffer/DBuffer.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,119 @@ +(* + File: DBuffer.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + Double FIFO buffer implements simple FIFO buffer. +*) + +val db_css = (!claset, !simpset addsimps [qc_def]); +Addsimps [qc_def]; + +val db_defs = [BInit_def, Enq_def, Deq_def, Next_def, IBuffer_def, Buffer_def, + DBInit_def,DBEnq_def,DBDeq_def,DBPass_def,DBNext_def,DBuffer_def]; + + +(*** Proper initialization ***) +goal DBuffer.thy "Init DBInit .-> Init (BInit inp qc out)"; +by (auto_tac (db_css addsimps2 [Init_def,DBInit_def,BInit_def])); +qed "DBInit"; + + +(*** Step simulation ***) +goal DBuffer.thy "[DBNext]_ .-> [Next inp qc out]_"; +by (rtac square_simulation 1); +by (Action_simp_tac 1); +by (action_simp_tac (!simpset addsimps hd_append::db_defs) [] [] 1); +qed "DB_step_simulation"; + + +(*** Simulation of fairness ***) + +(* Compute enabledness predicates for DBDeq and DBPass actions *) +goal DBuffer.thy "_ .= DBDeq"; +by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def])); +qed "DBDeq_visible"; + +goal DBuffer.thy "$Enabled (_) .= ($q2 .~= .[])"; +by (rewtac (action_rewrite DBDeq_visible)); +by (cut_facts_tac [DB_base] 1); +by (auto_tac (db_css addSEs2 [base_enabled,enabledE] + addsimps2 [angle_def,DBDeq_def,Deq_def])); +qed "DBDeq_enabled"; + +goal DBuffer.thy "_ .= DBPass"; +by (auto_tac (db_css addsimps2 [angle_def,DBPass_def,Deq_def])); +qed "DBPass_visible"; + +goal DBuffer.thy "$Enabled (_) .= ($q1 .~= .[])"; +by (rewtac (action_rewrite DBPass_visible)); +by (cut_facts_tac [DB_base] 1); +by (auto_tac (db_css addSEs2 [base_enabled,enabledE] + addsimps2 [angle_def,DBPass_def,Deq_def])); +qed "DBPass_enabled"; + + +(* The plan for proving weak fairness at the higher level is to prove + (0) DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out)) + which is in turn reduced to the two leadsto conditions + (1) DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= []) + (2) DBuffer => (q2 ~= [] ~> DBDeq) + and the fact that DBDeq implies _ + (and therefore DBDeq ~> _ trivially holds). + + Condition (1) is reduced to + (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= []) + by standard leadsto rules (leadsto_classical) and rule Deq_enabledE. + + Both (1a) and (2) are proved from DBuffer's WF conditions by standard + WF reasoning (Lamport's WF1 and WF_leadsto). + The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF. + + One could use Lamport's WF2 instead. +*) + +(* Condition (1a) *) +goal DBuffer.thy + "[][DBNext]_ .& WF(DBPass)_ \ +\ .-> ($qc .~= .[] .& $q2 .= .[] ~> $q2 .~= .[])"; +by (rtac WF1 1); +by (action_simp_tac (!simpset addsimps square_def::db_defs) [] [] 1); +by (action_simp_tac (!simpset addsimps [angle_def,DBPass_def]) [] [] 1); +by (action_simp_tac (!simpset addsimps [DBPass_enabled]) [] [] 1); +qed "DBFair_1a"; + +(* Condition (1) *) +goal DBuffer.thy + "[][DBNext]_ .& WF(DBPass)_ \ +\ .-> ($Enabled (_) ~> $q2 .~= .[])"; +by (auto_tac (temp_css addSIs2 [leadsto_classical] addSEs2 [temp_conjimpE DBFair_1a])); +by (auto_tac (temp_css addsimps2 [leadsto,Init_def] addDs2 [STL2bD] + addSDs2 [action_mp Deq_enabledE] addSEs2 [STL4E])); +qed "DBFair_1"; + +(* Condition (2) *) +goal DBuffer.thy + "[][DBNext]_ .& WF(DBDeq)_ \ +\ .-> ($q2 .~= .[] ~> DBDeq)"; +by (rtac WF_leadsto 1); +by (action_simp_tac (!simpset addsimps [DBDeq_visible,DBDeq_enabled]) [] [] 1); +by (action_simp_tac (!simpset addsimps [angle_def]) [] [] 1); +by (action_simp_tac (!simpset addsimps square_def::db_defs) [tempI] [Stable] 1); +qed "DBFair_2"; + +(* High-level fairness *) +goal DBuffer.thy + "[][DBNext]_ .& WF(DBPass)_ \ +\ .& WF(DBDeq)_ \ +\ .-> WF(Deq inp qc out)_"; +by (auto_tac (db_css addSIs2 [leadsto_WF])); +by (auto_tac (db_css addSIs2 [(temp_mp DBFair_1) RSN(2,LatticeTransitivity)])); +by (auto_tac (db_css addSIs2 [(temp_mp DBFair_2) RSN(2,LatticeTransitivity)])); +by (auto_tac (db_css addSIs2 [ImplLeadsto] addSEs2 [STL4E] + addsimps2 [angle_def,DBDeq_def,Deq_def,hd_append])); +qed "DBFair"; + +(*** Main theorem ***) +goalw DBuffer.thy [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out"; +by (auto_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair]))); +qed "DBuffer_impl_Buffer"; diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Buffer/DBuffer.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,40 @@ +(* + File: DBuffer.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: DBuffer + Logic Image: TLA + + Two FIFO buffers in a row, with interleaving assumption. +*) + +DBuffer = Buffer + + +consts + (* implementation variables *) + inp, mid, out :: nat stfun + q1, q2, qc :: nat list stfun + + DBInit, DBEnq, DBDeq, DBPass, DBNext :: action + DBuffer :: temporal + +rules + DB_base "base_var " + + (* the concatenation of the two buffers *) + qc_def "$qc .= $q2 .@ $q1" + + DBInit_def "DBInit == BInit inp q1 mid .& BInit mid q2 out" + DBEnq_def "DBEnq == Enq inp q1 mid .& unchanged " + DBDeq_def "DBDeq == Deq mid q2 out .& unchanged " + DBPass_def "DBPass == Deq inp q1 mid + .& (q2$ .= $q2 .@ .[ mid$ ]) + .& (out$ .= $out)" + DBNext_def "DBNext == DBEnq .| DBDeq .| DBPass" + DBuffer_def "DBuffer == Init(DBInit) + .& [][DBNext]_ + .& WF(DBDeq)_ + .& WF(DBPass)_" + +end \ No newline at end of file diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Inc/Inc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Inc/Inc.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,253 @@ +(* + File: TLA/ex/inc/Inc.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Proofs for the "increment" example from SRC79. +*) + +val PsiInv_defs = [PsiInv_def,PsiInv1_def,PsiInv2_def,PsiInv3_def]; +val Psi_defs = [Psi_def,InitPsi_def,N1_def,N2_def,alpha1_def,alpha2_def, + beta1_def,beta2_def,gamma1_def,gamma2_def]; + +val Inc_css = (!claset, !simpset); + +(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***) + +qed_goal "PsiInv_Init" Inc.thy "InitPsi .-> PsiInv" + (fn _ => [ auto_tac (Inc_css addsimps2 InitPsi_def::PsiInv_defs) ]); + +qed_goal "PsiInv_alpha1" Inc.thy "alpha1 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 alpha1_def::PsiInv_defs) ]); + +qed_goal "PsiInv_alpha2" Inc.thy "alpha2 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 alpha2_def::PsiInv_defs) ]); + +qed_goal "PsiInv_beta1" Inc.thy "beta1 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 beta1_def::PsiInv_defs) ]); + +qed_goal "PsiInv_beta2" Inc.thy "beta2 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 beta2_def::PsiInv_defs) ]); + +qed_goal "PsiInv_gamma1" Inc.thy "gamma1 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 gamma1_def::PsiInv_defs) ]); + +qed_goal "PsiInv_gamma2" Inc.thy "gamma2 .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]); + +qed_goal "PsiInv_stutter" Inc.thy "unchanged .& PsiInv .-> PsiInv`" + (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]); + +qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv" + (fn _ => [inv_tac (Inc_css addsimps2 [Psi_def]) 1, + SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init] + addsimps2 [Init_def])) 1, + auto_tac (Inc_css addSEs2 (map action_conjimpE + [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1, + PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2]) + addIs2 [action_mp PsiInv_stutter] + addsimps2 [square_def,N1_def, N2_def]) + ]); + + + +(* Automatic proof works too, but it make take a while on a slow machine. + More substantial examples require manual guidance anyway. + +goal Inc.thy "Psi .-> []PsiInv"; +by (auto_inv_tac (!simpset addsimps PsiInv_defs @ Psi_defs @ pcount.simps) 1); + +*) + +(**** Step simulation ****) + +qed_goal "Init_sim" Inc.thy "Psi .-> Init(InitPhi)" + (fn _ => [ auto_tac (Inc_css addsimps2 [InitPhi_def,Psi_def,InitPsi_def,Init_def]) ]); + +qed_goal "Step_sim" Inc.thy "Psi .-> [][M1 .| M2]_" + (fn _ => [auto_tac (Inc_css addsimps2 [square_def,M1_def,M2_def] @ Psi_defs + addSEs2 [STL4E]) + ]); + +(**** Proof of fairness ****) + +(* + The goal is to prove Fair_M1 far below, which asserts + Psi .-> WF(M1)_ + (the other fairness condition is symmetrical). + + The strategy is to use WF2 (with beta1 as the helpful action). Proving its + temporal premise needs two auxiliary lemmas: + 1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1 + 2. N1_live: the first component will eventually reach b + + Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness + of the semaphore, and needs auxiliary lemmas that ensure that the second + component will eventually release the semaphore. Most of the proofs of + the auxiliary lemmas are very similar. +*) + +qed_goal "Stuck_at_b" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .-> stable($pc1 .= #b)" + (fn _ => [rtac StableL 1, + auto_tac (Inc_css addsimps2 square_def::Psi_defs) + ]); + +qed_goal "N1_enabled_at_g" Inc.thy + "($pc1 .= #g) .-> $(Enabled (_))" + (fn _ => [Action_simp_tac 1, + res_inst_tac [("F","gamma1")] enabled_mono 1, + enabled_tac Inc_base 1, + auto_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def]) + ]); + +qed_goal "g1_leadsto_a1" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .& SF(N1)_ .& []#True \ +\ .-> ($pc1 .= #g ~> $pc1 .= #a)" + (fn _ => [rtac SF1 1, + (* the first two subgoals are simple action formulas and succumb to the + auto_tac; don't expand N1 in the third subgoal *) + SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, + (* reduce []A .-> <>Enabled B to A .-> Enabled B *) + auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N1_enabled_at_g] + addSDs2 [STL2bD] + addsimps2 [Init_def]) + ]); + +(* symmetrical for N2, and similar for beta2 *) +qed_goal "N2_enabled_at_g" Inc.thy + "($pc2 .= #g) .-> $(Enabled (_))" + (fn _ => [Action_simp_tac 1, + res_inst_tac [("F","gamma2")] enabled_mono 1, + enabled_tac Inc_base 1, + auto_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def]) + ]); + +qed_goal "g2_leadsto_a2" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .& SF(N2)_ .& []#True \ +\ .-> ($pc2 .= #g ~> $pc2 .= #a)" + (fn _ => [rtac SF1 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, + auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_g] + addSDs2 [STL2bD] + addsimps2 [Init_def]) + ]); + +qed_goal "N2_enabled_at_b" Inc.thy + "($pc2 .= #b) .-> $(Enabled (_))" + (fn _ => [Action_simp_tac 1, + res_inst_tac [("F","beta2")] enabled_mono 1, + enabled_tac Inc_base 1, + auto_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def]) + ]); + +qed_goal "b2_leadsto_g2" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .& SF(N2)_ .& []#True \ +\ .-> ($pc2 .= #b ~> $pc2 .= #g)" + (fn _ => [rtac SF1 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, + auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_b] + addSDs2 [STL2bD] + addsimps2 [Init_def]) + ]); + +(* Combine above lemmas: the second component will eventually reach pc2 = a *) +qed_goal "N2_leadsto_a" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .& SF(N2)_ .& []#True \ +\ .-> (($pc2 .= #a .| $pc2 .= #b .| $pc2 .= #g) ~> $pc2 .= #a)" + (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]), + rtac (LatticeReflexivity RS tempD) 1, + rtac LatticeTransitivity 1, + auto_tac (Inc_css addSIs2 (map temp_mp [b2_leadsto_g2,g2_leadsto_a2])) + ]); + +(* A variant that gets rid of the disjunction, thanks to induction over data types *) +qed_goal "N2_live" Inc.thy + "[][(N1 .| N2) .& .~ beta1]_ .& SF(N2)_ \ +\ .-> <>($pc2 .= #a)" + (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]), + rewrite_goals_tac (Init_def::action_rews), + pcount.induct_tac "pc2 (fst_st sigma)" 1, + Auto_tac() + ]); + +(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *) + +qed_goal "N1_enabled_at_both_a" Inc.thy + "$pc2 .= #a .& (PsiInv .& $pc1 .= #a) .-> $(Enabled (_))" + (fn _ => [Action_simp_tac 1, + res_inst_tac [("F","alpha1")] enabled_mono 1, + enabled_tac Inc_base 1, + auto_tac (Inc_css addIs2 [sym] + addsimps2 [angle_def,alpha1_def,N1_def] @ PsiInv_defs) + ]); + +qed_goal "a1_leadsto_b1" Inc.thy + "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_) \ +\ .& SF(N1)_ .& [] SF(N2)_ \ +\ .-> ($pc1 .= #a ~> $pc1 .= #b)" + (fn _ => [rtac SF1 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, + auto_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_mp DmdImpl)]), + auto_tac (Inc_css addSIs2 [temp_mp BoxDmdT2, temp_mp N2_live] + addsimps2 split_box_conj::more_temp_simps) + ]); + +(* Combine the leadsto properties for N1: it will arrive at pc1 = b *) + +qed_goal "N1_leadsto_b" Inc.thy + "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_) \ +\ .& SF(N1)_ .& [] SF(N2)_ \ +\ .-> (($pc1 .= #b .| $pc1 .= #g .| $pc1 .= #a) ~> $pc1 .= #b)" + (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]), + rtac (LatticeReflexivity RS tempD) 1, + rtac LatticeTransitivity 1, + auto_tac (Inc_css addSIs2 (map temp_mp [a1_leadsto_b1,g1_leadsto_a1]) + addsimps2 [split_box_conj]) + ]); + +qed_goal "N1_live" Inc.thy + "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_) \ +\ .& SF(N1)_ .& [] SF(N2)_ \ +\ .-> <>($pc1 .= #b)" + (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]), + rewrite_goals_tac (Init_def::action_rews), + pcount.induct_tac "pc1 (fst_st sigma)" 1, + Auto_tac() + ]); + +qed_goal "N1_enabled_at_b" Inc.thy + "($pc1 .= #b) .-> $(Enabled (_))" + (fn _ => [Action_simp_tac 1, + res_inst_tac [("F","beta1")] enabled_mono 1, + enabled_tac Inc_base 1, + auto_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def]) + ]); + +(* Now assemble the bits and pieces to prove that Psi is fair. *) + +qed_goal "Fair_M1_lemma" Inc.thy + "[](PsiInv .& [(N1 .| N2)]_) \ +\ .& SF(N1)_ .& [] SF(N2)_ \ +\ .-> SF(M1)_" + (fn _ => [res_inst_tac [("B","beta1"),("P","$pc1 .= #b")] SF2 1, + (* the action premises are simple *) + SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def])) 1, + SELECT_GOAL (auto_tac (Inc_css addsimps2 angle_def::Psi_defs)) 1, + SELECT_GOAL (auto_tac (Inc_css addSEs2 [action_mp N1_enabled_at_b])) 1, + (* temporal premise: use previous lemmas and simple TL *) + auto_tac (Inc_css addSIs2 DmdStable::(map temp_mp [N1_live,Stuck_at_b]) + addEs2 [STL4E] + addsimps2 [square_def]) + ]); + +qed_goal "Fair_M1" Inc.thy "Psi .-> WF(M1)_" + (fn _ => [auto_tac (Inc_css addSIs2 SFImplWF::(map temp_mp [Fair_M1_lemma, PsiInv]) + addsimps2 [split_box_conj]), + auto_tac (Inc_css addsimps2 Psi_def::more_temp_simps) + ]); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Inc/Inc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Inc/Inc.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,68 @@ +(* + File: TLA/ex/inc/Inc.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Inc + Logic Image: TLA + + Lamport's "increment" example. +*) + +Inc = TLA + Nat + Pcount + + +consts + (* program variables *) + x,y,sem :: "nat stfun" + pc1,pc2 :: "pcount stfun" + + (* names of actions and predicates *) + M1,M2,N1,N2 :: "action" + alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: "action" + InitPhi, InitPsi :: "action" + PsiInv,PsiInv1,PsiInv2,PsiInv3 :: "action" + + (* temporal formulas *) + Phi, Psi :: "temporal" + +rules + (* the "base" variables, required to compute enabledness predicates *) + Inc_base "base_var " + + (* definitions for high-level program *) + InitPhi_def "InitPhi == ($x .= # 0) .& ($y .= # 0)" + M1_def "M1 == (x$ .= Suc[$x]) .& (y$ .= $y)" + M2_def "M2 == (y$ .= Suc[$y]) .& (x$ .= $x)" + Phi_def "Phi == Init(InitPhi) .& [][M1 .| M2]_ .& \ +\ WF(M1)_ .& WF(M2)_" + + (* definitions for low-level program *) + InitPsi_def "InitPsi == ($pc1 .= #a) .& ($pc2 .= #a) .& \ +\ ($x .= # 0) .& ($y .= # 0) .& ($sem .= Suc[# 0])" + alpha1_def "alpha1 == ($pc1 .= #a) .& (pc1$ .= #b) .& ($sem .= Suc[sem$]) .& \ +\ unchanged()" + alpha2_def "alpha2 == ($pc2 .= #a) .& (pc2$ .= #b) .& ($sem .= Suc[sem$]) .& \ +\ unchanged()" + beta1_def "beta1 == ($pc1 .= #b) .& (pc1$ .= #g) .& (x$ .= Suc[$x]) .& \ +\ unchanged()" + beta2_def "beta2 == ($pc2 .= #b) .& (pc2$ .= #g) .& (y$ .= Suc[$y]) .& \ +\ unchanged()" + gamma1_def "gamma1 == ($pc1 .= #g) .& (pc1$ .= #a) .& (sem$ .= Suc[$sem]) .& \ +\ unchanged()" + gamma2_def "gamma2 == ($pc2 .= #g) .& (pc2$ .= #a) .& (sem$ .= Suc[$sem]) .& \ +\ unchanged()" + N1_def "N1 == alpha1 .| beta1 .| gamma1" + N2_def "N2 == alpha2 .| beta2 .| gamma2" + Psi_def "Psi == Init(InitPsi) \ +\ .& [][N1 .| N2]_ \ +\ .& SF(N1)_ \ +\ .& SF(N2)_" + + PsiInv1_def "PsiInv1 == ($sem .= Suc[# 0]) .& ($pc1 .= #a) .& ($pc2 .= #a)" + PsiInv2_def "PsiInv2 == ($sem .= # 0) .& ($pc1 .= #a) .& ($pc2 .= #b .| $pc2 .= #g)" + PsiInv3_def "PsiInv3 == ($sem .= # 0) .& ($pc2 .= #a) .& ($pc1 .= #b .| $pc1 .= #g)" + PsiInv_def "PsiInv == PsiInv1 .| PsiInv2 .| PsiInv3" + +end + +ML diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Inc/Pcount.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Inc/Pcount.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,20 @@ +(* + File: TLA/ex/inc/Pcount.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Pcount + Logic Image: TLA + +Data type "program counter" for the increment example. +Isabelle/HOL's datatype package generates useful simplifications +and case distinction tactics. +*) + +Pcount = HOL + Arith + + +datatype pcount = a | b | g + +end + +ML diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/IntLemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/IntLemmas.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,392 @@ +(* + File: IntLemmas.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Lemmas and tactics for "intensional" logics. + +Mostly a lifting of standard HOL lemmas. They are not required in standard +reasoning about intensional logics, which starts by unlifting proof goals +to the HOL level. +*) + + +qed_goal "substW" Intensional.thy + "[| x .= y; w |= (P::[('v::world) => 'a, 'w::world] => bool)(x) |] ==> w |= P(y)" + (fn [prem1,prem2] => [rtac (rewrite_rule ([prem1] RL [inteq_reflection]) prem2) 1]); + + +(* Lift HOL rules to intensional reasoning *) + +qed_goal "reflW" Intensional.thy "x .= x" + (fn _ => [ rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 ]); + + +qed_goal "symW" Intensional.thy "s .= t ==> t .= s" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, dtac intD 1, + rewrite_goals_tac intensional_rews, + etac sym 1 ]); + +qed_goal "not_symW" Intensional.thy "s .~= t ==> t .~= s" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, dtac intD 1, + rewrite_goals_tac intensional_rews, + etac not_sym 1 ]); + +qed_goal "transW" Intensional.thy + "[| r .= s; s .= t |] ==> r .= t" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + etac trans 1, + atac 1 ]); + +qed_goal "box_equalsW" Intensional.thy + "[| a .= b; a .= c; b .= d |] ==> c .= d" + (fn prems => [ (rtac transW 1), + (rtac transW 1), + (rtac symW 1), + (REPEAT (resolve_tac prems 1)) ]); + + +qed_goal "fun_congW" Intensional.thy + "(f::('a => 'b)) = g ==> f[x] .= g[x]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + etac fun_cong 1 ]); + +qed_goal "fun_cong2W" Intensional.thy + "(f::(['a,'b] => 'c)) = g ==> f[x,y] .= g[x,y]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + asm_full_simp_tac HOL_ss 1 ]); + +qed_goal "fun_cong3W" Intensional.thy + "(f::(['a,'b,'c] => 'd)) = g ==> f[x,y,z] .= g[x,y,z]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + asm_full_simp_tac HOL_ss 1 ]); + + +qed_goal "arg_congW" Intensional.thy "x .= y ==> (f::'a=>'b)[x] .= f[y]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + etac arg_cong 1 ]); + +qed_goal "arg_cong2W" Intensional.thy + "[| u .= v; x .= y |] ==> (f::['a,'b]=>'c)[u,x] .= f[v,y]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + REPEAT (etac subst 1), + rtac refl 1 ]); + +qed_goal "arg_cong3W" Intensional.thy + "[| r .= s; u .= v; x .= y |] ==> (f::['a,'b,'c]=>'d)[r,u,x] .= f[s,v,y]" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + REPEAT (etac subst 1), + rtac refl 1 ]); + +qed_goal "congW" Intensional.thy + "[| (f::'a=>'b) = g; x .= y |] ==> f[x] .= g[y]" + (fn prems => [ rtac box_equalsW 1, + rtac reflW 3, + rtac arg_congW 1, + resolve_tac prems 1, + rtac fun_congW 1, + rtac sym 1, + resolve_tac prems 1 ]); + +qed_goal "cong2W" Intensional.thy + "[| (f::['a,'b]=>'c) = g; u .= v; x .= y |] ==> f[u,x] .= g[v,y]" + (fn prems => [ rtac box_equalsW 1, + rtac reflW 3, + rtac arg_cong2W 1, + REPEAT (resolve_tac prems 1), + rtac fun_cong2W 1, + rtac sym 1, + resolve_tac prems 1 ]); + +qed_goal "cong3W" Intensional.thy + "[| (f::['a,'b,'c]=>'d) = g; r .= s; u .= v; x .= y |] ==> (f[r,u,x]) .= (g[s,v,y])" + (fn prems => [ rtac box_equalsW 1, + rtac reflW 3, + rtac arg_cong3W 1, + REPEAT (resolve_tac prems 1), + rtac fun_cong3W 1, + rtac sym 1, + resolve_tac prems 1 ]); + + +(** Lifted equivalence **) + +(* Note the object-level implication in the hypothesis. Meta-level implication + would not be correct! *) +qed_goal "iffIW" Intensional.thy + "[| A .-> B; B .-> A |] ==> A .= B" + (fn prems => [ cut_facts_tac prems 1, + rtac intI 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + (fast_tac prop_cs 1) ]); + +qed_goal "iffD2W" Intensional.thy + "[| (P::('w::world) form) .= Q; w |= Q |] ==> w |= P" + (fn prems => + [cut_facts_tac prems 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1 ]); + +val iffD1W = symW RS iffD2W; + +(** #True **) + +qed_goal "TrueIW" Intensional.thy "#True" + (fn _ => [rtac intI 1, rewrite_goals_tac intensional_rews, rtac TrueI 1]); + + +qed_goal "eqTrueIW" Intensional.thy "(P::('w::world) form) ==> P .= #True" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + asm_full_simp_tac HOL_ss 1] ); + +qed_goal "eqTrueEW" Intensional.thy "P .= #True ==> (P::('w::world) form)" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + asm_full_simp_tac HOL_ss 1] ); + +(** #False **) + +qed_goal "FalseEW" Intensional.thy "#False ==> P::('w::world) form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + etac FalseE 1]); + +qed_goal "False_neq_TrueW" Intensional.thy + "(#False::('w::world) form) .= #True ==> P::('w::world) form" + (fn [prem] => [rtac (prem RS eqTrueEW RS FalseEW) 1]); + + +(** Negation **) + +(* Again use object-level implication *) +qed_goal "notIW" Intensional.thy "(P .-> #False) ==> .~P" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1]); + + +qed_goal "notEWV" Intensional.thy + "[| .~P; P::('w::world) form |] ==> R::('w::world) form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + etac notE 1, atac 1]); + +(* The following rule is stronger: It is enough to detect an + inconsistency at *some* world to conclude R. Note also that P and R + are allowed to be (intensional) formulas of different types! *) + +qed_goal "notEW" Intensional.thy + "[| w |= .~P; w |= P |] ==> R::('w::world) form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + etac notE 1, atac 1]); + +(** Implication **) + +qed_goal "impIW" Intensional.thy "(!!w. (w |= A) ==> (w |= B)) ==> A .-> B" + (fn [prem] => [ rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac impI 1, + etac prem 1 ]); + + +qed_goal "mpW" Intensional.thy "[| A .-> B; w |= A |] ==> w |= B" + (fn prems => [ cut_facts_tac prems 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + etac mp 1, + atac 1 ]); + +qed_goal "impEW" Intensional.thy + "[| A .-> B; w |= A; w |= B ==> w |= C |] ==> w |= (C::('w::world) form)" + (fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]); + +qed_goal "rev_mpW" Intensional.thy "[| w |= P; P .-> Q |] ==> w |= Q" + (fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]); + +qed_goal "contraposW" Intensional.thy "[| w |= .~Q; P .-> Q |] ==> w |= .~P" + (fn [major,minor] => [rewrite_goals_tac intensional_rews, + rtac contrapos 1, + rtac (rewrite_rule intensional_rews major) 1, + etac rev_mpW 1, + rtac minor 1]); + +qed_goal "iffEW" Intensional.thy + "[| (P::('w::world) form) .= Q; [| P .-> Q; Q .-> P |] ==> R::('w::world) form |] ==> R" + (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2W, p1 RS iffD1W, p2, impIW])1)]); + + +(** Conjunction **) + +qed_goal "conjIW" Intensional.thy "[| w |= P; w |= Q |] ==> w |= P .& Q" + (fn prems => [rewrite_goals_tac intensional_rews, + REPEAT (resolve_tac ([conjI]@prems) 1)]); + +qed_goal "conjunct1W" Intensional.thy "(w |= P .& Q) ==> w |= P" + (fn prems => [cut_facts_tac prems 1, + rewrite_goals_tac intensional_rews, + etac conjunct1 1]); + +qed_goal "conjunct2W" Intensional.thy "(w |= P .& Q) ==> w |= Q" + (fn prems => [cut_facts_tac prems 1, + rewrite_goals_tac intensional_rews, + etac conjunct2 1]); + +qed_goal "conjEW" Intensional.thy + "[| w |= P .& Q; [| w |= P; w |= Q |] ==> w |= R |] ==> w |= (R::('w::world) form)" + (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1, + etac conjunct1W 1, etac conjunct2W 1]); + + +(** Disjunction **) + +qed_goal "disjI1W" Intensional.thy "w |= P ==> w |= P .| Q" + (fn [prem] => [rewrite_goals_tac intensional_rews, + rtac disjI1 1, + rtac prem 1]); + +qed_goal "disjI2W" Intensional.thy "w |= Q ==> w |= P .| Q" + (fn [prem] => [rewrite_goals_tac intensional_rews, + rtac disjI2 1, + rtac prem 1]); + +qed_goal "disjEW" Intensional.thy + "[| w |= P .| Q; P .-> R; Q .-> R |] ==> w |= R" + (fn prems => [cut_facts_tac prems 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1]); + +(** Classical propositional logic **) + +qed_goal "classicalW" Intensional.thy "(.~P .-> P) ==> P::('w::world)form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1]); + +qed_goal "notnotDW" Intensional.thy ".~.~P ==> P::('w::world) form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + etac notnotD 1]); + +qed_goal "disjCIW" Intensional.thy "(w |= .~Q .-> P) ==> (w |= P.|Q)" + (fn prems => [cut_facts_tac prems 1, + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1]); + +qed_goal "impCEW" Intensional.thy + "[| P.->Q; (w |= .~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= (R::('w::world) form)" + (fn [a1,a2,a3] => + [rtac (excluded_middle RS disjE) 1, + etac (rewrite_rule intensional_rews a2) 1, + rtac a3 1, + etac (a1 RS mpW) 1]); + +(* The following generates too many parse trees... + +qed_goal "iffCEW" Intensional.thy + "[| P .= Q; \ +\ [| (w |= P); (w |= Q) |] ==> (w |= R); \ +\ [| (w |= .~P); (w |= .~Q) |] ==> (w |= R) \ +\ |] ==> w |= (R::('w::world) form)" + +*) + +qed_goal "case_split_thmW" Intensional.thy + "[| P .-> Q; .~P .-> Q |] ==> Q::('w::world) form" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + REPEAT (dtac intD 1), + rewrite_goals_tac intensional_rews, + fast_tac prop_cs 1]); + +fun case_tacW a = res_inst_tac [("P",a)] case_split_thmW; + + +(** Rigid quantifiers **) + +qed_goal "allIW" Intensional.thy "(!!x. P(x)) ==> RALL x. P(x)" + (fn [prem] => [rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac allI 1, + rtac (prem RS intE) 1]); + +qed_goal "specW" Intensional.thy "(RALL x. P(x)) ==> P(x)" + (fn prems => [cut_facts_tac prems 1, + rtac intI 1, + dtac intD 1, + rewrite_goals_tac intensional_rews, + etac spec 1]); + + +qed_goal "allEW" Intensional.thy + "[| RALL x.P(x); P(x) ==> R |] ==> R::('w::world) form" + (fn major::prems=> + [ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]); + +qed_goal "all_dupEW" Intensional.thy + "[| RALL x.P(x); [| P(x); RALL x.P(x) |] ==> R |] ==> R::('w::world) form" + (fn prems => + [ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]); + + +qed_goal "exIW" Intensional.thy "P(x) ==> REX x.P(x)" + (fn [prem] => [rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac exI 1, + rtac (prem RS intD) 1]); + +qed_goal "exEW" Intensional.thy + "[| w |= REX x.P(x); !!x. P(x) .-> Q |] ==> w |= Q" + (fn [major,minor] => [rtac exE 1, + rtac (rewrite_rule intensional_rews major) 1, + etac rev_mpW 1, + rtac minor 1]); + +(** Classical quantifier reasoning **) + +qed_goal "exCIW" Intensional.thy + "(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x.P(x)" + (fn prems => [cut_facts_tac prems 1, + rewrite_goals_tac intensional_rews, + fast_tac HOL_cs 1]); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Intensional.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Intensional.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,209 @@ +(* + File: Intensional.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Lemmas and tactics for "intensional" logics. +*) + +val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex]; + +(** Lift usual HOL simplifications to "intensional" level. + Convert s .= t into rewrites s == t, so we can use the standard + simplifier. +**) +local + +fun prover s = (prove_goal Intensional.thy s + (fn _ => [rewrite_goals_tac (int_valid::intensional_rews), + blast_tac HOL_cs 1])) RS inteq_reflection; + +in + +val int_simps = map prover + [ "(x.=x) .= #True", + "(.~#True) .= #False", "(.~#False) .= #True", "(.~ .~ P) .= P", + "((.~P) .= P) .= #False", "(P .= (.~P)) .= #False", + "(P .~= Q) .= (P .= (.~Q))", + "(#True.=P) .= P", "(P.=#True) .= P", + "(#True .-> P) .= P", "(#False .-> P) .= #True", + "(P .-> #True) .= #True", "(P .-> P) .= #True", + "(P .-> #False) .= (.~P)", "(P .-> .~P) .= (.~P)", + "(P .& #True) .= P", "(#True .& P) .= P", + "(P .& #False) .= #False", "(#False .& P) .= #False", + "(P .& P) .= P", "(P .& .~P) .= #False", "(.~P .& P) .= #False", + "(P .| #True) .= #True", "(#True .| P) .= #True", + "(P .| #False) .= P", "(#False .| P) .= P", + "(P .| P) .= P", "(P .| .~P) .= #True", "(.~P .| P) .= #True", + "(RALL x.P) .= P", "(REX x.P) .= P", + "(.~Q .-> .~P) .= (P .-> Q)", + "(P.|Q .-> R) .= ((P.->R).&(Q.->R))" ]; + +end; + +Addsimps (intensional_rews @ int_simps); + +(* Derive introduction and destruction rules from definition of + intensional validity. +*) +qed_goal "intI" Intensional.thy "(!!w. w |= A) ==> A" + (fn prems => [rewtac int_valid, + resolve_tac prems 1 + ]); + +qed_goalw "intD" Intensional.thy [int_valid] "A ==> w |= A" + (fn [prem] => [ rtac (forall_elim_var 0 prem) 1 ]); + +(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) + +(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. + F .= G gets (w |= F) = (w |= G) + F .-> G gets (w |= F) --> (w |= G) +*) +fun int_unlift th = rewrite_rule intensional_rews (th RS intD); + +(* F .-> G becomes w |= F ==> w |= G *) +fun int_mp th = zero_var_indexes ((int_unlift th) RS mp); + +(* F .-> G becomes [| w |= F; w |= G ==> R |] ==> R + so that it can be used as an elimination rule +*) +fun int_impE th = zero_var_indexes ((int_unlift th) RS impE); + +(* F .& G .-> H becomes [| w |= F; w |= G |] ==> w |= H *) +fun int_conjmp th = zero_var_indexes (conjI RS (int_mp th)); + +(* F .& G .-> H becomes [| w |= F; w |= G; (w |= H ==> R) |] ==> R *) +fun int_conjimpE th = zero_var_indexes (conjI RS (int_impE th)); + +(* Turn F .= G into meta-level rewrite rule F == G *) +fun int_rewrite th = (rewrite_rule intensional_rews (th RS inteq_reflection)); + +(* Make the simplifier accept "intensional" goals by first unlifting them. + This is the standard way of proving "intensional" theorems; apply + int_rewrite (or action_rewrite, temp_rewrite) to convert "x .= y" into "x == y" + if you want to rewrite without unlifting. +*) +fun maybe_unlift th = + (case concl_of th of + Const("TrueInt",_) $ p => int_unlift th + | _ => th); + +simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift); + + +(* ==================== Rewrites for abstractions ==================== *) + +(* The following are occasionally useful. Don't add them to the default + simpset, or it will loop! Alternatively, we could replace the "unl_XXX" + rules by definitions of lifting via lambda abstraction, but then proof + states would have lots of lambdas, and would be hard to read. +*) + +qed_goal "con_abs" Intensional.thy "(%w. c) == #c" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift_abs" Intensional.thy "(%w. f(x w)) == (f[x])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift2_abs" Intensional.thy "(%w. f(x w) (y w)) == (f[x,y])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift2_abs_con1" Intensional.thy "(%w. f x (y w)) == (f[#x,y])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift2_abs_con2" Intensional.thy "(%w. f(x w) y) == (f[x,#y])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs" Intensional.thy "(%w. f(x w) (y w) (z w)) == (f[x,y,z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con1" Intensional.thy "(%w. f x (y w) (z w)) == (f[#x,y,z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con2" Intensional.thy "(%w. f (x w) y (z w)) == (f[x,#y,z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con3" Intensional.thy "(%w. f (x w) (y w) z) == (f[x,y,#z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con12" Intensional.thy "(%w. f x y (z w)) == (f[#x,#y,z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con13" Intensional.thy "(%w. f x (y w) z) == (f[#x,y,#z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +qed_goal "lift3_abs_con23" Intensional.thy "(%w. f (x w) y z) == (f[x,#y,#z])" + (fn _ => [rtac inteq_reflection 1, + rtac intI 1, + rewrite_goals_tac intensional_rews, + rtac refl 1 + ]); + +(* ========================================================================= *) + +qed_goal "Not_rall" Intensional.thy + "(.~ (RALL x. F(x))) .= (REX x. .~ F(x))" + (fn _ => [rtac intI 1, + rewrite_goals_tac intensional_rews, + fast_tac HOL_cs 1 + ]); + +qed_goal "Not_rex" Intensional.thy + "(.~ (REX x. F(x))) .= (RALL x. .~ F(x))" + (fn _ => [rtac intI 1, + rewrite_goals_tac intensional_rews, + fast_tac HOL_cs 1 + ]); + +(* IntLemmas.ML contains a collection of further lemmas about "intensional" logic. + These are not loaded by default because they are not required for the + standard proof procedures that first unlift proof goals to the HOL level. + +use "IntLemmas.ML"; + +*) diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Intensional.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Intensional.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,101 @@ +(* + File: TLA/Intensional.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Intensional + Logic Image: HOL + +Define a framework for "intensional" (possible-world based) logics +on top of HOL, with lifting of constants and functions. +*) + +Intensional = Prod + + +classes + world < logic (* Type class of "possible worlds". Concrete types + will be provided by children theories. *) + +types + ('a,'w) term = "'w => 'a" (* Intention: 'w::world *) + 'w form = "'w => bool" + +consts + TrueInt :: "('w::world form) => prop" ("(_)" 5) + + (* Holds at *) + holdsAt :: "['w::world, 'w form] => bool" ("(_ |= _)" [100,9] 8) + + (* Lifting base functions to "intensional" level *) + con :: "'a => ('w::world => 'a)" ("(#_)" [100] 99) + lift :: "['a => 'b, 'w::world => 'a] => ('w => 'b)" ("(_[_])") + lift2 :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])") + lift3 :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])") + + (* Lifted infix functions *) + IntEqu :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .=/ _)" [50,51] 50) + IntNeq :: "['w::world => 'a, 'w => 'a] => 'w form" ("(_ .~=/ _)" [50,51] 50) + NotInt :: "('w::world) form => 'w form" ("(.~ _)" [40] 40) + AndInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .&/ _)" [36,35] 35) + OrInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .|/ _)" [31,30] 30) + ImpInt :: "[('w::world) form, 'w form] => 'w form" ("(_ .->/ _)" [26,25] 25) + IfInt :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10) + PlusInt :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)" ("(_ .+/ _)" [66,65] 65) + MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)" ("(_ .-/ _)" [66,65] 65) + TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)" ("(_ .*/ _)" [71,70] 70) + + LessInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .< _)" [50, 51] 50) + LeqInt :: "['w::world => 'a::ord, 'w => 'a] => 'w form" ("(_/ .<= _)" [50, 51] 50) + + (* lifted set membership *) + memInt :: "[('a,'w::world) term, ('a set,'w) term] => 'w form" ("(_/ .: _)" [50, 51] 50) + + (* "Rigid" quantification *) + RAll :: "('a => 'w::world form) => 'w form" (binder "RALL " 10) + REx :: "('a => 'w::world form) => 'w form" (binder "REX " 10) + +syntax + "@tupleInt" :: "args => ('a * 'b, 'w) term" ("(1{[_]})") + +translations + + "{[x,y,z]}" == "{[x, {[y,z]} ]}" + "{[x,y]}" == "Pair [x, y]" + "{[x]}" => "x" + + "u .= v" == "op =[u,v]" + "u .~= v" == ".~(u .= v)" + ".~ A" == "Not[A]" + "A .& B" == "op &[A,B]" + "A .| B" == "op |[A,B]" + "A .-> B" == "op -->[A,B]" + ".if A .then u .else v" == "If[A,u,v]" + "u .+ v" == "op +[u,v]" + "u .- v" == "op -[u,v]" + "u .* v" == "op *[u,v]" + + "a .< b" == "op < [a,b]" + "a .<= b" == "op <= [a,b]" + "a .: A" == "op :[a,A]" + + "holdsAt w (lift f x)" == "lift f x w" + "holdsAt w (lift2 f x y)" == "lift2 f x y w" + "holdsAt w (lift3 f x y z)" == "lift3 f x y z w" + + "w |= A" => "A(w)" + +rules + inteq_reflection "(x .= y) ==> (x == y)" + + int_valid "TrueInt(A) == (!! w. w |= A)" + + unl_con "(#c) w == c" (* constants *) + unl_lift "(f[x]) w == f(x w)" + unl_lift2 "(f[x,y]) w == f (x w) (y w)" + unl_lift3 "(f[x, y, z]) w == f (x w) (y w) (z w)" + + unl_Rall "(RALL x. A(x)) w == ALL x. (w |= A(x))" + unl_Rex "(REX x. A(x)) w == EX x. (w |= A(x))" +end + +ML diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MIParameters.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MIParameters.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,17 @@ +(* + File: MIParameters.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: MIParameters + Logic Image: TLA + + RPC-Memory example: Parameters of the memory implementation. +*) + +MIParameters = Arith + + +datatype histState = histA | histB + +end + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MIlive.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MIlive.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,382 @@ +(* + File: MIlive.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Lower-level lemmas for the liveness proof +*) + +(* Liveness assertions for the different implementation states, based on the + fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas + for readability. Reuse action proofs from safety part. +*) + +(* ------------------------------ State S1 ------------------------------ *) + +qed_goal "S1_successors" MemoryImplementation.thy + "$(S1 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> $(S1 rmhist p)` .| $(S2 rmhist p)`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_1]) + ]); + +(* Show that the implementation can satisfy the high-level fairness requirements + by entering the state S1 infinitely often. +*) + +qed_goal "S1_RNextdisabled" MemoryImplementation.thy + "$(S1 rmhist p) .-> \ +\ .~$(Enabled (_))" + (fn _ => [action_simp_tac (!simpset addsimps [angle_def,S_def,S1_def]) + [notI] [enabledE,MemoryidleE] 1, + auto_tac MI_fast_css + ]); + +qed_goal "S1_Returndisabled" MemoryImplementation.thy + "$(S1 rmhist p) .-> \ +\ .~$(Enabled (_))" + (fn _ => [action_simp_tac (!simpset addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def]) + [notI] [enabledE] 1 + ]); + +qed_goal "RNext_fair" MemoryImplementation.thy + "!!sigma. (sigma |= []<>($(S1 rmhist p))) \ +\ ==> (sigma |= WF(RNext memCh mem (resbar rmhist) p)_)" + (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt] + addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]) + ]); + +qed_goal "Return_fair" MemoryImplementation.thy + "!!sigma. (sigma |= []<>($(S1 rmhist p))) \ +\ ==> (sigma |= WF(MemReturn memCh (resbar rmhist) p)_)" + (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt] + addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]) + ]); + +(* ------------------------------ State S2 ------------------------------ *) + +qed_goal "S2_successors" MemoryImplementation.thy + "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(S2 rmhist p)` .| $(S3 rmhist p)`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_2]) + ]); + +qed_goal "S2MClkFwd_successors" MemoryImplementation.thy + "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .& _(c p) \ +\ .-> $(S3 rmhist p)`" + (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_2]) ]); + +qed_goal "S2MClkFwd_enabled" MemoryImplementation.thy + "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(Enabled (_(c p)))" + (fn _ => [cut_facts_tac [MI_base] 1, + auto_tac (MI_css addsimps2 [c_def,base_pair] + addSIs2 [MClkFwd_ch_enabled,action_mp MClkFwd_enabled]), + ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S2_def]) [] []) + ]); + +qed_goal "S2_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) .& WF(MClkFwd memCh crCh cst p)_(c p) \ +\ .-> ($(S2 rmhist p) ~> $(S3 rmhist p))" + (fn _ => [REPEAT (resolve_tac [WF1,S2_successors, + S2MClkFwd_successors,S2MClkFwd_enabled] 1) + ]); + + +(* ------------------------------ State S3 ------------------------------ *) + +qed_goal "S3_successors" MemoryImplementation.thy + "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(S3 rmhist p)` .| ($(S4 rmhist p) .| $(S6 rmhist p))`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_3]) + ]); + +qed_goal "S3RPC_successors" MemoryImplementation.thy + "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .& _(r p) \ +\ .-> ($(S4 rmhist p) .| $(S6 rmhist p))`" + (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_3]) ]); + +qed_goal "S3RPC_enabled" MemoryImplementation.thy + "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(Enabled (_(r p)))" + (fn _ => [cut_facts_tac [MI_base] 1, + auto_tac (MI_css addsimps2 [r_def,base_pair] + addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]), + ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S3_def]) [] []) + ]); + +qed_goal "S3_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) \ +\ .& WF(RPCNext crCh rmCh rst p)_(r p) \ +\ .-> ($(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p)))" + (fn _ => [REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)]); + +(* ------------- State S4 -------------------------------------------------- *) + +qed_goal "S4_successors" MemoryImplementation.thy + "$(S4 rmhist p) .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .-> $(S4 rmhist p)` .| $(S5 rmhist p)`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_4]) + ]); + +(* ------------- State S4a: S4 /\ (ires p = NotAResult) ------------------------------ *) + +qed_goal "S4a_successors" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .-> ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult))` \ +\ .| (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`" + (fn _ => [split_idle_tac [m_def] 1, + auto_tac (MI_css addsimps2 [m_def] addSEs2 [action_conjimpE Step1_2_4]) + ]); + +qed_goal "S4aRNext_successors" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .& _(m p) \ +\ .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`" + (fn _ => [auto_tac (MI_css addsimps2 [angle_def] + addSEs2 [action_conjimpE Step1_2_4, + action_conjimpE ReadResult, action_impE WriteResult]) + ]); + +qed_goal "S4aRNext_enabled" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .-> $(Enabled (_(m p)))" + (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [action_mp RNext_enabled]), + ALLGOALS (cut_facts_tac [MI_base]), + auto_tac (MI_css addsimps2 [base_pair]), + (* it's faster to expand S4 only where necessary *) + action_simp_tac (!simpset addsimps [S_def,S4_def]) [] [] 1 + ]); + +qed_goal "S4a_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_ .& (RALL l. $(MemInv mem l))) \ +\ .& WF(RNext rmCh mem ires p)_(m p) \ +\ .-> (($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))" + (fn _ => [rtac WF1 1, + ALLGOALS (action_simp_tac (!simpset) + (map ((rewrite_rule [slice_def]) o action_mp) + [S4a_successors,S4aRNext_successors,S4aRNext_enabled]) + []) + ]); + +(* ------------- State S4b: S4 /\ (ires p # NotAResult) ------------------------------ *) + +qed_goal "S4b_successors" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .-> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))` .| $(S5 rmhist p)`" + (fn _ => [split_idle_tac [m_def] 1, + auto_tac (MI_css addSEs2 (action_impE WriteResult + :: map action_conjimpE [Step1_2_4,ReadResult])) + ]); + +qed_goal "S4bReturn_successors" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .& _(m p) \ +\ .-> ($(S5 rmhist p))`" + (fn _ => [auto_tac (MI_css addsimps2 [angle_def] + addSEs2 [action_conjimpE Step1_2_4] + addEs2 [action_conjimpE ReturnNotReadWrite]) + ]); + +qed_goal "S4bReturn_enabled" MemoryImplementation.thy + "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ +\ .& (ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l))) \ +\ .-> $(Enabled (_(m p)))" + (fn _ => [cut_facts_tac [MI_base] 1, + auto_tac (MI_css addsimps2 [m_def,base_pair] + addSIs2 [action_mp MemReturn_enabled]), + ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S4_def]) [] []) + ]); + +qed_goal "S4b_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_ .& (RALL l. $(MemInv mem l))) \ +\ .& WF(MemReturn rmCh ires p)_(m p) \ +\ .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p))" + (fn _ => [rtac WF1 1, + ALLGOALS (action_simp_tac (!simpset) + (map ((rewrite_rule [slice_def]) o action_mp) + [S4b_successors,S4bReturn_successors,S4bReturn_enabled]) + [allE]) + ]); + +(* ------------------------------ State S5 ------------------------------ *) + +qed_goal "S5_successors" MemoryImplementation.thy + "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(S5 rmhist p)` .| $(S6 rmhist p)`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_5]) + ]); + +qed_goal "S5RPC_successors" MemoryImplementation.thy + "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .& _(r p) \ +\ .-> $(S6 rmhist p)`" + (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_5]) ]); + +qed_goal "S5RPC_enabled" MemoryImplementation.thy + "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(Enabled (_(r p)))" + (fn _ => [cut_facts_tac [MI_base] 1, + auto_tac (MI_css addsimps2 [r_def,base_pair] + addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]), + ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S5_def]) [] []) + ]); + +qed_goal "S5_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) \ +\ .& WF(RPCNext crCh rmCh rst p)_(r p) \ +\ .-> ($(S5 rmhist p) ~> $(S6 rmhist p))" + (fn _ => [REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)]); + + +(* ------------------------------ State S6 ------------------------------ *) + +qed_goal "S6_successors" MemoryImplementation.thy + "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .-> $(S1 rmhist p)` .| $(S3 rmhist p)` .| $(S6 rmhist p)`" + (fn _ => [split_idle_tac [] 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_6]) + ]); + +qed_goal "S6MClkReply_successors" MemoryImplementation.thy + "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_) \ +\ .& _(c p) \ +\ .-> $(S1 rmhist p)`" + (fn _ => [auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_6, + action_impE MClkReplyNotRetry]) + ]); + +qed_goal "MClkReplyS6" MemoryImplementation.thy + "$(ImpInv rmhist p) .& _(c p) .-> $(S6 rmhist p)" + (fn _ => [action_simp_tac + (!simpset addsimps + [angle_def,MClkReply_def,Return_def, + ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def]) + [] [] 1 + ]); + +qed_goal "S6MClkReply_enabled" MemoryImplementation.thy + "$(S6 rmhist p) .-> $(Enabled (_(c p)))" + (fn _ => [cut_facts_tac [MI_base] 1, + auto_tac (MI_css addsimps2 [c_def,base_pair] + addSIs2 [action_mp MClkReply_enabled]), + ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S6_def]) [] []) + ]); + +qed_goal "S6_live" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_ .& $(ImpInv rmhist p)) \ +\ .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p)) \ +\ .-> []<>($(S1 rmhist p))" + (fn _ => [Auto_tac(), + subgoal_tac "sigma |= []<>(_(c p))" 1, + eres_inst_tac [("P","_(c p)")] + EnsuresInfinite 1, atac 1, + action_simp_tac (!simpset) [] + (map action_conjimpE [MClkReplyS6,S6MClkReply_successors]) 1, + auto_tac (MI_css addsimps2 [SF_def]), + etac swap 1, + auto_tac (MI_css addSIs2 [action_mp S6MClkReply_enabled] + addSEs2 [STL4E,DmdImplE]) + ]); + +(* ------------------------------ complex leadsto properties ------------------------------ *) + +qed_goal "S5S6LeadstoS6" MemoryImplementation.thy + "!!sigma. (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) \ +\ ==> (sigma |= ($(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" + (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro, + temp_unlift LatticeReflexivity]) + ]); + +qed_goal "S4bS5S6LeadstoS6" MemoryImplementation.thy + "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ +\ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ +\ ==> (sigma |= (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" + (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6] + addIs2 [LatticeTransitivity]) + ]); + +qed_goal "S4S5S6LeadstoS6" MemoryImplementation.thy + "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ +\ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ +\ ==> (sigma |= ($(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" + (fn _ => [subgoal_tac "sigma |= (($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) .| ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p)" 1, + eres_inst_tac [("G", "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) .| ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)")] LatticeTransitivity 1, + SELECT_GOAL (auto_tac (MI_css addSIs2 [ImplLeadsto, temp_unlift necT])) 1, + rtac LatticeDisjunctionIntro 1, + etac LatticeTransitivity 1, + etac LatticeTriangle 1, atac 1, + auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6]) + ]); + +qed_goal "S3S4S5S6LeadstoS6" MemoryImplementation.thy + "!!sigma. [| (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ +\ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ +\ ==> (sigma |= ($(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" + (fn _ => [rtac LatticeDisjunctionIntro 1, + rtac LatticeTriangle 1, atac 2, + rtac (S4S5S6LeadstoS6 RS LatticeTransitivity) 1, + auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,temp_unlift necT] + addIs2 [ImplLeadsto]) + ]); + +qed_goal "S2S3S4S5S6LeadstoS6" MemoryImplementation.thy + "!!sigma. [| (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \ +\ (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ +\ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ +\ ==> (sigma |= ($(S2 rmhist p) .| $(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" + (fn _ => [rtac LatticeDisjunctionIntro 1, + rtac LatticeTransitivity 1, atac 2, + rtac (S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1, + auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,temp_unlift necT] + addIs2 [ImplLeadsto]) + ]); + +qed_goal "NotS1LeadstoS6" MemoryImplementation.thy + "!!sigma. [| (sigma |= []($(ImpInv rmhist p))); \ +\ (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \ +\ (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ +\ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ +\ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ +\ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ +\ ==> (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p))" + (fn _ => [rtac (S2S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1, + auto_tac (MI_css addsimps2 [ImpInv_def] addIs2 [ImplLeadsto] addSEs2 [STL4E]) + ]); + +qed_goal "S1Infinite" MemoryImplementation.thy + "!!sigma. [| (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p)); \ +\ (sigma |= []<>($(S6 rmhist p)) .-> []<>($(S1 rmhist p))) |] \ +\ ==> (sigma |= []<>($(S1 rmhist p)))" + (fn _ => [rtac classical 1, + asm_full_simp_tac (!simpset addsimps [NotBox, temp_rewrite NotDmd]) 1, + auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [temp_mp DBImplBDAct]) + ]); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MIsafe.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MIsafe.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,449 @@ +(* + File: MIsafe.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Lower-level lemmas about memory implementation (safety) +*) + +(* ========================= Lemmas about values ========================= *) + +(* RPCFailure notin MemVals U {OK,BadArg} *) + +qed_goal "MVOKBAnotRF" MemoryImplementation.thy + "!!x. MVOKBA x ==> x ~= RPCFailure" + (fn _ => [ auto_tac (HOL_css addsimps2 (RP_simps @ [MVOKBA_def])) ]); +bind_thm("MVOKBAnotRFE", make_elim MVOKBAnotRF); + +(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *) + +qed_goal "MVOKBARFnotNR" MemoryImplementation.thy + "!!x. MVOKBARF x ==> x ~= NotAResult" + (fn _ => [ auto_tac (HOL_css addsimps2 (RP_simps @ [MVOKBARF_def]) + addSEs2 [MemValNotAResultE]) + ]); +bind_thm("MVOKBARFnotNRE", make_elim MVOKBARFnotNR); + +(* ========================= Si's are mutually exclusive ==================================== *) +(* Si and Sj are mutually exclusive for i # j. This helps to simplify the big + conditional in the definition of resbar when doing the step-simulation proof. + We prove a weaker result, which suffices for our purposes: + Si implies (not Sj), for j $(S1 rmhist p) .& .~$(S2 rmhist p) .& .~$(S3 rmhist p) .& \ +\ .~$(S4 rmhist p) .& .~$(S5 rmhist p) .& .~$(S6 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def, + S3_def, S4_def, S5_def, S6_def]) + ]); +*) + +qed_goal "S2_excl" MemoryImplementation.thy + "$(S2 rmhist p) .-> $(S2 rmhist p) .& .~$(S1 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def]) ]); +bind_thm("S2_exclE", action_impE S2_excl); + +qed_goal "S3_excl" MemoryImplementation.thy + "$(S3 rmhist p) .-> $(S3 rmhist p) .& .~$(S1 rmhist p) .& .~$(S2 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def, S3_def]) ]); +bind_thm("S3_exclE", action_impE S3_excl); + +qed_goal "S4_excl" MemoryImplementation.thy + "$(S4 rmhist p) .-> $(S4 rmhist p) .& .~$(S1 rmhist p) .& .~$(S2 rmhist p) .& .~$(S3 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def]) ]); +bind_thm("S4_exclE", action_impE S4_excl); + +qed_goal "S5_excl" MemoryImplementation.thy + "$(S5 rmhist p) .-> $(S5 rmhist p) .& .~$(S1 rmhist p) .& .~$(S2 rmhist p) .& \ +\ .~$(S3 rmhist p) .& .~$(S4 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def,S5_def]) ]); +bind_thm("S5_exclE", action_impE S5_excl); + +qed_goal "S6_excl" MemoryImplementation.thy + "$(S6 rmhist p) .-> $(S6 rmhist p) .& .~$(S1 rmhist p) .& .~$(S2 rmhist p) .& \ +\ .~$(S3 rmhist p) .& .~$(S4 rmhist p) .& .~$(S5 rmhist p)" + (fn _ => [ auto_tac (MI_css addsimps2 [S_def,S1_def,S2_def,S3_def,S4_def,S5_def,S6_def]) ]); +bind_thm("S6_exclE", action_impE S6_excl); + + +(* ==================== Lemmas about the environment ============================== *) + +qed_goal "Envbusy" MemoryImplementation.thy + "$(Calling memCh p) .-> .~ ENext p" + (fn _ => [ auto_tac (MI_css addsimps2 [ENext_def,Call_def]) ]); + +(* ==================== Lemmas about the implementation's states ==================== *) + +(* The following series of lemmas are used in establishing the implementation's + next-state relation (Step 1.2 of the proof in the paper). For each state Si, we + establish which component actions are possible and their results. +*) + +(* ------------------------------ State S1 ---------------------------------------- *) + +qed_goal "S1Env" MemoryImplementation.thy + "(ENext p) .& $(S1 rmhist p) .& unchanged .-> (S2 rmhist p)$" + (fn _ => [auto_tac (MI_css + addsimps2 [ENext_def,Call_def,c_def,r_def,m_def, + caller_def,rtrner_def,MVNROKBA_def, + S_def,S1_def,S2_def,Calling_def]) + ]); +bind_thm("S1EnvE", action_conjimpE S1Env); + +qed_goal "S1ClerkUnch" MemoryImplementation.thy + "[MClkNext memCh crCh cst p]_(c p) .& $(S1 rmhist p) .-> unchanged (c p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_conjimpE MClkidle] + addsimps2 [square_def,S_def,S1_def]) + ]); +bind_thm("S1ClerkUnchE", action_conjimpE S1ClerkUnch); + +qed_goal "S1RPCUnch" MemoryImplementation.thy + "[RPCNext crCh rmCh rst p]_(r p) .& $(S1 rmhist p) .-> unchanged (r p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_impE RPCidle] + addsimps2 [square_def,S_def,S1_def]) + ]); +bind_thm("S1RPCUnchE", action_conjimpE S1RPCUnch); + +qed_goal "S1MemUnch" MemoryImplementation.thy + "[RNext rmCh mem ires p]_(m p) .& $(S1 rmhist p) .-> unchanged (m p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_impE Memoryidle] + addsimps2 [square_def,S_def,S1_def]) + ]); +bind_thm("S1MemUnchE", action_conjimpE S1MemUnch); + +qed_goal "S1Hist" MemoryImplementation.thy + "[HNext rmhist p]_ .& $(S1 rmhist p) .-> unchanged (rmhist@p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,HNext_def,MemReturn_def, + RPCFail_def,MClkReply_def,Return_def, + S_def,S1_def]) + ]); +bind_thm("S1HistE", action_conjimpE S1Hist); + +(* ------------------------------ State S2 ---------------------------------------- *) + +qed_goal "S2EnvUnch" MemoryImplementation.thy + "[ENext p]_(e p) .& $(S2 rmhist p) .-> unchanged (e p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_impE Envbusy] + addsimps2 [square_def,S_def,S2_def]) + ]); +bind_thm("S2EnvUnchE", action_conjimpE S2EnvUnch); + +qed_goal "S2Clerk" MemoryImplementation.thy + "MClkNext memCh crCh cst p .& $(S2 rmhist p) .-> MClkFwd memCh crCh cst p" + (fn _ => [auto_tac (MI_fast_css addsimps2 [MClkNext_def,MClkRetry_def,MClkReply_def, + S_def,S2_def]) + ]); +bind_thm("S2ClerkE", action_conjimpE S2Clerk); + +(* The dumb action_simp_tac wins 15 : 129 over auto_tac *) +qed_goal "S2Forward" MemoryImplementation.thy + "$(S2 rmhist p) .& (MClkFwd memCh crCh cst p) .& unchanged \ +\ .-> (S3 rmhist p)$" + (fn _ => [action_simp_tac (!simpset addsimps + [MClkFwd_def,Call_def,e_def,r_def,m_def,caller_def,rtrner_def, + S_def,S2_def,S3_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S2ForwardE", action_conjimpE S2Forward); + +qed_goal "S2RPCUnch" MemoryImplementation.thy + "[RPCNext crCh rmCh rst p]_(r p) .& $(S2 rmhist p) .-> unchanged (r p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S2_def] + addSEs2 [action_impE RPCidle]) + ]); +bind_thm("S2RPCUnchE", action_conjimpE S2RPCUnch); + +qed_goal "S2MemUnch" MemoryImplementation.thy + "[RNext rmCh mem ires p]_(m p) .& $(S2 rmhist p) .-> unchanged (m p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S2_def] + addSEs2 [action_impE Memoryidle]) + ]); +bind_thm("S2MemUnchE", action_conjimpE S2MemUnch); + +qed_goal "S2Hist" MemoryImplementation.thy + "[HNext rmhist p]_ .& $(S2 rmhist p) .-> unchanged (rmhist@p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [square_def,HNext_def,MemReturn_def, + RPCFail_def,MClkReply_def,Return_def,S_def,S2_def]) + ]); +bind_thm("S2HistE", action_conjimpE S2Hist); + +(* ------------------------------ State S3 ---------------------------------------- *) + +qed_goal "S3EnvUnch" MemoryImplementation.thy + "[ENext p]_(e p) .& $(S3 rmhist p) .-> unchanged (e p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_impE Envbusy] + addsimps2 [square_def,S_def,S3_def]) + ]); +bind_thm("S3EnvUnchE", action_conjimpE S3EnvUnch); + +qed_goal "S3ClerkUnch" MemoryImplementation.thy + "[MClkNext memCh crCh cst p]_(c p) .& $(S3 rmhist p) .-> unchanged (c p)" + (fn _ => [auto_tac (MI_fast_css addSEs2 [action_impE MClkbusy] + addsimps2 [square_def,S_def,S3_def]) + ]); +bind_thm("S3ClerkUnchE", action_conjimpE S3ClerkUnch); + +qed_goal "S3LegalRcvArg" MemoryImplementation.thy + "$(S3 rmhist p) .-> IsLegalRcvArg[ arg[$(crCh@p)] ]" + (fn _ => [action_simp_tac + (!simpset addsimps [IsLegalRcvArg_def,MClkRelayArg_def,S_def,S3_def]) + [exI] [] 1 + ]); + +qed_goal "S3RPC" MemoryImplementation.thy + "(RPCNext crCh rmCh rst p) .& $(S3 rmhist p) \ +\ .-> (RPCFwd crCh rmCh rst p) .| (RPCFail crCh rmCh rst p)" + (fn _ => [auto_tac MI_css, + etac ((rewrite_rule action_rews (S3LegalRcvArg RS actionD)) RS impdupE) 1, + auto_tac (MI_css addsimps2 [RPCNext_def,RPCReject_def,RPCReply_def,S_def,S3_def]) + ]); +bind_thm("S3RPCE", action_conjimpE S3RPC); + +qed_goal "S3Forward" MemoryImplementation.thy + "(RPCFwd crCh rmCh rst p) .& HNext rmhist p .& $(S3 rmhist p) .& unchanged \ +\ .-> (S4 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [action_simp_tac + (!simpset addsimps [RPCFwd_def,HNext_def,MemReturn_def,RPCFail_def,MClkReply_def, + Return_def,Call_def,e_def,c_def,m_def,caller_def,rtrner_def, + S_def,S3_def,S4_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S3ForwardE", action_conjimpE S3Forward); + +qed_goal "S3Fail" MemoryImplementation.thy + "(RPCFail crCh rmCh rst p) .& $(S3 rmhist p) .& HNext rmhist p .& unchanged \ +\ .-> (S6 rmhist p)$" + (fn _ => [action_simp_tac + (!simpset addsimps [HNext_def,RPCFail_def,Return_def,e_def,c_def,m_def, + caller_def,rtrner_def,MVOKBARF_def, + S_def,S3_def,S6_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S3FailE", action_conjimpE S3Fail); + +qed_goal "S3MemUnch" MemoryImplementation.thy + "[RNext rmCh mem ires p]_(m p) .& $(S3 rmhist p) .-> unchanged (m p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S3_def] + addSEs2 [action_impE Memoryidle]) + ]); +bind_thm("S3MemUnchE", action_conjimpE S3MemUnch); + +qed_goal "S3Hist" MemoryImplementation.thy + "HNext rmhist p .& $(S3 rmhist p) .& unchanged (r p) .-> unchanged (rmhist@p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [HNext_def,MemReturn_def,RPCFail_def,MClkReply_def, + Return_def,r_def,rtrner_def,S_def,S3_def,Calling_def]) + ]); +bind_thm("S3HistE", action_conjimpE S3Hist); + + +(* ------------------------------ State S4 ---------------------------------------- *) + +qed_goal "S4EnvUnch" MemoryImplementation.thy + "[ENext p]_(e p) .& $(S4 rmhist p) .-> unchanged (e p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S4_def] + addSEs2 [action_impE Envbusy]) + ]); +bind_thm("S4EnvUnchE", action_conjimpE S4EnvUnch); + +qed_goal "S4ClerkUnch" MemoryImplementation.thy + "[MClkNext memCh crCh cst p]_(c p) .& $(S4 rmhist p) .-> unchanged (c p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S4_def] + addSEs2 [action_impE MClkbusy]) + ]); +bind_thm("S4ClerkUnchE", action_conjimpE S4ClerkUnch); + +qed_goal "S4RPCUnch" MemoryImplementation.thy + "[RPCNext crCh rmCh rst p]_(r p) .& $(S4 rmhist p) .-> unchanged (r p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S4_def] + addSEs2 [action_conjimpE RPCbusy]) + ]); +bind_thm("S4RPCUnchE", action_conjimpE S4RPCUnch); + +qed_goal "S4ReadInner" MemoryImplementation.thy + "(ReadInner rmCh mem ires p l) .& $(S4 rmhist p) .& unchanged \ +\ .& (HNext rmhist p) .& $(MemInv mem l) \ +\ .-> (S4 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [action_simp_tac + (!simpset addsimps [ReadInner_def,GoodRead_def, BadRead_def,HNext_def, + MemReturn_def, RPCFail_def,MClkReply_def,Return_def, + e_def,c_def,r_def,rtrner_def,caller_def,MVNROKBA_def, + S_def,S4_def,RdRequest_def,Calling_def,MemInv_def]) + [] [] 1 + ]); + +qed_goal "S4Read" MemoryImplementation.thy + "(Read rmCh mem ires p) .& $(S4 rmhist p) .& unchanged \ +\ .& (HNext rmhist p) .& (RALL l. $(MemInv mem l)) \ +\ .-> (S4 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [Read_def] + addSEs2 [action_conjimpE S4ReadInner]) + ]); +bind_thm("S4ReadE", action_conjimpE S4Read); + +qed_goal "S4WriteInner" MemoryImplementation.thy + "(WriteInner rmCh mem ires p l v) .& $(S4 rmhist p) .& unchanged .& (HNext rmhist p) \ +\ .-> (S4 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [action_simp_tac + (!simpset addsimps [WriteInner_def,GoodWrite_def, BadWrite_def,HNext_def, + MemReturn_def,RPCFail_def,MClkReply_def,Return_def, + e_def,c_def,r_def,rtrner_def,caller_def,MVNROKBA_def, + S_def,S4_def,WrRequest_def,Calling_def]) + [] [] 1 + ]); + +qed_goal "S4Write" MemoryImplementation.thy + "(Write rmCh mem ires p l) .& $(S4 rmhist p) .& unchanged .& (HNext rmhist p) \ +\ .-> (S4 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [ auto_tac (MI_css addsimps2 [Write_def] addSEs2 [action_conjimpE S4WriteInner]) ]); +bind_thm("S4WriteE", action_conjimpE S4Write); + +qed_goal "WriteS4" MemoryImplementation.thy + "$(ImpInv rmhist p) .& (Write rmCh mem ires p l) .-> $(S4 rmhist p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [Write_def,WriteInner_def,ImpInv_def,WrRequest_def, + S_def,S1_def,S2_def,S3_def,S4_def,S5_def,S6_def]) + ]); +bind_thm("WriteS4E", action_conjimpE WriteS4); + +qed_goal "S4Return" MemoryImplementation.thy + "(MemReturn rmCh ires p) .& $(S4 rmhist p) .& unchanged .& (HNext rmhist p) \ +\ .-> (S5 rmhist p)$" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [HNext_def,MemReturn_def,Return_def,e_def,c_def,r_def, + rtrner_def,caller_def,MVNROKBA_def,MVOKBA_def, + S_def,S4_def,S5_def,Calling_def]) + ]); +bind_thm("S4ReturnE", action_conjimpE S4Return); + +qed_goal "S4Hist" MemoryImplementation.thy + "(HNext rmhist p) .& $(S4 rmhist p) .& (m p)$ .= $(m p) .-> (rmhist@p)$ .= $(rmhist@p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [HNext_def,MemReturn_def,RPCFail_def,MClkReply_def, + Return_def,m_def,rtrner_def,S_def,S4_def,Calling_def]) + ]); +bind_thm("S4HistE", action_conjimpE S4Hist); + +(* ------------------------------ State S5 ---------------------------------------- *) + +qed_goal "S5EnvUnch" MemoryImplementation.thy + "[ENext p]_(e p) .& $(S5 rmhist p) .-> unchanged (e p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S5_def] + addSEs2 [action_impE Envbusy]) + ]); +bind_thm("S5EnvUnchE", action_conjimpE S5EnvUnch); + +qed_goal "S5ClerkUnch" MemoryImplementation.thy + "[MClkNext memCh crCh cst p]_(c p) .& $(S5 rmhist p) .-> unchanged (c p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S5_def] + addSEs2 [action_impE MClkbusy]) + ]); +bind_thm("S5ClerkUnchE", action_conjimpE S5ClerkUnch); + +qed_goal "S5RPC" MemoryImplementation.thy + "(RPCNext crCh rmCh rst p) .& $(S5 rmhist p) \ +\ .-> (RPCReply crCh rmCh rst p) .| (RPCFail crCh rmCh rst p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [RPCNext_def,RPCReject_def,RPCFwd_def,S_def,S5_def]) + ]); +bind_thm("S5RPCE", action_conjimpE S5RPC); + +qed_goal "S5Reply" MemoryImplementation.thy + "(RPCReply crCh rmCh rst p) .& $(S5 rmhist p) .& unchanged \ +\ .-> (S6 rmhist p)$" + (fn _ => [action_simp_tac + (!simpset + addsimps [RPCReply_def,Return_def,e_def,c_def,m_def, + MVOKBA_def,MVOKBARF_def,caller_def,rtrner_def, + S_def,S5_def,S6_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S5ReplyE", action_conjimpE S5Reply); + +qed_goal "S5Fail" MemoryImplementation.thy + "(RPCFail crCh rmCh rst p) .& $(S5 rmhist p) .& unchanged \ +\ .-> (S6 rmhist p)$" + (fn _ => [action_simp_tac + (!simpset + addsimps [RPCFail_def,Return_def,e_def,c_def,m_def, + MVOKBARF_def,caller_def,rtrner_def, + S_def,S5_def,S6_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S5FailE", action_conjimpE S5Fail); + +qed_goal "S5MemUnch" MemoryImplementation.thy + "[RNext rmCh mem ires p]_(m p) .& $(S5 rmhist p) .-> unchanged (m p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S5_def] + addSEs2 [action_impE Memoryidle]) + ]); +bind_thm("S5MemUnchE", action_conjimpE S5MemUnch); + +qed_goal "S5Hist" MemoryImplementation.thy + "[HNext rmhist p]_ .& $(S5 rmhist p) .-> (rmhist@p)$ .= $(rmhist@p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [square_def,HNext_def,MemReturn_def, + RPCFail_def,MClkReply_def,Return_def,S_def,S5_def]) + ]); +bind_thm("S5HistE", action_conjimpE S5Hist); + +(* ------------------------------ State S6 ---------------------------------------- *) + +qed_goal "S6EnvUnch" MemoryImplementation.thy + "[ENext p]_(e p) .& $(S6 rmhist p) .-> unchanged (e p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S6_def] + addSEs2 [action_impE Envbusy]) + ]); +bind_thm("S6EnvUnchE", action_conjimpE S6EnvUnch); + +qed_goal "S6Clerk" MemoryImplementation.thy + "(MClkNext memCh crCh cst p) .& $(S6 rmhist p) \ +\ .-> (MClkRetry memCh crCh cst p) .| (MClkReply memCh crCh cst p)" + (fn _ => [ auto_tac (MI_fast_css addsimps2 [MClkNext_def,MClkFwd_def,S_def,S6_def]) ]); +bind_thm("S6ClerkE", action_conjimpE S6Clerk); + +qed_goal "S6Retry" MemoryImplementation.thy + "(MClkRetry memCh crCh cst p) .& (HNext rmhist p) .& $(S6 rmhist p) .& unchanged \ +\ .-> (S3 rmhist p)$ .& unchanged (rmhist@p)" + (fn _ => [action_simp_tac + (!simpset addsimps [HNext_def,MClkReply_def,MClkRetry_def,Call_def, + Return_def,e_def,r_def,m_def,caller_def,rtrner_def, + S_def,S6_def,S3_def,Calling_def]) + [] [] 1]); +bind_thm("S6RetryE", action_conjimpE S6Retry); + +qed_goal "S6Reply" MemoryImplementation.thy + "(MClkReply memCh crCh cst p) .& (HNext rmhist p) .& $(S6 rmhist p) .& unchanged \ +\ .-> (S1 rmhist p)$" + (fn _ => [action_simp_tac (!simpset + addsimps [HNext_def,MemReturn_def,RPCFail_def,Return_def, + MClkReply_def,e_def,r_def,m_def,caller_def,rtrner_def, + S_def,S6_def,S1_def,Calling_def]) + [] [] 1 + ]); +bind_thm("S6ReplyE", action_conjimpE S6Reply); + +qed_goal "S6RPCUnch" MemoryImplementation.thy + "[RPCNext crCh rmCh rst p]_(r p) .& $(S6 rmhist p) .-> unchanged (r p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S6_def] + addSEs2 [action_impE RPCidle]) + ]); +bind_thm("S6RPCUnchE", action_conjimpE S6RPCUnch); + +qed_goal "S6MemUnch" MemoryImplementation.thy + "[RNext rmCh mem ires p]_(m p) .& $(S6 rmhist p) .-> unchanged (m p)" + (fn _ => [auto_tac (MI_fast_css addsimps2 [square_def,S_def,S6_def] + addSEs2 [action_impE Memoryidle]) + ]); +bind_thm("S6MemUnchE", action_conjimpE S6MemUnch); + +qed_goal "S6Hist" MemoryImplementation.thy + "(HNext rmhist p) .& $(S6 rmhist p) .& (c p)$ .= $(c p) .-> (rmhist@p)$ .= $(rmhist@p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [HNext_def,MClkReply_def,Return_def,c_def,rtrner_def, + S_def,S6_def,Calling_def]) + ]); +bind_thm("S6HistE", action_conjimpE S6Hist); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemClerk.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemClerk.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,71 @@ +(* + File: MemClerk.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Memory clerk specification (ML file) +*) + +val MC_action_defs = + [MClkInit_def RS inteq_reflection] + @ [MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def]; + +val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def]; + +(* The Clerk engages in an action for process p only if there is an outstanding, + unanswered call for that process. +*) + +qed_goal "MClkidle" MemClerk.thy + ".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p" + (fn _ => [ auto_tac (!claset, + !simpset addsimps (MC_action_defs @ [Return_def])) + ]); + +qed_goal "MClkbusy" MemClerk.thy + "$(Calling rcv p) .-> .~ MClkNext send rcv cst p" + (fn _ => [ auto_tac (!claset, + !simpset addsimps (MC_action_defs @ [Call_def])) + ]); + +(* unlifted versions as introduction rules *) + +bind_thm("MClkidleI", action_mp MClkidle); +bind_thm("MClkbusyI", action_mp MClkbusy); + +(* Enabledness of actions *) + +qed_goal "MClkFwd_enabled" MemClerk.thy + "!!p. base_var ==> \ +\ $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA) \ +\ .-> $(Enabled (MClkFwd send rcv cst p))" + (fn _ => [action_simp_tac (!simpset addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def]) + [] [base_enabled,Pair_inject] 1]); + +qed_goal "MClkFwd_ch_enabled" MemClerk.thy + "Enabled (MClkFwd send rcv cst p) s \ +\ ==> Enabled (_) s" + (fn [prem] => [auto_tac (!claset addSIs [prem RS enabled_mono], + !simpset addsimps [angle_def,MClkFwd_def]) + ]); + +qed_goal "MClkReply_change" MemClerk.thy + "MClkReply send rcv cst p .-> _" + (fn _ => [auto_tac (action_css addsimps2 [angle_def,MClkReply_def] + addEs2 [Return_changedE]) + ]); + +qed_goal "MClkReply_enabled" MemClerk.thy + "!!p. base_var ==> \ +\ $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB) \ +\ .-> $(Enabled (_))" + (fn _ => [action_simp_tac (!simpset) [MClkReply_change RSN (2,enabled_mono)] [] 1, + action_simp_tac (!simpset addsimps [MClkReply_def,Return_def,caller_def,rtrner_def]) + [] [base_enabled,Pair_inject] 1 + ]); + +qed_goal "MClkReplyNotRetry" MemClerk.thy + "MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)" + (fn _ => [ auto_tac (!claset, + !simpset addsimps [MClkReply_def,MClkRetry_def]) + ]); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemClerk.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemClerk.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,72 @@ +(* + File: MemClerk.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: MemClerk + Logic Image: TLA + + RPC-Memory example: specification of the memory clerk. +*) + +MemClerk = Memory + RPC + MemClerkParameters + + +types + (* The clerk takes the same arguments as the memory and sends requests to the RPC *) + mClkSndChType = "memChType" + mClkRcvChType = "rpcSndChType" + mClkStType = "(PrIds => mClkState) stfun" + +consts + (* state predicates *) + MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" + + (* actions *) + MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" + MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" + MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" + MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" + + (* temporal *) + MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" + MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" + +rules + MClkInit_def "$(MClkInit rcv cst p) .= + ($(cst@p) .= #clkA .& .~ $(Calling rcv p))" + + MClkFwd_def "MClkFwd send rcv cst p == + $(Calling send p) + .& $(cst@p) .= #clkA + .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ]) + .& (cst@p)$ .= #clkB + .& unchanged (rtrner send @ p)" + + MClkRetry_def "MClkRetry send rcv cst p == + $(cst@p) .= #clkB + .& res[$(rcv@p)] .= #RPCFailure + .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ]) + .& unchanged " + + MClkReply_def "MClkReply send rcv cst p == + .~ $(Calling rcv p) + .& $(cst@p) .= #clkB + .& Return send p (MClkReplyVal[ res[$(rcv@p)] ]) + .& (cst@p)$ .= #clkA + .& unchanged (caller rcv @ p)" + + MClkNext_def "MClkNext send rcv cst p == + MClkFwd send rcv cst p + .| MClkRetry send rcv cst p + .| MClkReply send rcv cst p" + + MClkIPSpec_def "MClkIPSpec send rcv cst p == + Init($(MClkInit rcv cst p)) + .& [][ MClkNext send rcv cst p ]_ + .& WF(MClkFwd send rcv cst p)_ + .& SF(MClkReply send rcv cst p)_" + + MClkISpec_def "MClkISpec send rcv cst == RALL p. MClkIPSpec send rcv cst p" +end + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemClerkParameters.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemClerkParameters.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,11 @@ +(* + File: MemClerkParameters.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Memory clerk parameters (ML file) +*) + +val CP_simps = RP_simps @ mClkState.simps; + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemClerkParameters.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,34 @@ +(* + File: MemClerkParameters.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: MemClerkParameters + Logic Image: TLA + + RPC-Memory example: Parameters of the memory clerk. +*) + +MemClerkParameters = RPCParameters + + +datatype mClkState = clkA | clkB + +types + (* types sent on the clerk's send and receive channels are argument types + of the memory and the RPC, respectively *) + mClkSndArgType = "memArgType" + mClkRcvArgType = "rpcArgType" + +consts + (* translate a memory call to an RPC call *) + MClkRelayArg :: "memArgType => rpcArgType" + (* translate RPC failures to memory failures *) + MClkReplyVal :: "Vals => Vals" + +rules + MClkRelayArg_def "MClkRelayArg marg == Inl (remoteCall, marg)" + MClkReplyVal_def "MClkReplyVal v == + if v = RPCFailure then MemFailure else v" + +end + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/Memory.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/Memory.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,160 @@ +(* + File: Memory.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Memory specification (ML file) +*) + +val RM_action_defs = + (map (fn t => t RS inteq_reflection) + [MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def]) + @ [GoodRead_def, BadRead_def, ReadInner_def, Read_def, + GoodWrite_def, BadWrite_def, WriteInner_def, Write_def, + MemReturn_def, RNext_def]; + +val UM_action_defs = RM_action_defs @ [MemFail_def, UNext_def]; + +val RM_temp_defs = [RPSpec_def, MSpec_def, IRSpec_def]; +val UM_temp_defs = [UPSpec_def, MSpec_def, IUSpec_def]; + +(* Make sure the simpset accepts non-boolean simplifications *) +simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift); + +(* -------------------- Proofs -------------------------------------------------- *) + +(* The reliable memory is an implementation of the unreliable one *) +qed_goal "ReliableImplementsUnReliable" Memory.thy + "IRSpec ch mm rs .-> IUSpec ch mm rs" + (fn _ => [auto_tac (temp_css addsimps2 ([square_def,UNext_def] @ RM_temp_defs @ UM_temp_defs) + addSEs2 [STL4E]) + ]); + +(* The memory spec implies the memory invariant *) +qed_goal "MemoryInvariant" Memory.thy + "(MSpec ch mm rs l) .-> []($(MemInv mm l))" + (fn _ => [ auto_inv_tac (!simpset addsimps RM_temp_defs @ MP_simps @ RM_action_defs) 1 ]); + +(* The invariant is trivial for non-locations *) +qed_goal "NonMemLocInvariant" Memory.thy + ".~ #(MemLoc l) .-> []($MemInv mm l)" + (fn _ => [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT RS tempD]) ]); + +qed_goal "MemoryInvariantAll" Memory.thy + "((RALL l. #(MemLoc l) .-> MSpec ch mm rs l)) .-> (RALL l. []($MemInv mm l))" + (fn _ => [step_tac temp_cs 1, + case_tac "MemLoc l" 1, + auto_tac (temp_css addSEs2 (map temp_mp [MemoryInvariant,NonMemLocInvariant])) + ]); + +(* The memory engages in an action for process p only if there is an unanswered call from p. + We need this only for the reliable memory. +*) + +qed_goal "Memoryidle" Memory.thy + ".~ $(Calling ch p) .-> .~ RNext ch mm rs p" + (fn _ => [ auto_tac (action_css addsimps2 (RM_action_defs @ [Return_def])) ]); + +bind_thm("MemoryidleI", action_mp Memoryidle); +bind_thm("MemoryidleE", action_impE Memoryidle); + + +(* Enabledness conditions *) + +qed_goal "MemReturn_change" Memory.thy + "MemReturn ch rs p .-> _" + (fn _ => [ auto_tac (action_css addsimps2 [MemReturn_def,angle_def]) ]); + +qed_goal "MemReturn_enabled" Memory.thy + "!!p. base_var ==> \ +\ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \ +\ .-> $(Enabled (_))" + (fn _ => [action_simp_tac (!simpset) [MemReturn_change RSN (2,enabled_mono)] [] 1, + action_simp_tac (!simpset addsimps [MemReturn_def,Return_def,rtrner_def]) + [] [base_enabled,Pair_inject] 1 + ]); + +qed_goal "ReadInner_enabled" Memory.thy + "!!p. base_var ==> \ +\ $(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))) \ +\ .-> $(Enabled (ReadInner ch mm rs p l))" + (fn _ => [Action_simp_tac 1, + (* unlift before applying case_tac: case_split_thm expects boolean conclusion *) + case_tac "MemLoc l" 1, + ALLGOALS + (action_simp_tac + (!simpset addsimps [ReadInner_def,GoodRead_def,BadRead_def, + RdRequest_def]) + [] [base_enabled,Pair_inject]) + ]); + +qed_goal "WriteInner_enabled" Memory.thy + "!!p. base_var ==> \ +\ $(Calling ch p) .& (arg[$(ch@p)] .= #(Inr (write,l,v))) \ +\ .-> $(Enabled (WriteInner ch mm rs p l v))" + (fn _ => [Action_simp_tac 1, + case_tac "MemLoc l & MemVal v" 1, + ALLGOALS + (action_simp_tac + (!simpset addsimps [WriteInner_def,GoodWrite_def,BadWrite_def, + WrRequest_def]) + [] [base_enabled,Pair_inject]) + ]); + +qed_goal "ReadResult" Memory.thy + "(Read ch mm rs p) .& (RALL l. $(MemInv mm l)) .-> (rs@p)$ .~= #NotAResult" + (fn _ => [action_simp_tac + (!simpset addsimps (MP_simps + @ [Read_def,ReadInner_def,GoodRead_def, + BadRead_def,MemInv_def])) + [] [] 1, + auto_tac (action_css addsimps2 MP_simps) ]); + +qed_goal "WriteResult" Memory.thy + "(Write ch mm rs p l) .-> (rs@p)$ .~= #NotAResult" + (fn _ => [auto_tac (!claset, + !simpset addsimps (MP_simps @ + [Write_def,WriteInner_def,GoodWrite_def,BadWrite_def])) + ]); + +qed_goal "ReturnNotReadWrite" Memory.thy + "(RALL l. $MemInv mm l) .& (MemReturn ch rs p) \ +\ .-> .~(Read ch mm rs p) .& (RALL l. .~(Write ch mm rs p l))" + (fn _ => [auto_tac + (action_css addsimps2 [MemReturn_def] + addSEs2 [action_impE WriteResult,action_conjimpE ReadResult]) + ]); + +qed_goal "RWRNext_enabled" Memory.thy + "($(rs@p) .= #NotAResult) .& (RALL l. $(MemInv mm l)) \ +\ .& $(Enabled (Read ch mm rs p .| (REX l. Write ch mm rs p l))) \ +\ .-> $(Enabled (_))" + (fn _ => [auto_tac + (action_css addsimps2 [RNext_def,angle_def] + addSEs2 [enabled_mono2] + addEs2 [action_conjimpE ReadResult,action_impE WriteResult]) + ]); + + +(* Combine previous lemmas: the memory can make a visible step if there is an + outstanding call for which no result has been produced. +*) +qed_goal "RNext_enabled" Memory.thy + "!!p. (ALL l. base_var ) ==> \ +\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \ +\ .-> $(Enabled (_))" + (fn _ => [auto_tac (action_css addsimps2 [enabled_disj] + addSIs2 [action_mp RWRNext_enabled]), + res_inst_tac [("s","arg(ch s p)")] sumE 1, + action_simp_tac (!simpset addsimps [Read_def,enabled_ex,base_pair]) + [action_mp ReadInner_enabled,exI] [] 1, + split_all_tac 1, Rd.induct_tac "xa" 1, + (* introduce a trivial subgoal to solve flex-flex constraint?! *) + subgoal_tac "y = snd(xa,y)" 1, + TRYALL Simp_tac, (* solves "read" case *) + etac swap 1, + action_simp_tac (!simpset addsimps [Write_def,enabled_ex,base_pair]) + [action_mp WriteInner_enabled,exI] [] 1, + split_all_tac 1, Wr.induct_tac "x" 1, + subgoal_tac "(xa = fst(snd(x,xa,y))) & (y = snd(snd(x,xa,y)))" 1, + ALLGOALS Simp_tac ]); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/Memory.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/Memory.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,137 @@ +(* + File: Memory.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Memory + Logic Image: TLA + + RPC-Memory example: Memory specification +*) + +Memory = MemoryParameters + ProcedureInterface + + +types + memChType = "(memArgType,Vals) channel" + memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) + resType = "(PrIds => Vals) stfun" + +consts + (* state predicates *) + MInit :: "memType => Locs => stpred" + PInit :: "resType => PrIds => stpred" + (* auxiliary predicates: is there a pending read/write request for + some process id and location/value? *) + RdRequest :: "memChType => PrIds => Locs => stpred" + WrRequest :: "memChType => PrIds => Locs => Vals => stpred" + + (* actions *) + GoodRead :: "memType => resType => PrIds => Locs => action" + BadRead :: "memType => resType => PrIds => Locs => action" + ReadInner :: "memChType => memType => resType => PrIds => Locs => action" + Read :: "memChType => memType => resType => PrIds => action" + GoodWrite :: "memType => resType => PrIds => Locs => Vals => action" + BadWrite :: "memType => resType => PrIds => Locs => Vals => action" + WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action" + Write :: "memChType => memType => resType => PrIds => Locs => action" + MemReturn :: "memChType => resType => PrIds => action" + MemFail :: "memChType => resType => PrIds => action" + RNext :: "memChType => memType => resType => PrIds => action" + UNext :: "memChType => memType => resType => PrIds => action" + + (* temporal formulas *) + RPSpec :: "memChType => memType => resType => PrIds => temporal" + UPSpec :: "memChType => memType => resType => PrIds => temporal" + MSpec :: "memChType => memType => resType => Locs => temporal" + IRSpec :: "memChType => memType => resType => temporal" + IUSpec :: "memChType => memType => resType => temporal" + + RSpec :: "memChType => resType => temporal" + USpec :: "memChType => temporal" + + (* memory invariant: in the paper, the invariant is hidden in the definition of + the predicate S used in the implementation proof, but it is easier to verify + at this level. *) + MemInv :: "memType => Locs => stpred" + +rules + MInit_def "$(MInit mm l) .= ($(mm@l) .= # InitVal)" + PInit_def "$(PInit rs p) .= ($(rs@p) .= # NotAResult)" + + RdRequest_def "$(RdRequest ch p l) .= + ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))))" + WrRequest_def "$(WrRequest ch p l v) .= + ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inr (write,l,v))))" + (* a read that doesn't raise BadArg *) + GoodRead_def "GoodRead mm rs p l == + #(MemLoc l) .& (rs@p)$ .= $(mm@l)" + (* a read that raises BadArg *) + BadRead_def "BadRead mm rs p l == + .~ #(MemLoc l) .& (rs@p)$ .= #BadArg" + (* the read action with l visible *) + ReadInner_def "ReadInner ch mm rs p l == + $(RdRequest ch p l) + .& (GoodRead mm rs p l .| BadRead mm rs p l) + .& unchanged (rtrner ch @ p)" + (* the read action with l quantified *) + Read_def "Read ch mm rs p == REX l. ReadInner ch mm rs p l" + + (* similar definitions for the write action *) + GoodWrite_def "GoodWrite mm rs p l v == + #(MemLoc l) .& #(MemVal v) + .& (mm@l)$ .= #v .& (rs@p)$ .= #OK" + BadWrite_def "BadWrite mm rs p l v == + .~ (#(MemLoc l) .& #(MemVal v)) + .& (rs@p)$ .= #BadArg .& unchanged (mm@l)" + WriteInner_def "WriteInner ch mm rs p l v == + $(WrRequest ch p l v) + .& (GoodWrite mm rs p l v .| BadWrite mm rs p l v) + .& unchanged (rtrner ch @ p)" + Write_def "Write ch mm rs p l == REX v. WriteInner ch mm rs p l v" + + (* the return action *) + MemReturn_def "MemReturn ch rs p == + $(rs@p) .~= #NotAResult + .& (rs@p)$ .= #NotAResult + .& Return ch p ($(rs@p))" + (* the failure action of the unreliable memory *) + MemFail_def "MemFail ch rs p == + $(Calling ch p) + .& (rs@p)$ .= #MemFailure + .& unchanged (rtrner ch @ p)" + RNext_def "RNext ch mm rs p == + Read ch mm rs p + .| (REX l. Write ch mm rs p l) + .| MemReturn ch rs p" + UNext_def "UNext ch mm rs p == + RNext ch mm rs p .| MemFail ch rs p" + + RPSpec_def "RPSpec ch mm rs p == + Init($(PInit rs p)) + .& [][ RNext ch mm rs p ]_ + .& WF(RNext ch mm rs p)_ + .& WF(MemReturn ch rs p)_" + UPSpec_def "UPSpec ch mm rs p == + Init($(PInit rs p)) + .& [][ UNext ch mm rs p ]_ + .& WF(RNext ch mm rs p)_ + .& WF(MemReturn ch rs p)_" + MSpec_def "MSpec ch mm rs l == + Init($(MInit mm l)) + .& [][ REX p. Write ch mm rs p l ]_(mm@l)" + IRSpec_def "IRSpec ch mm rs == + (RALL p. RPSpec ch mm rs p) + .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)" + IUSpec_def "IUSpec ch mm rs == + (RALL p. UPSpec ch mm rs p) + .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)" + + RSpec_def "RSpec ch rs == EEX mm. IRSpec ch mm rs" + USpec_def "USpec ch == EEX mm rs. IUSpec ch mm rs" + + MemInv_def "$(MemInv mm l) .= + (#(MemLoc l) .-> MemVal[ $(mm@l)])" +end + + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemoryImplementation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,672 @@ +(* + File: MemoryImplementation.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: Memory implementation (ML file) + + The main theorem is theorem "Implementation" at the end of this file, + which shows that the composition of a reliable memory, an RPC component, and + a memory clerk implements an unreliable memory. The files "MIsafe.ML" and + "MIlive.ML" contain lower-level lemmas for the safety and liveness parts. + + Steps are (roughly) numbered as in the hand proof. +*) + + +(* ------------------------------ HOL lemmas ------------------------------ *) +(* Add the following simple lemmas as default simplification rules. *) + +section "Auxiliary lemmas"; + +qed_goal "equal_false_not" HOL.thy "(P = False) = (~P)" + (fn _ => [fast_tac prop_cs 1]); + +Addsimps [equal_false_not]; + + +(* A variant of the implication elimination rule that keeps the antecedent. + Use "thm RS impdupE" to generate an unsafe (looping) elimination rule. +*) + +qed_goal "impdupE" HOL.thy + "[| P --> Q; P; [| P;Q |] ==> R |] ==> R" + (fn maj::prems => [REPEAT (resolve_tac ([maj RS mp] @ prems) 1)]); + + +(* Introduction/elimination rules for if-then-else *) + +qed_goal "ifI" HOL.thy + "[| Q ==> P(x); ~Q ==> P(y) |] ==> P(if Q then x else y)" + (fn prems => [case_tac "Q" 1, ALLGOALS (Asm_simp_tac THEN' (eresolve_tac prems))]); + +qed_goal "ifE" HOL.thy + "[| P(if Q then x else y); [| Q; P(x) |] ==> R; [| ~Q; P(y) |] ==> R |] ==> R" + (fn (prem1::prems) => [case_tac "Q" 1, + ALLGOALS ((cut_facts_tac [prem1]) + THEN' Asm_full_simp_tac + THEN' (REPEAT o ((eresolve_tac prems) ORELSE' atac))) + ]); + +(* --------------------------- automatic prover --------------------------- *) +(* Set up a clasimpset that contains data-level simplifications. *) + +val MI_css = temp_css addsimps2 (CP_simps @ histState.simps + @ [slice_def,equal_false_not,if_cancel,sum_case_Inl, sum_case_Inr]); + +(* A more aggressive variant that tries to solve subgoals by assumption + or contradiction during the simplification. + THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!! + (but sometimes a lot faster than MI_css) +*) +val MI_fast_css = + let + val (cs,ss) = MI_css + in + (cs, ss addSSolver (fn thms => assume_tac ORELSE' (etac notE))) +end; + +(* Make sure the simpset accepts non-boolean simplifications *) +simpset := let val (_,ss) = MI_css in ss end; + + +(****************************** The history variable ******************************) +section "History variable"; + +qed_goal "HistoryLemma" MemoryImplementation.thy + "Init(RALL p. $(ImpInit p)) .& [](RALL p. ImpNext p) \ +\ .-> (EEX rmhist. Init(RALL p. $(HInit rmhist p)) \ +\ .& [](RALL p. [HNext rmhist p]_))" + (fn _ => [Auto_tac(), + rtac historyI 1, TRYALL atac, + action_simp_tac (!simpset addsimps [HInit_def]) [] [] 1, + res_inst_tac [("x","p")] fun_cong 1, atac 1, + action_simp_tac (!simpset addsimps [HNext_def]) [busy_squareI] [] 1, + res_inst_tac [("x","p")] fun_cong 1, atac 1 + ]); + +qed_goal "History" MemoryImplementation.thy + "Implementation .-> (EEX rmhist. Hist rmhist)" + (fn _ => [Auto_tac(), + rtac ((temp_mp HistoryLemma) RS eex_mono) 1, + SELECT_GOAL + (auto_tac (MI_css + addsimps2 [Impl_def,MClkISpec_def,RPCISpec_def,IRSpec_def, + MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, + ImpInit_def,Init_def,ImpNext_def, + c_def,r_def,m_def,all_box,split_box_conj])) 1, + auto_tac (MI_css + addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) + ]); + +(******************************** The safety part *********************************) + +section "The safety part"; + +(* ------------------------- Include lower-level lemmas ------------------------- *) +use "MIsafe.ML"; + +section "Correctness of predicate-action diagram"; + +(* ========== Step 1.1 ================================================= *) +(* The implementation's initial condition implies the state predicate S1 *) + +qed_goal "Step1_1" MemoryImplementation.thy + "$(ImpInit p) .& $(HInit rmhist p) .-> $(S1 rmhist p)" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def, + HInit_def,ImpInit_def,S_def,S1_def]) + ]); + +(* ========== Step 1.2 ================================================== *) +(* Figure 16 is a predicate-action diagram for the implementation. *) + +qed_goal "Step1_2_1" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged .& $(S1 rmhist p) \ +\ .-> (S2 rmhist p)$ .& (ENext p) .& unchanged " + (fn _ => [auto_tac (MI_css addsimps2 [ImpNext_def] + addSEs2 [S1ClerkUnchE,S1RPCUnchE,S1MemUnchE,S1HistE]), + ALLGOALS (action_simp_tac (!simpset addsimps [square_def]) [] [S1EnvE]) + ]); + +qed_goal "Step1_2_2" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged .& $(S2 rmhist p) \ +\ .-> (S3 rmhist p)$ .& (MClkFwd memCh crCh cst p) .& unchanged " + (fn _ => [auto_tac (MI_css addsimps2 [ImpNext_def] + addSEs2 [S2EnvUnchE,S2RPCUnchE,S2MemUnchE,S2HistE]), + ALLGOALS (action_simp_tac (!simpset addsimps [square_def]) [] [S2ClerkE,S2ForwardE]) + ]); + +qed_goal "Step1_2_3" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged .& $(S3 rmhist p) \ +\ .-> ((S4 rmhist p)$ .& RPCFwd crCh rmCh rst p .& unchanged ) \ +\ .| ((S6 rmhist p)$ .& RPCFail crCh rmCh rst p .& unchanged )" + (fn _ => [action_simp_tac (!simpset addsimps [ImpNext_def]) + [] [S3EnvUnchE,S3ClerkUnchE,S3MemUnchE] 1, + ALLGOALS (action_simp_tac (!simpset addsimps [square_def]) + [] [S3RPCE,S3ForwardE,S3FailE]), + auto_tac (MI_css addEs2 [S3HistE]) + ]); + +qed_goal "Step1_2_4" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged \ +\ .& $(S4 rmhist p) .& (RALL l. $(MemInv mem l)) \ +\ .-> ((S4 rmhist p)$ .& Read rmCh mem ires p .& unchanged ) \ +\ .| ((S4 rmhist p)$ .& (REX l. Write rmCh mem ires p l) .& unchanged ) \ +\ .| ((S5 rmhist p)$ .& MemReturn rmCh ires p .& unchanged )" + (fn _ => [action_simp_tac (!simpset addsimps [ImpNext_def]) + [] [S4EnvUnchE,S4ClerkUnchE,S4RPCUnchE] 1, + ALLGOALS (action_simp_tac (!simpset addsimps [square_def,RNext_def]) + [] [S4ReadE,S4WriteE,S4ReturnE]), + auto_tac (MI_css addEs2 [S4HistE]) + ]); + +qed_goal "Step1_2_5" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged .& $(S5 rmhist p) \ +\ .-> ((S6 rmhist p)$ .& RPCReply crCh rmCh rst p .& unchanged ) \ +\ .| ((S6 rmhist p)$ .& RPCFail crCh rmCh rst p .& unchanged )" + (fn _ => [action_simp_tac (!simpset addsimps [ImpNext_def]) + [] [S5EnvUnchE,S5ClerkUnchE,S5MemUnchE,S5HistE] 1, + action_simp_tac (!simpset addsimps [square_def]) [] [S5RPCE] 1, + auto_tac (MI_fast_css addSEs2 [S5ReplyE,S5FailE]) + ]); + +qed_goal "Step1_2_6" MemoryImplementation.thy + "[HNext rmhist p]_ .& ImpNext p \ +\ .& .~ unchanged .& $(S6 rmhist p) \ +\ .-> ((S1 rmhist p)$ .& (MClkReply memCh crCh cst p) .& unchanged )\ +\ .| ((S3 rmhist p)$ .& (MClkRetry memCh crCh cst p) .& unchanged )" + (fn _ => [action_simp_tac (!simpset addsimps [ImpNext_def]) + [] [S6EnvUnchE,S6RPCUnchE,S6MemUnchE] 1, + ALLGOALS (action_simp_tac (!simpset addsimps [square_def]) + [] [S6ClerkE,S6RetryE,S6ReplyE]), + auto_tac (MI_css addEs2 [S6HistE]) + ]); + + +(* -------------------------------------------------------------------------- + Step 1.3: S1 implies the barred initial condition. +*) + +section "Initialization (Step 1.3)"; + +val resbar_unl = rewrite_rule [slice_def] (action_unlift resbar_def); + +qed_goal "Step1_3" MemoryImplementation.thy + "$(S1 rmhist p) .-> $(PInit (resbar rmhist) p)" + (fn _ => [action_simp_tac (!simpset addsimps [resbar_unl,PInit_def,S_def,S1_def]) + [] [] 1 + ]); + +(* ---------------------------------------------------------------------- + Step 1.4: Implementation's next-state relation simulates specification's + next-state relation (with appropriate substitutions) +*) + +section "Step simulation (Step 1.4)"; + +qed_goal "Step1_4_1" MemoryImplementation.thy + "ENext p .& $(S1 rmhist p) .& (S2 rmhist p)$ .& unchanged \ +\ .-> unchanged " + (fn _ => [ auto_tac (MI_fast_css addsimps2 [c_def,r_def,m_def,resbar_unl]) ]); + +qed_goal "Step1_4_2" MemoryImplementation.thy + "MClkFwd memCh crCh cst p .& $(S2 rmhist p) .& (S3 rmhist p)$ \ +\ .& unchanged \ +\ .-> unchanged " + (fn _ => [auto_tac (MI_fast_css + addsimps2 [MClkFwd_def, e_def, r_def, m_def, resbar_unl, + S_def, S2_def, S3_def]) + ]); + +qed_goal "Step1_4_3a" MemoryImplementation.thy + "RPCFwd crCh rmCh rst p .& $(S3 rmhist p) .& (S4 rmhist p)$ \ +\ .& unchanged \ +\ .-> unchanged " + (fn _ => [auto_tac (MI_fast_css addsimps2 [e_def,c_def,m_def,resbar_unl]), + (* NB: Adding S3_exclE,S4_exclE as safe elims above would loop, + adding them as unsafe elims doesn't help, + because auto_tac doesn't find the proof! *) + REPEAT (eresolve_tac [S3_exclE,S4_exclE] 1), + action_simp_tac (!simpset addsimps [S_def, S3_def]) [] [] 1 + ]); + +qed_goal "Step1_4_3b" MemoryImplementation.thy + "RPCFail crCh rmCh rst p .& $(S3 rmhist p) .& (S6 rmhist p)$ .& unchanged \ +\ .-> MemFail memCh (resbar rmhist) p" + (fn _ => [auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def, + resbar_unl]), + (* It's faster not to expand S3 at once *) + action_simp_tac (!simpset addsimps [S3_def,S_def]) [] [] 1, + etac S6_exclE 1, + auto_tac (MI_fast_css addsimps2 [Return_def]) + ]); + + +qed_goal "Step1_4_4a1" MemoryImplementation.thy + "$(S4 rmhist p) .& (S4 rmhist p)$ .& ReadInner rmCh mem ires p l \ +\ .& unchanged .& $(MemInv mem l) \ +\ .-> ReadInner memCh mem (resbar rmhist) p l" + (fn _ => [action_simp_tac + (!simpset addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def]) + [] [] 1, + ALLGOALS (REPEAT o (etac S4_exclE)), + auto_tac (MI_css addsimps2 [resbar_unl]), + ALLGOALS (action_simp_tac + (!simpset addsimps [RPCRelayArg_def,MClkRelayArg_def, + S_def,S4_def,RdRequest_def,MemInv_def]) + [] [impE,MemValNotAResultE]) + ]); + +qed_goal "Step1_4_4a" MemoryImplementation.thy + "Read rmCh mem ires p .& $(S4 rmhist p) .& (S4 rmhist p)$ \ +\ .& unchanged .& (RALL l. $(MemInv mem l)) \ +\ .-> Read memCh mem (resbar rmhist) p" + (fn _ => [ auto_tac (MI_css addsimps2 [Read_def] addSIs2 [action_mp Step1_4_4a1]) ]); + +qed_goal "Step1_4_4b1" MemoryImplementation.thy + "$(S4 rmhist p) .& (S4 rmhist p)$ .& WriteInner rmCh mem ires p l v \ +\ .& unchanged \ +\ .-> WriteInner memCh mem (resbar rmhist) p l v" + (fn _ => [action_simp_tac + (!simpset addsimps [WriteInner_def, GoodWrite_def, BadWrite_def, + e_def, c_def, m_def]) + [] [] 1, + ALLGOALS (REPEAT o (etac S4_exclE)), + auto_tac (MI_css addsimps2 [resbar_unl]), + (* it's faster not to merge the two simplifications *) + ALLGOALS (action_simp_tac + (!simpset addsimps [RPCRelayArg_def,MClkRelayArg_def, + S_def,S4_def,WrRequest_def]) + [] []) + ]); + +qed_goal "Step1_4_4b" MemoryImplementation.thy + "Write rmCh mem ires p l .& $(S4 rmhist p) .& (S4 rmhist p)$ \ +\ .& unchanged \ +\ .-> Write memCh mem (resbar rmhist) p l" + (fn _ => [ auto_tac (MI_css addsimps2 [Write_def] addSIs2 [action_mp Step1_4_4b1]) ]); + +qed_goal "Step1_4_4c" MemoryImplementation.thy + "MemReturn rmCh ires p .& $(S4 rmhist p) .& (S5 rmhist p)$ .& unchanged \ +\ .-> unchanged " + (fn _ => [action_simp_tac + (!simpset addsimps [e_def,c_def,r_def,resbar_unl]) [] [] 1, + REPEAT (eresolve_tac [S4_exclE,S5_exclE] 1), + auto_tac (MI_fast_css addsimps2 [MemReturn_def,Return_def]) + ]); + +qed_goal "Step1_4_5a" MemoryImplementation.thy + "RPCReply crCh rmCh rst p .& $(S5 rmhist p) .& (S6 rmhist p)$ .& unchanged \ +\ .-> unchanged " + (fn _ => [auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_unl]), + REPEAT (eresolve_tac [S5_exclE,S6_exclE] 1), + auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def] + addSEs2 [MVOKBAnotRFE]) + ]); + +qed_goal "Step1_4_5b" MemoryImplementation.thy + "RPCFail crCh rmCh rst p .& $(S5 rmhist p) .& (S6 rmhist p)$ .& unchanged \ +\ .-> MemFail memCh (resbar rmhist) p" + (fn _ => [action_simp_tac + (!simpset addsimps [e_def, c_def, m_def, RPCFail_def, Return_def, + MemFail_def, resbar_unl]) + [] [] 1, + action_simp_tac (!simpset addsimps [S5_def,S_def]) [] [] 1, + etac S6_exclE 1, + auto_tac MI_css + ]); + +qed_goal "Step1_4_6a" MemoryImplementation.thy + "MClkReply memCh crCh cst p .& $(S6 rmhist p) .& (S1 rmhist p)$ .& unchanged \ +\ .-> MemReturn memCh (resbar rmhist) p" + (fn _ => [action_simp_tac + (!simpset addsimps [e_def, r_def, m_def, MClkReply_def, MemReturn_def, + Return_def, resbar_unl]) + [] [] 1, + ALLGOALS (etac S6_exclE), + ALLGOALS Asm_full_simp_tac, (* simplify if-then-else *) + ALLGOALS (action_simp_tac + (!simpset addsimps [MClkReplyVal_def,S6_def,S_def]) + [] []), + rtac ifI 1, + ALLGOALS (action_simp_tac (!simpset) [] [MVOKBARFnotNRE]) + ]); + +qed_goal "Step1_4_6b" MemoryImplementation.thy + "MClkRetry memCh crCh cst p .& $(S6 rmhist p) .& (S3 rmhist p)$ \ +\ .& unchanged \ +\ .-> MemFail memCh (resbar rmhist) p" + (fn _ => [action_simp_tac + (!simpset addsimps [e_def, r_def, m_def, MClkRetry_def, MemFail_def, resbar_unl]) + [] [] 1, + SELECT_GOAL (auto_tac (MI_css addsimps2 [S6_def,S_def])) 1, + etac S3_exclE 1, + Asm_full_simp_tac 1, + action_simp_tac (!simpset addsimps [S6_def,S3_def,S_def]) [] [] 1 + ]); + +qed_goal "S_lemma" MemoryImplementation.thy + "unchanged \ +\ .-> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)" + (fn _ => [auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def, + S_def,Calling_def]) + ]); + +qed_goal "Step1_4_7H" MemoryImplementation.thy + "unchanged \ +\ .-> unchanged " + (fn _ => [Action_simp_tac 1, + SELECT_GOAL (auto_tac (MI_fast_css addsimps2 [c_def])) 1, + ALLGOALS (simp_tac (!simpset + addsimps [S1_def,S2_def,S3_def,S4_def,S5_def,S6_def])), + auto_tac (MI_css addSIs2 [action_mp S_lemma]) + ]); + +(* unlifted version as elimination rule *) +bind_thm("Step1_4_7h", + (rewrite_rule action_rews (Step1_4_7H RS actionD)) RS impdupE); + +qed_goal "Step1_4_7" MemoryImplementation.thy + "unchanged .-> unchanged " + (fn _ => [rtac actionI 1, + rewrite_goals_tac action_rews, + rtac impI 1, + etac Step1_4_7h 1, + auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,rtrner_def,resbar_unl]) + ]); + + +(* Frequently needed abbreviation: distinguish between idling and non-idling + steps of the implementation, and try to solve the idling case by simplification +*) +fun split_idle_tac simps i = + EVERY [rtac actionI i, + case_tac "(unchanged ) [[s,t]]" i, + rewrite_goals_tac action_rews, + etac Step1_4_7h i, + asm_full_simp_tac (!simpset addsimps simps) i + ]; + +(* ---------------------------------------------------------------------- + Combine steps 1.2 and 1.4 to prove that the implementation satisfies + the specification's next-state relation. +*) + +(* Steps that leave all variables unchanged are safe, so I may assume + that some variable changes in the proof that a step is safe. *) +qed_goal "unchanged_safe" MemoryImplementation.thy + "(.~ (unchanged ) \ +\ .-> [UNext memCh mem (resbar rmhist) p]_) \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [rtac actionI 1, + case_tac "(unchanged ) [[s,t]]" 1, + rewrite_goals_tac action_rews, + auto_tac (MI_css addsimps2 [square_def] addSEs2 [action_impE Step1_4_7]) + ]); +(* turn into (unsafe, looping!) introduction rule *) +bind_thm("unchanged_safeI", impI RS (action_mp unchanged_safe)); + +qed_goal "S1safe" MemoryImplementation.thy + "$(S1 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + rtac idle_squareI 1, + auto_tac (MI_css addSEs2 (map action_conjimpE [Step1_2_1,Step1_4_1])) + ]); + +qed_goal "S2safe" MemoryImplementation.thy + "$(S2 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + rtac idle_squareI 1, + auto_tac (MI_fast_css addSEs2 (map action_conjimpE [Step1_2_2,Step1_4_2])) + ]); + +qed_goal "S3safe" MemoryImplementation.thy + "$(S3 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_3]), + auto_tac (MI_fast_css addsimps2 [square_def,UNext_def] + addSEs2 (map action_conjimpE [Step1_4_3a,Step1_4_3b])) + ]); + +qed_goal "S4safe" MemoryImplementation.thy + "$(S4 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .& (RALL l. $(MemInv mem l)) \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_4]), + ALLGOALS (action_simp_tac (!simpset addsimps [square_def,UNext_def,RNext_def]) [] []), + auto_tac (MI_fast_css addSEs2 (map action_conjimpE + [Step1_4_4a,Step1_4_4b,Step1_4_4c])) + ]); + +qed_goal "S5safe" MemoryImplementation.thy + "$(S5 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_5]), + auto_tac (MI_fast_css addsimps2 [square_def,UNext_def] + addSEs2 (map action_conjimpE [Step1_4_5a,Step1_4_5b])) + ]); + +qed_goal "S6safe" MemoryImplementation.thy + "$(S6 rmhist p) .& ImpNext p .& [HNext rmhist p]_ \ +\ .-> [UNext memCh mem (resbar rmhist) p]_" + (fn _ => [Action_simp_tac 1, + rtac unchanged_safeI 1, + auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_6]), + auto_tac (MI_fast_css addsimps2 [square_def,UNext_def,RNext_def] + addSEs2 (map action_conjimpE [Step1_4_6a,Step1_4_6b])) + ]); + +(* ---------------------------------------------------------------------- + Step 1.5: Temporal refinement proof, based on previous steps. +*) + +section "The liveness part"; + +use "MIlive.ML"; + +section "Refinement proof (step 1.5)"; + +(* Prove invariants of the implementation: + a. memory invariant + b. "implementation invariant": always in states S1,...,S6 +*) +qed_goal "Step1_5_1a" MemoryImplementation.thy + "IPImp p .-> (RALL l. []$(MemInv mem l))" + (fn _ => [auto_tac (MI_css addsimps2 [IPImp_def] + addSIs2 [temp_mp MemoryInvariantAll]) + ]); +bind_thm("MemInvI", (rewrite_rule intensional_rews (Step1_5_1a RS tempD)) RS impdupE); + +qed_goal "Step1_5_1b" MemoryImplementation.thy + " Init($(ImpInit p) .& $(HInit rmhist p)) .& [](ImpNext p) \ +\ .& [][HNext rmhist p]_ .& [](RALL l. $(MemInv mem l)) \ +\ .-> []($(ImpInv rmhist p))" + (fn _ => [inv_tac MI_css 1, + auto_tac (MI_css + addsimps2 [Init_def, ImpInv_def] + addSEs2 [action_impE Step1_1] + addEs2 (map action_conjimpE + [S1_successors,S2_successors,S3_successors, + S4_successors,S5_successors,S6_successors])) + ]); +bind_thm("ImpInvI", (rewrite_rule intensional_rews (Step1_5_1b RS tempD)) RS impdupE); + +(*** Initialization ***) +qed_goal "Step1_5_2a" MemoryImplementation.thy + "Init($(ImpInit p) .& $(HInit rmhist p)) .-> Init($PInit (resbar rmhist) p)" + (fn _ => [auto_tac (MI_css addsimps2 [Init_def] + addSIs2 (map action_mp [Step1_1,Step1_3])) + ]); + +(*** step simulation ***) +qed_goal "Step1_5_2b" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_ \ +\ .& $(ImpInv rmhist p) .& (RALL l. $(MemInv mem l))) \ +\ .-> [][UNext memCh mem (resbar rmhist) p]_" + (fn _ => [auto_tac (MI_fast_css + addsimps2 [ImpInv_def] + addSEs2 (STL4E::(map action_conjimpE + [S1safe,S2safe,S3safe,S4safe,S5safe,S6safe]))) + ]); + + +(*** Liveness ***) +qed_goal "GoodImpl" MemoryImplementation.thy + "IPImp p .& HistP rmhist p \ +\ .-> Init($(ImpInit p) .& $(HInit rmhist p)) \ +\ .& [](ImpNext p .& [HNext rmhist p]_) \ +\ .& [](RALL l. $(MemInv mem l)) .& []($(ImpInv rmhist p)) \ +\ .& ImpLive p" + (fn _ => [(* need some subgoals to prove [](ImpInv p), avoid duplication *) + rtac tempI 1, rewrite_goals_tac intensional_rews, rtac impI 1, + subgoal_tac + "sigma |= Init($(ImpInit p) .& $(HInit rmhist p)) \ +\ .& [](ImpNext p) \ +\ .& [][HNext rmhist p]_ \ +\ .& [](RALL l. $(MemInv mem l))" 1, + auto_tac (MI_css addsimps2 [split_box_conj] + addSEs2 [temp_conjimpE Step1_5_1b]), + SELECT_GOAL + (auto_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, + ImpLive_def,c_def,r_def,m_def])) 1, + SELECT_GOAL + (auto_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, + HistP_def,Init_def,action_unlift ImpInit_def])) 1, + SELECT_GOAL + (auto_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, + ImpNext_def,c_def,r_def,m_def, + split_box_conj])) 1, + SELECT_GOAL (auto_tac (MI_css addsimps2 [HistP_def])) 1, + etac ((temp_mp Step1_5_1a) RS ((temp_unlift allT) RS iffD1)) 1 + ]); + +(* The implementation is infinitely often in state S1 *) +qed_goal "Step1_5_3a" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) \ +\ .& [](RALL l. $(MemInv mem l)) \ +\ .& []($(ImpInv rmhist p)) .& ImpLive p \ +\ .-> []<>($(S1 rmhist p))" + (fn _ => [auto_tac (MI_css addsimps2 [ImpLive_def]), + rtac S1Infinite 1, + SELECT_GOAL + (auto_tac (MI_css + addsimps2 [split_box_conj] + addSIs2 (NotS1LeadstoS6:: + map temp_mp [S2_live,S3_live,S4a_live,S4b_live,S5_live]))) 1, + auto_tac (MI_css addsimps2 [split_box_conj] addSIs2 [temp_mp S6_live]) + ]); + +(* Hence, it satisfies the fairness requirements of the specification *) +qed_goal "Step1_5_3b" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) \ +\ .& [](RALL l. $(MemInv mem l)) .& []($(ImpInv rmhist p)) .& ImpLive p \ +\ .-> WF(RNext memCh mem (resbar rmhist) p)_" + (fn _ => [ auto_tac (MI_fast_css addSIs2 [RNext_fair,temp_mp Step1_5_3a]) ]); + +qed_goal "Step1_5_3c" MemoryImplementation.thy + "[](ImpNext p .& [HNext rmhist p]_) \ +\ .& [](RALL l. $(MemInv mem l)) .& []($(ImpInv rmhist p)) .& ImpLive p \ +\ .-> WF(MemReturn memCh (resbar rmhist) p)_" + (fn _ => [ auto_tac (MI_fast_css addSIs2 [Return_fair,temp_mp Step1_5_3a]) ]); + + +(* QED step of step 1 *) +qed_goal "Step1" MemoryImplementation.thy + "IPImp p .& HistP rmhist p .-> UPSpec memCh mem (resbar rmhist) p" + (fn _ => [auto_tac + (MI_css addsimps2 [UPSpec_def,split_box_conj] + addSEs2 [temp_impE GoodImpl] + addSIs2 (map temp_mp [Step1_5_2a,Step1_5_2b, + Step1_5_3b,Step1_5_3c])) + ]); + + +(* ------------------------------ Step 2 ------------------------------ *) +section "Step 2"; + +qed_goal "Step2_2a" MemoryImplementation.thy + "ImpNext p .& [HNext rmhist p]_ \ +\ .& $(S4 rmhist p) .& Write rmCh mem ires p l \ +\ .-> (S4 rmhist p)$ .& unchanged " + (fn _ => [split_idle_tac [] 1, + action_simp_tac (!simpset addsimps [ImpNext_def]) + [] [S4EnvUnchE,S4ClerkUnchE,S4RPCUnchE] 1, + TRYALL (action_simp_tac (!simpset addsimps [square_def]) [] [S4WriteE]), + Auto_tac() + ]); + +qed_goal "Step2_2" MemoryImplementation.thy + " (RALL p. ImpNext p) \ +\ .& (RALL p. [HNext rmhist p]_) \ +\ .& (RALL p. $(ImpInv rmhist p)) \ +\ .& [REX q. Write rmCh mem ires q l]_(mem@l) \ +\ .-> [REX q. Write memCh mem (resbar rmhist) q l]_(mem@l)" + (fn _ => [auto_tac (MI_css addsimps2 [square_def] + addSIs2 [action_mp Step1_4_4b] + addSEs2 [WriteS4E, action_conjimpE Step2_2a]) + ]); + +qed_goal "Step2_lemma" MemoryImplementation.thy + " []( (RALL p. ImpNext p) \ +\ .& (RALL p. [HNext rmhist p]_) \ +\ .& (RALL p. $(ImpInv rmhist p)) \ +\ .& [REX q. Write rmCh mem ires q l]_(mem@l)) \ +\ .-> [][REX q. Write memCh mem (resbar rmhist) q l]_(mem@l)" + (fn _ => [ auto_tac (MI_css addSEs2 [STL4E, action_conjimpE Step2_2]) ]); + +qed_goal "Step2" MemoryImplementation.thy + "#(MemLoc l) .& (RALL p. IPImp p .& HistP rmhist p) \ +\ .-> MSpec memCh mem (resbar rmhist) l" + (fn _ => [auto_tac (MI_css addsimps2 [MSpec_def]), + (* prove initial condition, don't expand IPImp in other subgoal *) + SELECT_GOAL (auto_tac (MI_css addsimps2 [IPImp_def,MSpec_def])) 1, + auto_tac (MI_css addSIs2 [temp_mp Step2_lemma] + addsimps2 [split_box_conj,all_box]), + SELECT_GOAL (auto_tac (MI_css addsimps2 [IPImp_def,MSpec_def])) 4, + auto_tac (MI_css addsimps2 [split_box_conj] + addSEs2 [temp_impE GoodImpl]) + ]); + +(* ----------------------------- Main theorem --------------------------------- *) +section "Memory implementation"; + +(* The combination of a legal caller, the memory clerk, the RPC component, + and a reliable memory implement the unreliable memory. +*) + +(* Implementation of internal specification by combination of implementation + and history variable with explicit refinement mapping +*) +qed_goal "Impl_IUSpec" MemoryImplementation.thy + "Implementation .& Hist rmhist .-> IUSpec memCh mem (resbar rmhist)" + (fn _ => [auto_tac (MI_css addsimps2 [IUSpec_def,Impl_def,IPImp_def,MClkISpec_def, + RPCISpec_def,IRSpec_def,Hist_def] + addSIs2 (map temp_mp [Step1,Step2])) + ]); + +(* The main theorem: introduce hiding and eliminate history variable. *) +qed_goal "Implementation" MemoryImplementation.thy + "Implementation .-> USpec memCh" + (fn _ => [Auto_tac(), + forward_tac [temp_mp History] 1, + auto_tac (MI_css addsimps2 [USpec_def] + addIs2 (map temp_mp [eexI, Impl_IUSpec]) + addSEs2 [eexE]) + ]); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemoryImplementation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,188 @@ +(* + File: MemoryImplementation.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: MemoryImplementation + Logic Image: TLA + + RPC-Memory example: Memory implementation +*) + +MemoryImplementation = Memory + RPC + MemClerk + MIParameters + + +types + histType = "(PrIds => histState) stfun" (* the type of the history variable *) + +consts + (* the specification *) + (* channel (external) *) + memCh :: "memChType" + (* internal variables *) + mem :: "memType" + resbar :: "histType => resType" (* defined by refinement mapping *) + + (* the state variables of the implementation *) + (* channels *) + (* same interface channel memCh *) + crCh :: "rpcSndChType" + rmCh :: "rpcRcvChType" + (* internal variables *) + (* identity refinement mapping for mem -- simply reused *) + rst :: "rpcStType" + cst :: "mClkStType" + ires :: "resType" +(* the history variable : not defined as a constant + rmhist :: "histType" +*) + + (* the environment action *) + ENext :: "PrIds => action" + + (* specification of the history variable *) + HInit :: "histType => PrIds => stpred" + HNext :: "histType => PrIds => action" + HistP :: "histType => PrIds => temporal" + Hist :: "histType => temporal" + + (* the implementation *) + ImpInit :: "PrIds => stpred" + ImpNext :: "PrIds => action" + ImpLive :: "PrIds => temporal" + IPImp :: "PrIds => temporal" + Implementation :: "temporal" + ImpInv :: "histType => PrIds => stpred" + + (* tuples of state functions changed by the various components *) + e :: "PrIds => (bit * memArgType) stfun" + c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcArgType)) stfun" + r :: "PrIds => (rpcState * (bit * Vals) * (bit * memArgType)) stfun" + m :: "PrIds => ((bit * Vals) * Vals) stfun" + + (* the predicate S describes the states of the implementation. + slight simplification: two "histState" parameters instead of a (one- or + two-element) set. *) + S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred" + + (* predicates S1 -- S6 define special instances of S *) + S1 :: "histType => PrIds => stpred" + S2 :: "histType => PrIds => stpred" + S3 :: "histType => PrIds => stpred" + S4 :: "histType => PrIds => stpred" + S5 :: "histType => PrIds => stpred" + S6 :: "histType => PrIds => stpred" + + (* auxiliary predicates *) + MVOKBARF :: "Vals => bool" + MVOKBA :: "Vals => bool" + MVNROKBA :: "Vals => bool" + +rules + MVOKBARF_def "MVOKBARF v == (MemVal v) | (v = OK) | (v = BadArg) | (v = RPCFailure)" + MVOKBA_def "MVOKBA v == (MemVal v) | (v = OK) | (v = BadArg)" + MVNROKBA_def "MVNROKBA v == (MemVal v) | (v = NotAResult) | (v = OK) | (v = BadArg)" + + (* the "base" variables: everything except resbar and hist (for any index) *) + MI_base "base_var " + + (* Environment's next-state relation *) + ENext_def "ENext p == REX l. #(MemLoc l) .& Call memCh p (#(Inl (read,l)))" + + (* Specification of the history variable used in the proof *) + HInit_def "$(HInit rmhist p) .= ($(rmhist@p) .= #histA)" + HNext_def "HNext rmhist p == + (rmhist@p)$ .= + (.if (MemReturn rmCh ires p .| RPCFail crCh rmCh rst p) + .then #histB + .else .if (MClkReply memCh crCh cst p) + .then #histA + .else $(rmhist@p))" + HistP_def "HistP rmhist p == + Init($(HInit rmhist p)) + .& [][HNext rmhist p]_" + Hist_def "Hist rmhist == RALL p. HistP rmhist p" + + (* definitions of e,c,r,m *) + e_def "e p == caller memCh @ p" + c_def "c p == " + r_def "r p == " + m_def "m p == " + + (* definition of the implementation (without the history variable) *) + IPImp_def "IPImp p == Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p) + .& MClkIPSpec memCh crCh cst p + .& RPCIPSpec crCh rmCh rst p + .& RPSpec rmCh mem ires p + .& (RALL l. #(MemLoc l) .-> MSpec rmCh mem ires l)" + + ImpInit_def "$(ImpInit p) .= ( .~ $(Calling memCh p) \ +\ .& $(MClkInit crCh cst p) \ +\ .& $(RPCInit rmCh rst p) \ +\ .& $(PInit ires p))" + + ImpNext_def "ImpNext p == [ENext p]_(e p) + .& [MClkNext memCh crCh cst p]_(c p) + .& [RPCNext crCh rmCh rst p]_(r p) + .& [RNext rmCh mem ires p]_(m p)" + + ImpLive_def "ImpLive p == WF(MClkFwd memCh crCh cst p)_(c p) + .& SF(MClkReply memCh crCh cst p)_(c p) + .& WF(RPCNext crCh rmCh rst p)_(r p) + .& WF(RNext rmCh mem ires p)_(m p) + .& WF(MemReturn rmCh ires p)_(m p)" + + Impl_def "Implementation == (RALL p. Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p)) + .& MClkISpec memCh crCh cst + .& RPCISpec crCh rmCh rst + .& IRSpec rmCh mem ires" + + ImpInv_def "$(ImpInv rmhist p) .= ($(S1 rmhist p) .| $(S2 rmhist p) .| $(S3 rmhist p) .| + $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p))" + + (* Definition of predicate S. + NB: The second conjunct of the definition in the paper is taken care of by + the type definitions. The last conjunct is asserted separately as the memory + invariant MemInv, proved in Memory.ML. *) + S_def "$(S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p) .= + ( ($(Calling memCh p) .= # ecalling) + .& ($(Calling crCh p) .= # ccalling) + .& (# ccalling .-> (arg[ $(crCh@p)] .= MClkRelayArg[ arg[$(memCh@p)] ])) + .& ((.~ # ccalling .& ($(cst@p) .= # clkB)) .-> MVOKBARF[ res[$(crCh@p)] ]) + .& ($(Calling rmCh p) .= # rcalling) + .& (# rcalling .-> (arg[ $(rmCh@p)] .= RPCRelayArg[ arg[$(crCh@p)] ])) + .& (.~ # rcalling .-> ($(ires@p) .= # NotAResult)) + .& ((.~ # rcalling .& ($(rst@p) .= # rpcB)) .-> MVOKBA[ res[$(rmCh@p)] ]) + .& ($(cst@p) .= # cs) + .& ($(rst@p) .= # rs) + .& (($(rmhist@p) .= #hs1) .| ($(rmhist@p) .= #hs2)) + .& (MVNROKBA[ $(ires@p)]))" + + S1_def "$(S1 rmhist p) .= $(S rmhist False False False clkA rpcA histA histA p)" + S2_def "$(S2 rmhist p) .= $(S rmhist True False False clkA rpcA histA histA p)" + S3_def "$(S3 rmhist p) .= $(S rmhist True True False clkB rpcA histA histB p)" + S4_def "$(S4 rmhist p) .= $(S rmhist True True True clkB rpcB histA histB p)" + S5_def "$(S5 rmhist p) .= $(S rmhist True True False clkB rpcB histB histB p)" + S6_def "$(S6 rmhist p) .= $(S rmhist True False False clkB rpcA histB histB p)" + + (* Definition of the refinement mapping resbar for result *) + resbar_def "$((resbar rmhist) @ p) .= + (.if ($(S1 rmhist p) .| $(S2 rmhist p)) + .then $(ires@p) + .else .if $(S3 rmhist p) + .then .if $(rmhist@p) .= #histA + .then $(ires@p) .else # MemFailure + .else .if $(S4 rmhist p) + .then .if ($(rmhist@p) .= #histB) .& ($(ires@p) .= # NotAResult) + .then #MemFailure .else $(ires@p) + .else .if $(S5 rmhist p) + .then res[$(rmCh@p)] + .else .if $(S6 rmhist p) + .then .if res[$(crCh@p)] .= #RPCFailure + .then #MemFailure .else res[$(crCh@p)] + .else #NotAResult)" (* dummy value *) + +end + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemoryParameters.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemoryParameters.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,24 @@ +(* + File: MemoryParameters.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: memory parameters (ML file) +*) + +val MP_simps = [BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal, + NotAResultNotOK, NotAResultNotBA, NotAResultNotMF] + @ (map (fn x => x RS not_sym) + [NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]); + + +(* Auxiliary rules *) + +qed_goal "MemValNotAResultE" MemoryParameters.thy + "[| MemVal x; (x ~= NotAResult ==> P) |] ==> P" + (fn [min,maj] => [rtac maj 1, + case_tac "x = NotAResult" 1, + cut_facts_tac [min,NotAResultNotVal] 1, + ALLGOALS Asm_full_simp_tac + ]); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/MemoryParameters.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,50 @@ +(* + File: MemoryParameters.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: MemoryParameters + Logic Image: TLA + + RPC-Memory example: Memory parameters +*) + +MemoryParameters = Prod + Sum + Arith + RPCMemoryParams + + +(* the memory operations. nb: data types must be defined in theories + that do not include Intensional -- otherwise the induction rule + can't be type-checked unambiguously. +*) +datatype Rd = read +datatype Wr = write + +types + (* legal arguments for the memory *) + memArgType = "(Rd * Locs) + (Wr * Locs * Vals)" + +consts + (* memory locations and contents *) + MemLoc :: "Locs => bool" + MemVal :: "Vals => bool" + + (* some particular values *) + OK :: "Vals" + BadArg :: "Vals" + MemFailure :: "Vals" + NotAResult :: "Vals" (* defined here for simplicity *) + + (* the initial value stored in each memory cell *) + InitVal :: "Vals" + +rules + (* basic assumptions about the above constants and predicates *) + BadArgNoMemVal "~MemVal(BadArg)" + MemFailNoMemVal "~MemVal(MemFailure)" + InitValMemVal "MemVal(InitVal)" + NotAResultNotVal "~MemVal(NotAResult)" + NotAResultNotOK "NotAResult ~= OK" + NotAResultNotBA "NotAResult ~= BadArg" + NotAResultNotMF "NotAResult ~= MemFailure" +end + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/ProcedureInterface.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/ProcedureInterface.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,62 @@ +(* + File: ProcedureInterface.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + Procedure interface (ML file) +*) + +Addsimps [slice_def]; + +(* ---------------------------------------------------------------------------- *) + +val Procedure_defs = [caller_def, rtrner_def, action_rewrite Calling_def, + Call_def, Return_def, + PLegalCaller_def, LegalCaller_def, + PLegalReturner_def, LegalReturner_def]; + +(* sample theorems (not used in the proof): + 1. calls and returns are mutually exclusive + +qed_goal "CallReturnMutex" ProcedureInterface.thy + "Call ch p v .-> .~ Return ch p w" + (fn prems => [ auto_tac (action_css addsimps2 [Call_def,Return_def]) ]); + + + 2. enabledness of calls and returns + NB: action_simp_tac is significantly faster than auto_tac + +qed_goal "Call_enabled" ProcedureInterface.thy + "!!p. base_var ((caller ch)@p) ==> (.~ $(Calling ch p) .-> $(Enabled (Call ch p (#v))))" + (fn _ => [action_simp_tac (!simpset addsimps [caller_def, Call_def]) + [] [base_enabled,Pair_inject] 1 + ]); + +qed_goal "Return_enabled" ProcedureInterface.thy + "!!p. base_var ((rtrner ch)@p) ==> $(Calling ch p) .-> $(Enabled (Return ch p (#v)))" + (fn _ => [action_simp_tac (!simpset addsimps [rtrner_def, Return_def]) + [] [base_enabled,Pair_inject] 1 + ]); + +*) + +(* Calls and returns change their subchannel *) +qed_goal "Call_changed" ProcedureInterface.thy + "Call ch p v .-> _((caller ch)@p)" + (fn _ => [auto_tac (!claset, + !simpset addsimps [angle_def,Call_def,caller_def, + action_rewrite Calling_def]) + ]); + +qed_goal "Return_changed" ProcedureInterface.thy + "Return ch p v .-> _((rtrner ch)@p)" + (fn _ => [auto_tac (!claset, + !simpset addsimps [angle_def,Return_def,rtrner_def, + action_rewrite Calling_def]) + ]); + +(* For convenience, generate elimination rules. + These rules loop if angle_def is active! *) +bind_thm("Call_changedE", action_impE Call_changed); +bind_thm("Return_changedE", action_impE Return_changed); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/ProcedureInterface.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,75 @@ +(* + File: ProcedureInterface.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: ProcedureInterface + Logic Image: TLA + + Procedure interface for RPC-Memory components. +*) + +ProcedureInterface = TLA + RPCMemoryParams + + +types + (* type of channels with argument type 'a and return type 'r. + we model a channel as an array of variables (of type chan) + rather than a single array-valued variable because the + notation gets a little simpler. + *) + ('a,'r) chan + ('a,'r) channel = (PrIds => ('a,'r) chan) stfun + +arities + chan :: (term,term) term + +consts + (* data-level functions *) + cbit,rbit :: "('a,'r) chan => bit" + arg :: "('a,'r) chan => 'a" + res :: "('a,'r) chan => 'r" + + (* slice through array-valued state function *) + "@" :: "('a => 'b) stfun => 'a => 'b stfun" (infixl 20) + + (* state functions *) + caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun" + rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun" + + (* state predicates *) + Calling :: "('a,'r) channel => PrIds => stpred" + + (* actions *) + Call :: "('a,'r) channel => PrIds => 'a trfct => action" + Return :: "('a,'r) channel => PrIds => 'r trfct => action" + + (* temporal formulas *) + PLegalCaller :: "('a,'r) channel => PrIds => temporal" + LegalCaller :: "('a,'r) channel => temporal" + PLegalReturner :: "('a,'r) channel => PrIds => temporal" + LegalReturner :: "('a,'r) channel => temporal" + +rules + slice_def "(x@i) s == x s i" + + caller_def "caller ch s p == (cbit (ch s p), arg (ch s p))" + rtrner_def "rtrner ch s p == (rbit (ch s p), res (ch s p))" + + Calling_def "$(Calling ch p) .= (cbit[$(ch@p)] .~= rbit[$(ch@p)])" + Call_def "Call ch p v == .~ $(Calling ch p) + .& (cbit[$(ch@p)])` .~= rbit[$(ch@p)] + .& (arg[$(ch@p)])` .= v" + Return_def "Return ch p v == $(Calling ch p) + .& (rbit[$(ch@p)])` .= cbit[$(ch@p)] + .& (res[$(ch@p)])` .= v" + + PLegalCaller_def "PLegalCaller ch p == + Init(.~ $(Calling ch p)) + .& [][ REX a. Call ch p (#a) ]_((caller ch)@p)" + LegalCaller_def "LegalCaller ch == RALL p. PLegalCaller ch p" + PLegalReturner_def "PLegalReturner ch p == + [][ REX v. Return ch p (#v) ]_((rtrner ch)@p)" + LegalReturner_def "LegalReturner ch == RALL p. PLegalReturner ch p" + +end + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/RPC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/RPC.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,59 @@ +(* + File: RPC.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: RPC specification (ML file) +*) + +val RPC_action_defs = + [RPCInit_def RS inteq_reflection] + @ [RPCFwd_def, RPCReject_def, RPCFail_def, RPCReply_def, RPCNext_def]; + +val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; + +(* The RPC component engages in an action for process p only if there is an outstanding, + unanswered call for that process. +*) + +qed_goal "RPCidle" RPC.thy + ".~ $(Calling send p) .-> .~ RPCNext send rcv rst p" + (fn _ => [ auto_tac (action_css addsimps2 (Return_def::RPC_action_defs)) ]); + +qed_goal "RPCbusy" RPC.thy + "$(Calling rcv p) .& ($(rst@p) .= #rpcB) .-> .~ RPCNext send rcv rst p" + (fn _ => [ auto_tac (action_css addsimps2 (RP_simps @ RPC_action_defs)) ]); + +(* unlifted versions as introduction rules *) + +bind_thm("RPCidleI", action_mp RPCidle); +bind_thm("RPCbusyI", action_mp RPCbusy); + +(* RPC failure actions are visible. *) +qed_goal "RPCFail_vis" RPC.thy + "RPCFail send rcv rst p .-> _" + (fn _ => [auto_tac (!claset addSEs [Return_changedE], + !simpset addsimps [angle_def,RPCNext_def,RPCFail_def]) + ]); + +qed_goal "RPCFail_Next_enabled" RPC.thy + "Enabled (RPCFail send rcv rst p) s \ +\ ==> Enabled (_) s" + (fn [prem] => [REPEAT (resolve_tac [prem RS enabled_mono,RPCFail_vis] 1)]); + +(* Enabledness of some actions *) + +qed_goal "RPCFail_enabled" RPC.thy + "!!p. base_var ==> \ +\ .~ $(Calling rcv p) .& $(Calling send p) .-> $(Enabled (RPCFail send rcv rst p))" + (fn _ => [action_simp_tac (!simpset addsimps [RPCFail_def,Return_def,caller_def,rtrner_def]) + [] [base_enabled,Pair_inject] 1 + ]); + +qed_goal "RPCReply_enabled" RPC.thy + "!!p. base_var ==> \ +\ .~ $(Calling rcv p) .& $(Calling send p) .& $(rst@p) .= #rpcB \ +\ .-> $(Enabled (RPCReply send rcv rst p))" + (fn _ => [action_simp_tac (!simpset addsimps [RPCReply_def,Return_def,caller_def,rtrner_def]) + [] [base_enabled,Pair_inject] 1]); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/RPC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/RPC.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,84 @@ +(* + File: RPC.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: RPC + Logic Image: TLA + + RPC-Memory example: RPC specification + For simplicity, specify the instance of RPC that is used in the + memory implementation (ignoring the BadCall exception). +*) + +RPC = RPCParameters + ProcedureInterface + + +types + rpcSndChType = "(rpcArgType,Vals) channel" + rpcRcvChType = "(memArgType,Vals) channel" + rpcStType = "(PrIds => rpcState) stfun" + +consts + (* state predicates *) + RPCInit :: "rpcRcvChType => rpcStType => PrIds => stpred" + + (* actions *) + RPCFwd :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" + RPCReject :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" + RPCFail :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" + RPCReply :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" + RPCNext :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" + + (* temporal *) + RPCIPSpec :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal" + RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal" + +rules + RPCInit_def "$(RPCInit rcv rst p) .= + ($(rst@p) .= # rpcA + .& .~ $(Calling rcv p))" + + RPCFwd_def "RPCFwd send rcv rst p == + $(Calling send p) + .& $(rst@p) .= # rpcA + .& IsLegalRcvArg[ arg[ $(send@p) ] ] + .& Call rcv p (RPCRelayArg[ arg[ $(send@p)] ]) + .& (rst@p)$ .= # rpcB + .& unchanged (rtrner send @ p)" + + RPCReject_def "RPCReject send rcv rst p == + $(rst@p) .= # rpcA + .& .~ IsLegalRcvArg[ arg[ $(send@p) ] ] + .& Return send p (#BadCall) + .& unchanged <(rst@p), (caller rcv @ p)>" + + RPCFail_def "RPCFail send rcv rst p == + .~ $(Calling rcv p) + .& Return send p (#RPCFailure) + .& (rst@p)$ .= #rpcA + .& unchanged (caller rcv @ p)" + + RPCReply_def "RPCReply send rcv rst p == + .~ $(Calling rcv p) + .& $(rst@p) .= #rpcB + .& Return send p (res[$(rcv@p)]) + .& (rst@p)$ .= #rpcA + .& unchanged (caller rcv @ p)" + + RPCNext_def "RPCNext send rcv rst p == + RPCFwd send rcv rst p + .| RPCReject send rcv rst p + .| RPCFail send rcv rst p + .| RPCReply send rcv rst p" + + RPCIPSpec_def "RPCIPSpec send rcv rst p == + Init($(RPCInit rcv rst p)) + .& [][ RPCNext send rcv rst p ]_ + .& WF(RPCNext send rcv rst p)_" + + RPCISpec_def "RPCISpec send rcv rst == RALL p. RPCIPSpec send rcv rst p" + +end + + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/RPCMemoryParams.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,28 @@ +(* + File: RPCMemoryParams.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: RPCMemoryParams + Logic Image: TLA + + Basic declarations for the RPC-memory example. +*) + +RPCMemoryParams = HOL + + +types + bit = "bool" (* signal wires for the procedure interface *) + (* Defined as bool for simplicity. All I should really need is *) + (* the existence of two distinct values. *) + Locs (* "syntactic" value type *) + Vals (* "syntactic" value type *) + PrIds (* process id's *) + +(* all of these are simple (HOL) types *) +arities + Locs :: term + Vals :: term + PrIds :: term + +end diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/RPCParameters.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/RPCParameters.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,12 @@ +(* + File: RPCParameters.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + + RPC-Memory example: RPC parameters (ML file) +*) + + +val RP_simps = MP_simps @ [RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] + @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]) + @ rpcOps.simps @ rpcState.simps; diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Memory/RPCParameters.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Memory/RPCParameters.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,54 @@ +(* + File: RPCParameters.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: RPCParameters + Logic Image: TLA + + RPC-Memory example: RPC parameters + For simplicity, specify the instance of RPC that is used in the + memory implementation. +*) + +RPCParameters = MemoryParameters + + +datatype rpcOps = remoteCall +datatype rpcState = rpcA | rpcB + +types + (* type of RPC arguments other than memory calls *) + noMemArgType + (* legal arguments for (our instance of) the RPC component *) + rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)" + +arities + noMemArgType :: term + +consts + (* some particular return values *) + RPCFailure :: "Vals" + BadCall :: "Vals" + + (* Translate an rpc call to a memory call and test if the current argument + is legal for the receiver (i.e., the memory). This can now be a little + simpler than for the generic RPC component. RelayArg returns an arbitrary + memory call for illegal arguments. *) + IsLegalRcvArg :: "rpcArgType => bool" + RPCRelayArg :: "rpcArgType => memArgType" + +rules + (* RPCFailure is different from MemVals and exceptions *) + RFNoMemVal "~(MemVal RPCFailure)" + NotAResultNotRF "NotAResult ~= RPCFailure" + OKNotRF "OK ~= RPCFailure" + BANotRF "BadArg ~= RPCFailure" + + IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)" + RPCRelayArg_def "RPCRelayArg ra == + case ra of Inl (rm) => (snd rm) + | Inr (rn) => Inl (read, @ l. True)" + +end + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/README.html Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,45 @@ +HOL/TLA/README + +

TLA: A formalization of TLA in HOL

+ +Author: Stephan Merz
+Copyright 1997 Universität München

+ +The distribution contains a representation of Lamport's + +Temporal Logic of Actions +in Isabelle/HOL. + +

+ +The encoding is mainly oriented towards practical verification +examples. It does not contain a formalization of TLA's semantics; +instead, it is based on a +complete axiomatization of the "raw" +(stuttering-sensitive) variant of propositional TLA. It is +accompanied by a +design note that explains the basic +setup and use of the prover. + +

+ +The distribution includes the following examples: +

+ +If you use Isabelle/TLA and have any comments, suggestions or contributions, +please contact Stephan Merz. + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/ROOT.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,17 @@ +(* Title: TLA/ROOT.ML + +Adds the Temporal Logic of Actions to a database containing Isabelle/HOL. +*) + +val banner = "Temporal Logic of Actions"; + +(* + raise the ambiguity level to avoid ambiguity warnings; + since Trueprop and TrueInt have both empty syntax, there is + an unavoidable ambiguity in the TLA (actually, Intensional) grammar. +*) +Syntax.ambiguity_level := 10000; + +use_thy "TLA"; + +val TLA_build_completed = (); diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Stfun.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Stfun.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,25 @@ +(* + File: Stfun.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Lemmas and tactics for states and state functions. +*) + +(* A stronger version of existential elimination (goal needn't be boolean) *) +qed_goalw "exE_prop" HOL.thy [Ex_def] + "[| ? x::'a.P(x); !!x. P(x) ==> PROP R |] ==> PROP R" + (fn prems => [REPEAT(resolve_tac prems 1)]); + +(* Might as well use that version in automated proofs *) +AddSEs [exE_prop]; + +(* [| base_var v; !!x. v x = c ==> PROP R |] ==> PROP R *) +bind_thm("baseE", (standard (base_var RS exE_prop))); + +qed_goal "PairVarE" Stfun.thy + "[| u = (x,y); [| v u = x; w u = y |] ==> PROP R |] ==> PROP R" + (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1, + ALLGOALS (asm_full_simp_tac (!simpset addsimps [pairSF_def])) + ]); + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/Stfun.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/Stfun.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,56 @@ +(* + File: TLA/Stfun.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: Stfun + Logic Image: HOL + +States and state functions for TLA +*) + +Stfun = Prod + + +types + state + 'a stfun = "state => 'a" + stpred = "bool stfun" + +arities + state :: term + +consts + (* For simplicity, we do not syntactically distinguish between state variables + and state functions, and treat "state" as an anonymous type. But we need a + "meta-predicate" to identify "base" state variables that represent the state + components of a system, in particular to define the enabledness of actions. + *) + base_var :: "'a stfun => bool" + + (* lift tupling to state functions *) + pairSF :: "['a stfun, 'b stfun] => ('a * 'b) stfun" + +syntax + "@tupleSF" :: "args => ('a * 'b) stfun" ("(1<_>)") + +translations + "" == " >" + "" == "pairSF x y" + "" => "x" + +rules + (* tupling *) + pairSF_def "(s) = (v(s),w(s))" + + (* "base" variables may be assigned arbitrary values by states. + NB: It's really stronger than that because "u" doesn't depend + on either c or v. In particular, if "==>" were replaced + with "==", base_pair would (still) not be derivable. + *) + base_var "base_var v ==> EX u. v u = c" + + (* a tuple of variables is "base" if each variable is "base" *) + base_pair "base_var = (base_var v & base_var w)" +end + +ML diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/TLA.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/TLA.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,1059 @@ +(* + File: TLA/TLA.ML + Author: Stephan Merz + Copyright: 1997 University of Munich + +Lemmas and tactics for temporal reasoning. +*) + +(* Specialize intensional introduction/elimination rules to temporal formulas *) + +qed_goal "tempI" TLA.thy "(!!sigma. (sigma |= (F::temporal))) ==> F" + (fn [prem] => [ REPEAT (resolve_tac [prem,intI] 1) ]); + +qed_goal "tempD" TLA.thy "F::temporal ==> (sigma |= F)" + (fn [prem] => [ REPEAT (resolve_tac [prem,intD] 1) ]); + + +(* ======== Functions to "unlift" temporal implications into HOL rules ====== *) + +(* Basic unlifting introduces a parameter "sigma" and applies basic rewrites, e.g. + F .= G gets (sigma |= F) = (sigma |= G) + F .-> G gets (sigma |= F) --> (sigma |= G) +*) +fun temp_unlift th = rewrite_rule intensional_rews (th RS tempD); + +(* F .-> G becomes sigma |= F ==> sigma |= G *) +fun temp_mp th = zero_var_indexes ((temp_unlift th) RS mp); + +(* F .-> G becomes [| sigma |= F; sigma |= G ==> R |] ==> R + so that it can be used as an elimination rule +*) +fun temp_impE th = zero_var_indexes ((temp_unlift th) RS impE); + +(* F .& G .-> H becomes [| sigma |= F; sigma |= G |] ==> sigma |= H *) +fun temp_conjmp th = zero_var_indexes (conjI RS (temp_mp th)); + +(* F .& G .-> H becomes [| sigma |= F; sigma |= G; (sigma |= H ==> R) |] ==> R *) +fun temp_conjimpE th = zero_var_indexes (conjI RS (temp_impE th)); + +(* Turn F .= G into meta-level rewrite rule F == G *) +fun temp_rewrite th = (rewrite_rule intensional_rews (th RS inteq_reflection)); + + +(* Update classical reasoner---will be updated once more below! *) + +AddSIs [tempI]; +AddDs [tempD]; + +val temp_cs = action_cs addSIs [tempI] addDs [tempD]; +val temp_css = (temp_cs,!simpset); + +(* ========================================================================= *) +section "Init"; + +(* Push logical connectives through Init. *) +qed_goal "Init_true" TLA.thy "Init(#True) .= #True" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_false" TLA.thy "Init(#False) .= #False" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_not" TLA.thy "Init(.~P) .= (.~Init(P))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_and" TLA.thy "Init(P .& Q) .= (Init(P) .& Init(Q))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_or" TLA.thy "Init(P .| Q) .= (Init(P) .| Init(Q))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_imp" TLA.thy "Init(P .-> Q) .= (Init(P) .-> Init(Q))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_iff" TLA.thy "Init(P .= Q) .= (Init(P) .= Init(Q))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_all" TLA.thy "Init(RALL x. P(x)) .= (RALL x. Init(P(x)))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +qed_goal "Init_ex" TLA.thy "Init(REX x. P(x)) .= (REX x. Init(P(x)))" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def]) ]); + +val Init_simps = map temp_rewrite + [Init_true,Init_false,Init_not,Init_and,Init_or, + Init_imp,Init_iff,Init_all,Init_ex]; + + +(* Temporal lemmas *) + +qed_goalw "DmdAct" TLA.thy [dmd_def,boxact_def] "(<>(F::action)) .= (<> Init F)" + (fn _ => [auto_tac (temp_css addsimps2 Init_simps)]); + + +(* ------------------------------------------------------------------------- *) +(*** "Simple temporal logic": only [] and <> ***) +(* ------------------------------------------------------------------------- *) +section "Simple temporal logic"; + +(* ------------------------ STL2 ------------------------------------------- *) +bind_thm("STL2", reflT); +bind_thm("STL2D", temp_mp STL2); + +(* The action variants. *) +qed_goalw "STL2b" TLA.thy [boxact_def] "[]P .-> Init P" + (fn _ => [rtac STL2 1]); +bind_thm("STL2bD", temp_mp STL2b); +(* see also STL2b_pr below: "[]P .-> Init(P .& P`)" *) + +(* Dual versions for <> *) +qed_goalw "ImplDmd" TLA.thy [dmd_def] "F .-> <>F" + (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]) ]); +bind_thm ("ImplDmdD", temp_mp ImplDmd); + +qed_goalw "InitDmd" TLA.thy [dmd_def] "Init(P) .-> <>P" + (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]); +bind_thm("InitDmdD", temp_mp InitDmd); + + +(* ------------------------ STL3 ------------------------------------------- *) +qed_goal "STL3" TLA.thy "([][]F) .= ([]F)" + (fn _ => [auto_tac (temp_css addIs2 [temp_mp transT,temp_mp STL2])]); + +(* corresponding elimination rule introduces double boxes: + [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W +*) +bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2)); +bind_thm("dup_boxD", (temp_unlift STL3) RS iffD1); + +(* dual versions for <> *) +qed_goalw "DmdDmd" TLA.thy [dmd_def] "(<><>F) .= (<>F)" + (fn _ => [ auto_tac (temp_css addsimps2 [STL3]) ]); +bind_thm("dup_dmdE", make_elim((temp_unlift DmdDmd) RS iffD2)); +bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1); + + +(* ------------------------ STL4 ------------------------------------------- *) +qed_goal "STL4" TLA.thy "(F .-> G) ==> ([]F .-> []G)" + (fn [prem] => [Auto_tac(), + rtac ((temp_mp normalT) RS mp) 1, + REPEAT (ares_tac [prem, necT RS tempD] 1) + ]); + +(* A more practical variant as an (unlifted) elimination rule *) +qed_goal "STL4E" TLA.thy + "[| (sigma |= []F); F .-> G |] ==> (sigma |= []G)" + (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp STL4]) 1) ]); + +(* see also STL4Edup below, which allows an auxiliary boxed formula: + []A /\ F => G + ----------------- + []A /\ []F => []G +*) + +(* The dual versions for <> *) +qed_goalw "DmdImpl" TLA.thy [dmd_def] + "(F .-> G) ==> (<>F .-> <>G)" + (fn [prem] => [fast_tac (temp_cs addSIs [int_mp prem] addSEs [STL4E]) 1]); + +qed_goal "DmdImplE" TLA.thy + "[| (sigma |= <>F); F .-> G |] ==> (sigma |= <>G)" + (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp DmdImpl]) 1) ]); + + +(* ------------------------ STL5 ------------------------------------------- *) +qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))" + (fn _ => [Auto_tac(), + subgoal_tac "sigma |= [](G .-> (F .& G))" 1, + etac ((temp_mp normalT) RS mp) 1, atac 1, + ALLGOALS (fast_tac (temp_cs addSEs [STL4E])) + ]); +(* rewrite rule to split conjunctions under boxes *) +bind_thm("split_box_conj", (temp_unlift STL5) RS sym); + +(* the corresponding elimination rule allows to combine boxes in the hypotheses + (NB: F and G must have the same type, i.e., both actions or temporals.) +*) +qed_goal "box_conjE" TLA.thy + "[| (sigma |= []F); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R" + (fn prems => [ REPEAT (resolve_tac + (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]); + +(* Define a tactic that tries to merge all boxes in an antecedent. The definition is + a bit kludgy: how do you simulate "double elim-resolution"? + Note: If there are boxed hypotheses of different types, the tactic may delete the + wrong formulas. We therefore also define less polymorphic tactics for + temporals and actions. +*) +qed_goal "box_thin" TLA.thy "[| (sigma |= []F); PROP W |] ==> PROP W" + (fn prems => [resolve_tac prems 1]); + +fun merge_box_tac i = + REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]); + +qed_goal "temp_box_conjE" TLA.thy + "[| (sigma |= [](F::temporal)); (sigma |= []G); (sigma |= [](F.&G)) ==> PROP R |] ==> PROP R" + (fn prems => [ REPEAT (resolve_tac + (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]); +qed_goal "temp_box_thin" TLA.thy "[| (sigma |= [](F::temporal)); PROP W |] ==> PROP W" + (fn prems => [resolve_tac prems 1]); +fun merge_temp_box_tac i = + REPEAT_DETERM (EVERY [etac temp_box_conjE i, atac i, etac temp_box_thin i]); + +qed_goal "act_box_conjE" TLA.thy + "[| (sigma |= [](A::action)); (sigma |= []B); (sigma |= [](A.&B)) ==> PROP R |] ==> PROP R" + (fn prems => [ REPEAT (resolve_tac + (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]); +qed_goal "act_box_thin" TLA.thy "[| (sigma |= [](A::action)); PROP W |] ==> PROP W" + (fn prems => [resolve_tac prems 1]); +fun merge_act_box_tac i = + REPEAT_DETERM (EVERY [etac act_box_conjE i, atac i, etac act_box_thin i]); + +(* rewrite rule to push universal quantification through box: + (sigma |= [](RALL x. F x)) = (! x. (sigma |= []F x)) +*) +bind_thm("all_box", standard((temp_unlift allT) RS sym)); + + +qed_goal "DmdOr" TLA.thy "(<>(F .| G)) .= (<>F .| <>G)" + (fn _ => [auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]), + TRYALL (EVERY' [etac swap, + merge_box_tac, + fast_tac (temp_cs addSEs [STL4E])]) + ]); + +qed_goal "exT" TLA.thy "(REX x. <>(F x)) .= (<>(REX x. F x))" + (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def,temp_rewrite Not_rex,all_box]) ]); + +bind_thm("ex_dmd", standard((temp_unlift exT) RS sym)); + + +qed_goal "STL4Edup" TLA.thy + "!!sigma. [| (sigma |= []A); (sigma |= []F); F .& []A .-> G |] ==> (sigma |= []G)" + (fn _ => [etac dup_boxE 1, + merge_box_tac 1, + etac STL4E 1, + atac 1 + ]); + +qed_goalw "DmdImpl2" TLA.thy [dmd_def] + "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)" + (fn _ => [Auto_tac(), + etac notE 1, + merge_box_tac 1, + fast_tac (temp_cs addSEs [STL4E]) 1 + ]); + +qed_goal "InfImpl" TLA.thy + "[| (sigma |= []<>F); (sigma |= []G); F .& G .-> H |] ==> (sigma |= []<>H)" + (fn [prem1,prem2,prem3] + => [cut_facts_tac [prem1,prem2] 1, + eres_inst_tac [("F","G")] dup_boxE 1, + merge_box_tac 1, + fast_tac (temp_cs addSEs [STL4E,DmdImpl2] addSIs [int_mp prem3]) 1 + ]); + +(* ------------------------ STL6 ------------------------------------------- *) +(* Used in the proof of STL6, but useful in itself. *) +qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)" + (fn _ => [ Auto_tac(), + etac dup_boxE 1, + merge_box_tac 1, + etac swap 1, + fast_tac (temp_cs addSEs [STL4E]) 1 ]); +bind_thm("BoxDmd", temp_conjmp BoxDmdT); + +(* weaker than BoxDmd, but more polymorphic (and often just right) *) +qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)" + (fn _ => [ Auto_tac(), + merge_box_tac 1, + fast_tac (temp_cs addSEs [notE,STL4E]) 1 + ]); + +qed_goal "STL6" TLA.thy "<>[]F .& <>[]G .-> <>[](F .& G)" + (fn _ => [auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]), + etac (temp_conjimpE linT) 1, atac 1, etac thin_rl 1, + rtac ((temp_unlift DmdDmd) RS iffD1) 1, + etac disjE 1, + etac DmdImplE 1, rtac BoxDmdT 1, + (* the second subgoal needs commutativity of .&, which complicates the proof *) + etac DmdImplE 1, + Auto_tac(), + etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1, + fast_tac (temp_cs addSEs [DmdImplE]) 1 + ]); + + +(* ------------------------ True / False ----------------------------------------- *) +section "Simplification of constants"; + +qed_goal "BoxTrue" TLA.thy "[](#True)" + (fn _ => [ fast_tac (temp_cs addSIs [necT]) 1 ]); + +qed_goal "BoxTrue_simp" TLA.thy "([](#True)) .= #True" + (fn _ => [ fast_tac (temp_cs addSIs [BoxTrue RS tempD]) 1 ]); + +qed_goal "DmdFalse_simp" TLA.thy "(<>(#False)) .= #False" + (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def, BoxTrue_simp]) ]); + +qed_goal "DmdTrue_simp" TLA.thy "(<>((#True)::temporal)) .= #True" + (fn _ => [ fast_tac (temp_cs addSIs [ImplDmdD]) 1 ]); + +qed_goal "DmdActTrue_simp" TLA.thy "(<>((#True)::action)) .= #True" + (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSIs2 [InitDmdD]) ]); + +qed_goal "BoxFalse_simp" TLA.thy "([]((#False)::temporal)) .= #False" + (fn _ => [ fast_tac (temp_cs addSDs [STL2D]) 1 ]); + +qed_goal "BoxActFalse_simp" TLA.thy "([]((#False)::action)) .= #False" + (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) ]); + +qed_goal "BoxConst_simp" TLA.thy "([]((#P)::temporal)) .= #P" + (fn _ => [rtac tempI 1, + case_tac "P" 1, + auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxFalse_simp]) + ]); + +qed_goal "BoxActConst_simp" TLA.thy "([]((#P)::action)) .= #P" + (fn _ => [rtac tempI 1, + case_tac "P" 1, + auto_tac (temp_css addsimps2 [BoxTrue_simp,BoxActFalse_simp]) + ]); + +qed_goal "DmdConst_simp" TLA.thy "(<>((#P)::temporal)) .= #P" + (fn _ => [rtac tempI 1, + case_tac "P" 1, + auto_tac (temp_css addsimps2 [DmdTrue_simp,DmdFalse_simp]) + ]); + +qed_goal "DmdActConst_simp" TLA.thy "(<>((#P)::action)) .= #P" + (fn _ => [rtac tempI 1, + case_tac "P" 1, + auto_tac (temp_css addsimps2 [DmdActTrue_simp,DmdFalse_simp]) + ]); + +val temp_simps = map temp_rewrite + [BoxTrue_simp,DmdFalse_simp,DmdTrue_simp, + DmdActTrue_simp, BoxFalse_simp, BoxActFalse_simp, + BoxConst_simp,BoxActConst_simp,DmdConst_simp,DmdActConst_simp]; + +(* Make these rewrites active by default *) +Addsimps temp_simps; +val temp_css = temp_css addsimps2 temp_simps; +val temp_cs = temp_cs addss (empty_ss addsimps temp_simps); + + +(* ------------------------ Further rewrites ----------------------------------------- *) +section "Further rewrites"; + +qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)" + (fn _ => [ Auto_tac() ]); + +qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)" + (fn _ => [ Auto_tac () ]); + +(* These are not by default included in temp_css, because they could be harmful, + e.g. []F .& .~[]F becomes []F .& <>.~F !! *) +val more_temp_simps = (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd]) + @ (map (fn th => (temp_unlift th) RS eq_reflection) + [NotBox, NotDmd]); + +qed_goal "BoxDmdBox" TLA.thy "([]<>[]F) .= (<>[]F)" + (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]), + rtac ccontr 1, + subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1, + etac thin_rl 1, + Auto_tac(), + etac (temp_conjimpE STL6) 1, atac 1, + Asm_full_simp_tac 1, + ALLGOALS (asm_full_simp_tac (!simpset addsimps more_temp_simps)) + ]); + +qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "(<>[]<>F) .= ([]<>F)" + (fn _ => [auto_tac (temp_css addsimps2 [temp_rewrite (rewrite_rule [dmd_def] BoxDmdBox)])]); + +val more_temp_simps = more_temp_simps @ (map temp_rewrite [BoxDmdBox, DmdBoxDmd]); + + +(* ------------------------ Miscellaneous ----------------------------------- *) + +qed_goal "BoxOr" TLA.thy + "!!sigma. [| (sigma |= []F .| []G) |] ==> (sigma |= [](F .| G))" + (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]); + +qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F" + (fn _ => [Auto_tac(), + rtac ccontr 1, + auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6]) + ]); + +(* Although the script is the same, the derivation isn't polymorphic and doesn't + work for other types of formulas (uses STL2). +*) +qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A" + (fn _ => [Auto_tac(), + rtac ccontr 1, + auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6]) + ]); + +qed_goal "BoxDmdDmdBox" TLA.thy + "!!sigma. [| (sigma |= []<>F); (sigma |= <>[]G) |] ==> (sigma |= []<>(F .& G))" + (fn _ => [rtac ccontr 1, + rewrite_goals_tac more_temp_simps, + etac (temp_conjimpE STL6) 1, atac 1, + subgoal_tac "sigma |= <>[].~F" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1, + fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1 + ]); + + +(* ------------------------------------------------------------------------- *) +(*** TLA-specific theorems: primed formulas ***) +(* ------------------------------------------------------------------------- *) +section "priming"; + +(* ------------------------ TLA2 ------------------------------------------- *) +qed_goal "STL2bD_pr" TLA.thy + "!!sigma. (sigma |= []P) ==> (sigma |= Init(P .& P`))" + (fn _ => [rewrite_goals_tac Init_simps, + fast_tac (temp_cs addSIs [temp_mp primeI, STL2bD]) 1]); + +(* Auxiliary lemma allows priming of boxed actions *) +qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)" + (fn _ => [Auto_tac(), + etac dup_boxE 1, + auto_tac (temp_css addsimps2 [boxact_def] + addSIs2 [STL2bD_pr] addSEs2 [STL4E]) + ]); + +qed_goal "TLA2" TLA.thy "P .& P` .-> Q ==> []P .-> []Q" + (fn prems => [fast_tac (temp_cs addSIs prems addDs [temp_mp BoxPrime] addEs [STL4E]) 1]); + +qed_goal "TLA2E" TLA.thy + "[| (sigma |= []P); P .& P` .-> Q |] ==> (sigma |= []Q)" + (fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_mp TLA2])) 1)]); + +qed_goalw "DmdPrime" TLA.thy [dmd_def] "(<>P`) .-> (<>P)" + (fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]); + + +(* ------------------------ INV1, stable --------------------------------------- *) +section "stable, invariant"; + +qed_goal "ind_rule" TLA.thy + "[| (sigma |= []H); (sigma |= Init(P)); H .-> (Init(P) .& .~[]F .-> Init(P`) .& F) |] \ +\ ==> (sigma |= []F)" + (fn prems => [rtac ((temp_mp indT) RS mp) 1, + REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]); + + +qed_goalw "INV1" TLA.thy [stable_def,boxact_def] + "Init(P) .& stable(P) .-> []P" + (fn _ => [auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])]); +bind_thm("INV1I", temp_conjmp INV1); + +qed_goalw "StableL" TLA.thy [stable_def] + "(P .& A .-> P`) ==> ([]A .-> stable(P))" + (fn [prem] => [fast_tac (temp_cs addSIs [action_mp prem] addSEs [STL4E]) 1]); + +qed_goal "Stable" TLA.thy + "[| (sigma |= []A); P .& A .-> P` |] ==> (sigma |= stable P)" + (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp StableL]) 1) ]); + +(* Generalization of INV1 *) +qed_goalw "StableBox" TLA.thy [stable_def] + "!!sigma. (sigma |= stable P) ==> (sigma |= [](Init P .-> []P))" + (fn _ => [etac dup_boxE 1, + auto_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I]) + ]); + +(* useful for WF2 / SF2 *) +qed_goal "DmdStable" TLA.thy + "!!sigma. [| (sigma |= stable P); (sigma |= <>P) |] ==> (sigma |= <>[]P)" + (fn _ => [rtac DmdImpl2 1, + etac StableBox 2, + auto_tac (temp_css addsimps2 [DmdAct]) + ]); + +(* ---------------- (Semi-)automatic invariant tactics ---------------------- *) + +(* inv_tac reduces goals of the form ... ==> sigma |= []P *) +fun inv_tac css = + SELECT_GOAL + (EVERY [auto_tac css, + TRY (merge_box_tac 1), + rtac INV1I 1, (* fail if the goal is not a box *) + TRYALL (etac Stable)]); + +(* auto_inv_tac applies inv_tac and then tries to attack the subgoals; + in simple cases it may be able to handle goals like MyProg .-> []Inv. + In these simple cases the simplifier seems to be more useful than the + auto-tactic, which applies too much propositional logic and simplifies + too late. +*) + +fun auto_inv_tac ss = + SELECT_GOAL + ((inv_tac (!claset,ss) 1) THEN + (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] []))); + + +qed_goalw "unless" TLA.thy [dmd_def] + "!!sigma. (sigma |= [](P .-> P` .| Q`)) ==> (sigma |= stable P .| <>Q`)" + (fn _ => [action_simp_tac (!simpset) [disjCI] [] 1, + merge_box_tac 1, + fast_tac (temp_cs addSEs [Stable]) 1 + ]); + + +(* --------------------- Recursive expansions --------------------------------------- *) +section "recursive expansions"; + +(* Recursive expansions of [] and <>, restricted to state predicates to avoid looping *) +qed_goal "BoxRec" TLA.thy "([]$P) .= (Init($P) .& ([]P$))" + (fn _ => [auto_tac (temp_css addSIs2 [STL2bD]), + fast_tac (temp_cs addSEs [TLA2E]) 1, + auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E]) + ]); + +qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))" + (fn _ => [Auto_tac(), + etac notE 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps) + addIs2 [INV1I] addEs2 [STL4E])) 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1, + fast_tac (temp_cs addSEs [notE,TLA2E]) 1 + ]); + +qed_goal "DmdRec2" TLA.thy + "!!sigma. [| (sigma |= <>($P)); (sigma |= [](.~P$)) |] ==> (sigma |= Init($P))" + (fn _ => [dtac ((temp_unlift DmdRec) RS iffD1) 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1 + ]); + +(* The "=>" part of the following is a little intricate. *) +qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)" + (fn _ => [Auto_tac(), + rtac classical 1, + rtac (temp_mp DBImplBDAct) 1, + subgoal_tac "sigma |= <>[]$P" 1, + fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1, + subgoal_tac "sigma |= <>[](<>$P .& [].~P$)" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [boxact_def] + addSEs2 [DmdImplE,STL4E,DmdRec2])) 1, + SELECT_GOAL (auto_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps)) 1, + fast_tac (temp_cs addIs [temp_mp DmdPrime] addSEs [STL4E]) 1 + ]); + +(* ------------------------ fairness ------------------------------------------- *) +section "fairness"; + +(* alternative definitions of fairness *) +qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def] + "WF(A)_v .= (([]<>.~$(Enabled(_v))) .| []<>_v)" + (fn _ => [ fast_tac temp_cs 1 ]); + +qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def] + "SF(A)_v .= ((<>[].~$(Enabled(_v))) .| []<>_v)" + (fn _ => [ fast_tac temp_cs 1 ]); + +(* theorems to "box" fairness conditions *) +qed_goal "BoxWFI" TLA.thy + "!!sigma. (sigma |= WF(A)_v) ==> (sigma |= []WF(A)_v)" + (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite WF_alt::more_temp_simps) addSIs2 [BoxOr]) ]); + +qed_goal "WF_Box" TLA.thy "([]WF(A)_v) .= WF(A)_v" + (fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2D]) 1 ]); + +qed_goal "BoxSFI" TLA.thy + "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= []SF(A)_v)" + (fn _ => [ auto_tac (temp_css addsimps2 (temp_rewrite SF_alt::more_temp_simps) addSIs2 [BoxOr]) ]); + +qed_goal "SF_Box" TLA.thy "([]SF(A)_v) .= SF(A)_v" + (fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2D]) 1 ]); + +val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]); + +qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def] + "!!sigma. (sigma |= SF(A)_v) ==> (sigma |= WF(A)_v)" + (fn _ => [ fast_tac (temp_cs addSDs [temp_mp DBImplBDAct]) 1 ]); + +(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *) +val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1)); + + +(* ------------------------------ leads-to ------------------------------ *) + +section "~>"; + +qed_goalw "leadsto_init" TLA.thy [leadsto] + "!!sigma. [| (sigma |= Init P); (sigma |= P ~> Q) |] ==> (sigma |= <>Q)" + (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]); + +qed_goalw "streett_leadsto" TLA.thy [leadsto] + "([]<>P .-> []<>Q) .= (<>(P ~> Q))" + (fn _ => [Auto_tac(), + asm_full_simp_tac (!simpset addsimps boxact_def::more_temp_simps) 1, + SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] + addsimps2 Init_simps)) 1, + SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1, + subgoal_tac "sigma |= []<><>Q" 1, + asm_full_simp_tac (!simpset addsimps more_temp_simps) 1, + rewtac (temp_rewrite DmdAct), + dtac BoxDmdDmdBox 1, atac 1, + auto_tac (temp_css addSEs2 [DmdImplE,STL4E]) + ]); + +qed_goal "leadsto_infinite" TLA.thy + "!!sigma. [| (sigma |= []<>P); (sigma |= P ~> Q) |] ==> (sigma |= []<>Q)" + (fn _ => [rtac ((temp_unlift streett_leadsto) RS iffD2 RS mp) 1, + auto_tac (temp_css addSIs2 [ImplDmdD]) + ]); + +(* In particular, strong fairness is a Streett condition. The following + rules are sometimes easier to use than WF2 or SF2 below. +*) +qed_goalw "leadsto_SF" TLA.thy [SF_def] + "!!sigma. (sigma |= $(Enabled(_v)) ~> _v) ==> sigma |= SF(A)_v" + (fn _ => [step_tac temp_cs 1, + rtac leadsto_infinite 1, + ALLGOALS atac + ]); + +bind_thm("leadsto_WF", leadsto_SF RS SFImplWF); + +(* introduce an invariant into the proof of a leadsto assertion. + []I => ((P ~> Q) = (P /\ I ~> Q)) +*) +qed_goalw "INV_leadsto" TLA.thy [leadsto] + "!!sigma. [| (sigma |= []I); (sigma |= (P .& I) ~> Q) |] ==> (sigma |= P ~> Q)" + (fn _ => [etac STL4Edup 1, atac 1, + auto_tac (temp_css addsimps2 [Init_def] addSDs2 [STL2bD]) + ]); + +qed_goalw "leadsto_classical" TLA.thy [leadsto,dmd_def] + "!!sigma. (sigma |= [](Init P .& [].~Q .-> <>Q)) ==> (sigma |= P ~> Q)" + (fn _ => [fast_tac (temp_cs addSEs [STL4E]) 1]); + +qed_goalw "leadsto_false" TLA.thy [leadsto] + "(P ~> #False) .= ([] .~P)" + (fn _ => [ auto_tac (temp_css addsimps2 boxact_def::Init_simps) ]); + +(* basic leadsto properties, cf. Unity *) + +qed_goal "ImplLeadsto" TLA.thy + "!!sigma. (sigma |= [](P .-> Q)) ==> (sigma |= (P ~> Q))" + (fn _ => [etac INV_leadsto 1, rewtac leadsto, + rtac (temp_unlift necT) 1, + auto_tac (temp_css addSIs2 [InitDmdD] addsimps2 [Init_def]) + ]); + +qed_goal "EnsuresLeadsto" TLA.thy + "A .& P .-> Q` ==> []A .-> (P ~> Q)" + (fn [prem] => [auto_tac (temp_css addSEs2 [INV_leadsto]), + rewtac leadsto, + auto_tac (temp_css addSIs2 [temp_unlift necT]), + rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1, + auto_tac (action_css addsimps2 [Init_def] addSIs2 [action_mp prem]) + ]); + +qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto] + "!!sigma. sigma |= [](P .-> Q`) ==> sigma |= P ~> Q" + (fn _ => [subgoal_tac "sigma |= []Init(P .-> Q`)" 1, + etac STL4E 1, + auto_tac (temp_css addsimps2 boxact_def::Init_simps + addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)]) + ]); + +qed_goal "EnsuresInfinite" TLA.thy + "[| (sigma |= []<>P); (sigma |= []A); A .& P .-> Q` |] ==> (sigma |= []<>Q)" + (fn prems => [REPEAT (resolve_tac (prems @ [leadsto_infinite, + temp_mp EnsuresLeadsto]) 1)]); + +(*** Gronning's lattice rules (taken from TLP) ***) +section "Lattice rules"; + +qed_goalw "LatticeReflexivity" TLA.thy [leadsto] "F ~> F" + (fn _ => [REPEAT (resolve_tac [necT,InitDmd] 1)]); + +qed_goalw "LatticeTransitivity" TLA.thy [leadsto] + "!!sigma. [| (sigma |= G ~> H); (sigma |= F ~> G) |] ==> (sigma |= F ~> H)" + (fn _ => [etac dup_boxE 1, (* [][](Init G .-> H) *) + merge_box_tac 1, + auto_tac (temp_css addSEs2 [STL4E]), + rewtac (temp_rewrite DmdAct), + subgoal_tac "sigmaa |= <><> Init H" 1, + asm_full_simp_tac (!simpset addsimps more_temp_simps) 1, + fast_tac (temp_cs addSEs [DmdImpl2]) 1 + ]); + +qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto] + "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= F ~> H)" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]); + +qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto] + "!!sigma. (sigma |= (F .| G) ~> H) ==> (sigma |= G ~> H)" + (fn _ => [ auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) ]); + +qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto] + "!!sigma. [| (sigma |= F ~> H); (sigma |= G ~> H) |] ==> (sigma |= (F .| G) ~> H)" + (fn _ => [merge_box_tac 1, + auto_tac (temp_css addsimps2 [Init_def] addSEs2 [STL4E]) + ]); + +qed_goal "LatticeDiamond" TLA.thy + "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| C)); (sigma |= C ~> D) |] \ +\ ==> (sigma |= A ~> D)" + (fn _ => [subgoal_tac "sigma |= (B .| C) ~> D" 1, + eres_inst_tac [("G", "B .| C")] LatticeTransitivity 1, + ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro])) + ]); + +qed_goal "LatticeTriangle" TLA.thy + "!!sigma. [| (sigma |= B ~> D); (sigma |= A ~> (B .| D)) |] ==> (sigma |= A ~> D)" + (fn _ => [subgoal_tac "sigma |= (B .| D) ~> D" 1, + eres_inst_tac [("G", "B .| D")] LatticeTransitivity 1, atac 1, + auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] addIs2 [ImplLeadsto]) + ]); + +(*** Lamport's fairness rules ***) +section "Fairness rules"; + +qed_goalw "WF1" TLA.thy [leadsto] + "[| P .& N .-> P` .| Q`; \ +\ P .& N .& _v .-> Q`; \ +\ P .& N .-> $(Enabled(_v)) |] \ +\ ==> []N .& WF(A)_v .-> (P ~> Q)" + (fn [prem1,prem2,prem3] + => [auto_tac (temp_css addSDs2 [BoxWFI]), + etac STL4Edup 1, atac 1, + Auto_tac(), + subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1, + auto_tac (temp_css addSDs2 [unless]), + etac (temp_conjimpE INV1) 1, atac 1, + merge_box_tac 1, + rtac STL2D 1, + rtac EnsuresInfinite 1, atac 2, + SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1, + atac 2, + subgoal_tac "sigmaa |= [][]$(Enabled(_v))" 1, + merge_box_tac 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1, + SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN + (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1, + fast_tac (action_cs addSIs [action_mp prem2]) 1, + fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1, + fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1 + ]); + +(* Sometimes easier to use; designed for action B rather than state predicate Q *) +qed_goalw "WF_leadsto" TLA.thy [leadsto] + "[| N .& P .-> $Enabled (_v); \ +\ N .& _v .-> B; \ +\ [](N .& [.~A]_v) .-> stable P |] \ +\ ==> []N .& WF(A)_v .-> (P ~> B)" + (fn [prem1,prem2,prem3] + => [auto_tac (temp_css addSDs2 [BoxWFI]), + etac STL4Edup 1, atac 1, + Auto_tac(), + subgoal_tac "sigmaa |= <>_v" 1, + SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1, + rtac classical 1, + rtac STL2D 1, + auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]), + rtac ImplDmdD 1, + rtac (temp_mp (prem1 RS STL4)) 1, + auto_tac (temp_css addsimps2 [split_box_conj]), + etac INV1I 1, + merge_act_box_tac 1, + auto_tac (temp_css addsimps2 [temp_rewrite not_angle] addSEs2 [temp_mp prem3]) + ]); + +qed_goalw "SF1" TLA.thy [leadsto] + "[| P .& N .-> P` .| Q`; \ +\ P .& N .& _v .-> Q`; \ +\ []P .& []N .& []F .-> <>$(Enabled(_v)) |] \ +\ ==> []N .& SF(A)_v .& []F .-> (P ~> Q)" + (fn [prem1,prem2,prem3] => + [auto_tac (temp_css addSDs2 [BoxSFI]), + eres_inst_tac [("F","F")] dup_boxE 1, + merge_temp_box_tac 1, + etac STL4Edup 1, atac 1, + Auto_tac(), + subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1, + auto_tac (temp_css addSDs2 [unless]), + etac (temp_conjimpE INV1) 1, atac 1, + merge_act_box_tac 1, + rtac STL2D 1, + rtac EnsuresInfinite 1, atac 2, + SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1, + atac 2, + subgoal_tac "sigmaa |= []<>$(Enabled(_v))" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1, + eres_inst_tac [("F","F")] dup_boxE 1, + etac STL4Edup 1, atac 1, + fast_tac (temp_cs addSEs [STL4E] addSIs [temp_mp prem3]) 1, + fast_tac (action_cs addSIs [action_mp prem2]) 1, + fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1, + fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1 + ]); + +qed_goal "WF2" TLA.thy + "[| N .& _f .-> _g; \ +\ P .& P` .& _f .-> B; \ +\ P .& $(Enabled(_g)) .-> $(Enabled(_f)); \ +\ [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(_g))) .-> <>[]P |] \ +\ ==> []N .& WF(A)_f .& []F .-> WF(M)_g" + (fn [prem1,prem2,prem3,prem4] + => [Auto_tac(), + case_tac "sigma |= <>[]$Enabled(_g)" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2, + case_tac "sigma |= <>[][.~B]_f" 1, + subgoal_tac "sigma |= <>[]P" 1, + asm_full_simp_tac (!simpset addsimps [WF_def]) 1, + rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1, + eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1, + etac (temp_conjimpE STL6) 1, atac 1, + subgoal_tac "sigma |= <>[]$Enabled(_f)" 1, + dtac mp 1, atac 1, + subgoal_tac "sigma |= <>([]N .& []P .& []<>_f)" 1, + rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1, + eres_inst_tac [("F","[]N .& []P .& []<>_f")] DmdImplE 1, + SELECT_GOAL (Auto_tac()) 1, + dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1, + merge_act_box_tac 1, + etac InfImpl 1, atac 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1, + etac BoxDmd 1, + dres_inst_tac [("F","<>_f"),("G","[]P")] BoxDmd 1, atac 1, + eres_inst_tac [("F","[]<>_f .& []P")] DmdImplE 1, + SELECT_GOAL (Auto_tac ()) 1, + rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1, + fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1, + etac (temp_conjimpE STL6) 1, atac 1, + eres_inst_tac [("V","sigma |= <>[][.~ B]_f")] thin_rl 1, + dtac BoxWFI 1, + eres_inst_tac [("F","N")] dup_boxE 1, + eres_inst_tac [("F","F")] dup_boxE 1, + merge_temp_box_tac 1, + dtac BoxDmd 1, atac 1, + eres_inst_tac [("V","sigma |= <>[]($Enabled (_g) .& [.~ B]_f)")] thin_rl 1, + rtac dup_dmdD 1, + rtac (temp_mp (prem4 RS DmdImpl)) 1, + etac DmdImplE 1, + SELECT_GOAL + (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3] + addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1, + asm_full_simp_tac (!simpset addsimps (WF_def::more_temp_simps)) 1, + etac InfImpl 1, atac 1, + SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1, + ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def])) + ]); + +qed_goal "SF2" TLA.thy + "[| N .& _f .-> _g; \ +\ P .& P` .& _f .-> B; \ +\ P .& $(Enabled(_g)) .-> $(Enabled(_f)); \ +\ [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(_g))) .-> <>[]P |] \ +\ ==> []N .& SF(A)_f .& []F .-> SF(M)_g" + (fn [prem1,prem2,prem3,prem4] + => [Auto_tac(), + case_tac "sigma |= []<>$Enabled(_g)" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2, + case_tac "sigma |= <>[][.~B]_f" 1, + subgoal_tac "sigma |= <>[]P" 1, + asm_full_simp_tac (!simpset addsimps [SF_def]) 1, + rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1, + eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1, + dtac BoxDmdDmdBox 1, atac 1, + subgoal_tac "sigma |= []<>$Enabled(_f)" 1, + dtac mp 1, atac 1, + subgoal_tac "sigma |= <>([]N .& []P .& []<>_f)" 1, + rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1, + eres_inst_tac [("F","[]N .& []P .& []<>_f")] DmdImplE 1, + SELECT_GOAL (Auto_tac()) 1, + dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1, + merge_act_box_tac 1, + etac InfImpl 1, atac 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1, + etac BoxDmd 1, + dres_inst_tac [("F","<>_f"),("G","[]P")] BoxDmd 1, atac 1, + eres_inst_tac [("F","[]<>_f .& []P")] DmdImplE 1, + SELECT_GOAL (Auto_tac ()) 1, + rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1, + fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1, + dtac BoxSFI 1, + eres_inst_tac [("F","N")] dup_boxE 1, + eres_inst_tac [("F","F")] dup_boxE 1, + eres_inst_tac [("F","<>$Enabled (_g)")] dup_boxE 1, + merge_temp_box_tac 1, + dtac (temp_conjmp BoxDmdT2) 1, atac 1, + rtac dup_dmdD 1, + rtac (temp_mp (prem4 RS DmdImpl)) 1, + SELECT_GOAL + (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3] + addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd] + addSEs2 [DmdImplE])) 1, + asm_full_simp_tac (!simpset addsimps (SF_def::more_temp_simps)) 1, + eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1, + SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1, + ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def])) + ]); + +(* ------------------------------------------------------------------------- *) +(*** Liveness proofs by well-founded orderings ***) +(* ------------------------------------------------------------------------- *) +section "Well-founded orderings"; + +qed_goal "wf_dmd" TLA.thy + "[| (wf r); \ +\ !!x. sigma |= [](F x .-> <>G .| <>(REX y. #((y,x):r) .& F y)) \ +\ |] ==> sigma |= [](F x .-> <>G)" + (fn prem1::prems => + [cut_facts_tac [prem1] 1, + etac wf_induct 1, + subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1, + cut_facts_tac prems 1, + etac STL4Edup 1, atac 1, + Auto_tac(), etac swap 1, atac 1, + rtac dup_dmdD 1, + etac DmdImpl2 1, atac 1, + subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1, + fast_tac (temp_cs addSEs [STL4E]) 1, + auto_tac (temp_css addsimps2 [all_box]), + etac allE 1, etac impCE 1, + rtac (temp_unlift necT) 1, + auto_tac (temp_css addSEs2 [STL4E]) + ]); + +(* Special case: leadsto via well-foundedness *) +qed_goalw "wf_leadsto" TLA.thy [leadsto] + "[| (wf r); \ +\ !!x. sigma |= P x ~> (Q .| (REX y. #((y,x):r) .& P y)) \ +\ |] ==> sigma |= P x ~> Q" + (fn prems => [REPEAT (resolve_tac (wf_dmd::prems) 1), + resolve_tac (prems RL [STL4E]) 1, + auto_tac (temp_css addsimps2 [temp_rewrite DmdOr]), + fast_tac temp_cs 1, + etac swap 1, + rewtac (temp_rewrite DmdAct), + auto_tac (temp_css addsimps2 [Init_def] addSEs2 [DmdImplE]) + ]); + +(* If r is well-founded, state function v cannot decrease forever *) +qed_goal "wf_not_box_decrease" TLA.thy + "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v" + (fn _ => [Auto_tac(), + subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1, + etac allE 1, + dtac STL2D 1, + auto_tac (temp_css addsimps2 [Init_def]), + etac wf_dmd 1, + etac dup_boxE 1, + etac STL4E 1, + action_simp_tac (!simpset addsimps [con_abs]) [tempI] [] 1, + case_tac "sigma |= <>[][#False]_v" 1, + ALLGOALS Asm_full_simp_tac, + rewrite_goals_tac more_temp_simps, + dtac STL2D 1, + subgoal_tac "sigma |= <>(REX y. #((y, xa) : r) .& ($v .= #y))" 1, + SELECT_GOAL (auto_tac (temp_css addsimps2 [DmdAct,Init_def] + addEs2 [DmdImplE])) 1, + subgoal_tac "sigma |= (stable ($v .= #xa) .| <>(REX y. #((y, xa) : r) .& $v .= #y)`)" 1, + case_tac "sigma |= stable ($v .= #xa)" 1, + SELECT_GOAL (auto_tac (temp_css addIs2 [temp_mp DmdPrime])) 2, + SELECT_GOAL (rewrite_goals_tac ((symmetric (temp_rewrite NotBox))::action_rews)) 1, + etac swap 1, + subgoal_tac "sigma |= []($v .= #xa)" 1, + dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1, + SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1, + SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1, + auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E]) + ]); + +(* "wf ?r ==> <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *) +bind_thm("wf_not_dmd_box_decrease", + standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl))); + +(* If there are infinitely many steps where v decreases w.r.t. r, then there + have to be infinitely many non-stuttering steps where v doesn't decrease. +*) +qed_goal "wf_box_dmd_decrease" TLA.thy + "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v" + (fn [prem] => [Auto_tac(), + rtac ccontr 1, + asm_full_simp_tac + (!simpset addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1, + dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1, + dtac BoxDmdDmdBox 1, atac 1, + subgoal_tac "sigma |= []<>((#False)::action)" 1, + SELECT_GOAL (Auto_tac()) 1, + etac STL4E 1, + rtac DmdImpl 1, + auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl]) + ]); + +(* In particular, for natural numbers, if n decreases infinitely often + then it has to increase infinitely often. +*) +qed_goal "nat_box_dmd_decrease" TLA.thy + "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)" + (fn _ => [Auto_tac(), + subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1, + etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1, + SELECT_GOAL (auto_tac (!claset, !simpset addsimps [angle_def])) 1, + rtac nat_less_cases 1, + Auto_tac(), + rtac (temp_mp wf_box_dmd_decrease) 1, + auto_tac (!claset addSEs [STL4E] addSIs [DmdImpl], !simpset) + ]); + +(* ------------------------------------------------------------------------- *) +(*** Flexible quantification over state variables ***) +(* ------------------------------------------------------------------------- *) +section "Flexible quantification"; + +qed_goal "aallI" TLA.thy + "(!!x. base_var x ==> sigma |= F x) ==> sigma |= (AALL x. F(x))" + (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] addSDs2 prems)]); + +qed_goal "aallE" TLA.thy + "[| sigma |= (AALL x. F(x)); (!!sigma. sigma |= F(x) ==> P sigma) |] \ +\ ==> (P sigma)::bool" + (fn prems => [cut_facts_tac prems 1, + resolve_tac prems 1, + rewrite_goals_tac (aall_def::intensional_rews), + etac swap 1, + auto_tac (temp_css addSIs2 [temp_mp eexI]) + ]); + +(* monotonicity of quantification *) +qed_goal "eex_mono" TLA.thy + "[| sigma |= EEX x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= EEX x. G(x)" + (fn [min,maj] => [cut_facts_tac [min] 1, + etac eexE 1, + REPEAT (ares_tac (map temp_mp [eexI,maj]) 1) + ]); + +qed_goal "aall_mono" TLA.thy + "[| sigma |= AALL x. F(x); !!x. F(x) .-> G(x) |] ==> sigma |= AALL x. G(x)" + (fn [min,maj] => [cut_facts_tac [min] 1, + fast_tac (temp_cs addSIs [aallI, temp_mp maj] + addEs [aallE]) 1 + ]); + +(* ---------------------------------------------------------------------- + example of a history variable: existence of a clock + +goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))"; +br tempI 1; +br historyI 1; +bws action_rews; +by (TRYALL (rtac impI)); +by (TRYALL (etac conjE)); +ba 3; +by (Asm_full_simp_tac 3); +by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue])); +(** solved **) + +---------------------------------------------------------------------- *) diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/TLA.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/TLA.thy Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,85 @@ +(* + File: TLA/TLA.thy + Author: Stephan Merz + Copyright: 1997 University of Munich + + Theory Name: TLA + Logic Image: HOL + +The temporal level of TLA. +*) + +TLA = Action + WF_Rel + + +types + behavior + temporal = "behavior form" + +arities + behavior :: world + +consts + (* get first 2 states of behavior *) + fst_st :: "behavior => state" + snd_st :: "behavior => state" + + Init :: "action => temporal" + (* define Box and Dmd for both actions and temporals *) + Box :: "('w::world) form => temporal" ("([](_))" [40] 40) + Dmd :: "('w::world) form => temporal" ("(<>(_))" [40] 40) + "~>" :: "[action,action] => temporal" (infixr 22) + stable :: "action => temporal" + WF :: "[action,'a stfun] => temporal" ("(WF'(_')'_(_))" [0,60] 55) + SF :: "[action,'a stfun] => temporal" ("(SF'(_')'_(_))" [0,60] 55) + + (* Quantification over (flexible) state variables *) + EEx :: "('a stfun => temporal) => temporal" (binder "EEX " 10) + AAll :: "('a stfun => temporal) => temporal" (binder "AALL " 10) + +translations + "sigma |= Init(A)" == "Init A sigma" + "sigma |= Box(F)" == "Box F sigma" + "sigma |= Dmd(F)" == "Dmd F sigma" + "sigma |= F ~> G" == "op ~> F G sigma" + "sigma |= stable(A)" == "stable A sigma" + "sigma |= WF(A)_v" == "WF A v sigma" + "sigma |= SF(A)_v" == "SF A v sigma" + +rules + dmd_def "(<>F) == .~[].~F" + boxact_def "([](F::action)) == ([] Init F)" + leadsto "P ~> Q == [](Init(P) .-> <>Q)" + stable_def "stable P == [](P .-> P`)" + + WF_def "WF(A)_v == <>[] $(Enabled(_v)) .-> []<>_v" + SF_def "SF(A)_v == []<> $(Enabled(_v)) .-> []<>_v" + + Init_def "(sigma |= Init(F)) == ([[fst_st sigma, snd_st sigma]] |= F)" + +(* The following axioms are written "polymorphically", not just for temporal formulas. *) + normalT "[](F .-> G) .-> ([]F .-> []G)" + reflT "[]F .-> F" (* F::temporal *) + transT "[]F .-> [][]F" + linT "(<>F) .& (<>G) .-> (<>(F .& <>G)) .| (<>(G .& <>F))" (* F,G::temporal *) + discT "[](F .-> <>(.~F .& <>F)) .-> (F .-> []<>F)" + primeI "[]P .-> Init(P`)" + primeE "[](Init(P) .-> []F) .-> Init(P`) .-> (F .-> []F)" + indT "[](Init(P) .& .~[]F .-> Init(P`) .& F) .-> Init(P) .-> []F" + allT "(RALL x. [](F(x))) .= ([](RALL x. F(x)))" + + necT "F ==> []F" + +(* Flexible quantification: refinement mappings, history variables *) + aall_def "(AALL x. F(x)) == .~ (EEX x. .~ F(x))" + eexI "F x .-> (EEX x. F x)" + historyI "[| sigma |= Init(I); sigma |= []N; + (!!h s t. (h s = ha s t) & I [[s,t]] --> HI(h)[[s,t]]); + (!!h s t. (h t = hc s t (h s)) & N [[s,t]] --> HN(h) [[s,t]]) + |] ==> sigma |= (EEX h. Init(HI(h)) .& []HN(h))" + eexE "[| sigma |= (EEX x. F x); + (!!x. [| base_var x; (sigma |= F x) |] ==> (G sigma)::bool) + |] ==> G sigma" + +end + +ML diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/cladata.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/cladata.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,56 @@ +(* Title: TLA/cladata.ML + Author: Stephan Merz (mostly stolen from Isabelle/HOL) + +Setting up the classical reasoner for TLA. + +The classical prover for TLA uses a different hyp_subst_tac that substitutes +somewhat more liberally for state variables. Unfortunately, this requires +either generating a new prover or redefining the basic proof tactics. +We take the latter approach, because otherwise there would be a type conflict +between standard HOL and TLA classical sets, and we would have to redefine +even more things (e.g., blast_tac), and try to keep track of which rules +have been active in setting up a new default claset. + +*) + + +(* Generate a different hyp_subst_tac + that substitutes for x(s) if s is a bound variable of "world" type. + This is useful to solve equations that contain state variables. +*) + +use "hypsubst.ML"; (* local version! *) + +structure ActHypsubst_Data = + struct + structure Simplifier = Simplifier + (*Take apart an equality judgement; otherwise raise Match!*) + fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u); + val eq_reflection = eq_reflection + val imp_intr = impI + val rev_mp = rev_mp + val subst = subst + val sym = sym + end; + +structure ActHypsubst = ActHypsubstFun(ActHypsubst_Data); +open ActHypsubst; + + +(** + Define the basic classical set and clasimpset for the action part of TLA. + Add the new hyp_subst_tac to the wrapper (also for the default claset). +**) + +val action_cs = (HOL_cs addSIs [actionI,intI] addSEs [exE_prop] addDs [actionD,intD] + addss !simpset) + addSaltern action_hyp_subst_tac; +val action_css = (action_cs, !simpset); + + +AddSIs [actionI,intI]; +AddDs [actionD,intD]; +Addss (!simpset); + + + diff -r f371115aed37 -r 82a99b090d9d src/HOL/TLA/hypsubst.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TLA/hypsubst.ML Wed Oct 08 11:50:33 1997 +0200 @@ -0,0 +1,236 @@ +(* Title: ~/projects/isabelle/TLA/hypsubst.ML + Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson + Copyright 1995 University of Cambridge + +Tactic to substitute using the assumption x=t in the rest of the subgoal, +and to delete that assumption. Original version due to Martin Coen. + +This version uses the simplifier, and requires it to be already present. + +Local changes for TLA (Stephan Merz): + Simplify equations like f(x) = g(y) if x,y are bound variables. + This is useful for TLA if f and g are state variables. f and g may be + free or bound variables, or even constants. (This may be unsafe, but + we do some type checking to restrict this to state variables!) + + + +Test data: + +goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; +goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; +goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a"; +goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a"; + +by (hyp_subst_tac 1); +by (bound_hyp_subst_tac 1); + +Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) +goal thy "P(a) --> (EX y. a=y --> P(f(a)))"; +*) + +(*** Signatures unchanged (but renamed) from the original hypsubst.ML ***) + +signature ACTHYPSUBST_DATA = + sig + structure Simplifier : SIMPLIFIER + val dest_eq : term -> term*term + val eq_reflection : thm (* a=b ==> a==b *) + val imp_intr : thm (* (P ==> Q) ==> P-->Q *) + val rev_mp : thm (* [| P; P-->Q |] ==> Q *) + val subst : thm (* [| a=b; P(a) |] ==> P(b) *) + val sym : thm (* a=b ==> b=a *) + end; + + +signature ACTHYPSUBST = + sig + val action_bound_hyp_subst_tac : int -> tactic + val action_hyp_subst_tac : int -> tactic + (*exported purely for debugging purposes*) + val gen_hyp_subst_tac : bool -> int -> tactic + val vars_gen_hyp_subst_tac : bool -> int -> tactic + val eq_var : bool -> bool -> term -> int * bool + val inspect_pair : bool -> bool -> term * term -> bool + val mk_eqs : thm -> thm list + val thin_leading_eqs_tac : bool -> int -> int -> tactic + end; + + +functor ActHypsubstFun(Data: ACTHYPSUBST_DATA): ACTHYPSUBST = +struct + +fun STATE tacfun st = tacfun st st; + + +local open Data in + +exception EQ_VAR; + +fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); + +local val odot = ord"." +in +(*Simplifier turns Bound variables to dotted Free variables: + change it back (any Bound variable will do) +*) +fun contract t = + case Pattern.eta_contract t of + Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) + | Free at $ Free(b,T) => Free at $ + (if ord b = odot then Bound 0 else Free(b,T)) + | t' => t' +end; + +fun has_vars t = maxidx_of_term t <> ~1; + +(* Added for TLA version. + Is type ty the type of a state variable? Only then do we substitute + in applications. This function either returns true or raises Match. +*) +fun is_stvar (Type("fun", Type("state",[])::_)) = true; + + +(*If novars then we forbid Vars in the equality. + If bnd then we only look for Bound (or dotted Free) variables to eliminate. + When can we safely delete the equality? + Not if it equates two constants; consider 0=1. + Not if it resembles x=t[x], since substitution does not eliminate x. + Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) + Not if it involves a variable free in the premises, + but we can't check for this -- hence bnd and bound_hyp_subst_tac + Prefer to eliminate Bound variables if possible. + Result: true = use as is, false = reorient first *) +fun inspect_pair bnd novars (t,u) = + case (contract t, contract u) of + (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u + then raise Match + else true (*eliminates t*) + | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t + then raise Match + else false (*eliminates u*) + | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse + novars andalso has_vars u + then raise Match + else true (*eliminates t*) + | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse + novars andalso has_vars t + then raise Match + else false (*eliminates u*) + | (Free(_,ty) $ (Bound _), _) => + if bnd orelse + novars andalso has_vars u + then raise Match + else is_stvar(ty) (* changed for TLA *) + | (_, Free(_,ty) $ (Bound _)) => + if bnd orelse + novars andalso has_vars t + then raise Match + else not(is_stvar(ty)) (* changed for TLA *) + | ((Bound _) $ (Bound _), _) => (* can't check for types here *) + if bnd orelse + novars andalso has_vars u + then raise Match + else true + | (_, (Bound _) $ (Bound _)) => (* can't check for types here *) + if bnd orelse + novars andalso has_vars t + then raise Match + else false + | (Const(_,ty) $ (Bound _), _) => + if bnd orelse + novars andalso has_vars u + then raise Match + else is_stvar(ty) (* changed for TLA *) + | (_, Const(_,ty) $ (Bound _)) => + if bnd orelse + novars andalso has_vars t + then raise Match + else not(is_stvar(ty)) (* changed for TLA *) + | _ => raise Match; + +(*Locates a substitutable variable on the left (resp. right) of an equality + assumption. Returns the number of intervening assumptions. *) +fun eq_var bnd novars = + let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t + | eq_var_aux k (Const("==>",_) $ A $ B) = + ((k, inspect_pair bnd novars (dest_eq A)) + (*Exception comes from inspect_pair or dest_eq*) + handle Match => eq_var_aux (k+1) B) + | eq_var_aux k _ = raise EQ_VAR + in eq_var_aux 0 end; + +(*We do not try to delete ALL equality assumptions at once. But + it is easy to handle several consecutive equality assumptions in a row. + Note that we have to inspect the proof state after doing the rewriting, + since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality + must NOT be deleted. Tactic must rotate or delete m assumptions. +*) +fun thin_leading_eqs_tac bnd m i = STATE(fn state => + let fun count [] = 0 + | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); + 1 + count Bs) + handle Match => 0) + val (_,_,Bi,_) = dest_state(state,i) + val j = Int.min (m, count (Logic.strip_assums_hyp Bi)) + in REPEAT_DETERM_N j (etac thin_rl i) THEN + REPEAT_DETERM_N (m-j) (etac revcut_rl i) + end); + +(*For the simpset. Adds ALL suitable equalities, even if not first! + No vars are allowed here, as simpsets are built from meta-assumptions*) +fun mk_eqs th = + [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) + then th RS Data.eq_reflection + else symmetric(th RS Data.eq_reflection) (*reorient*) ] + handle Match => []; (*Exception comes from inspect_pair or dest_eq*) + +local open Simplifier +in + + val hyp_subst_ss = empty_ss setmksimps mk_eqs + + (*Select a suitable equality assumption and substitute throughout the subgoal + Replaces only Bound variables if bnd is true*) + fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => + let val (_,_,Bi,_) = dest_state(state,i) + val n = length(Logic.strip_assums_hyp Bi) - 1 + val (k,_) = eq_var bnd true Bi + in + EVERY [REPEAT_DETERM_N k (etac revcut_rl i), + asm_full_simp_tac hyp_subst_ss i, + etac thin_rl i, + thin_leading_eqs_tac bnd (n-k) i] + end + handle THM _ => no_tac | EQ_VAR => no_tac)); + +end; + +val ssubst = standard (sym RS subst); + +(*Old version of the tactic above -- slower but the only way + to handle equalities containing Vars.*) +fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => + let val (_,_,Bi,_) = dest_state(state,i) + val n = length(Logic.strip_assums_hyp Bi) - 1 + val (k,symopt) = eq_var bnd false Bi + in + EVERY [REPEAT_DETERM_N k (etac rev_mp i), + etac revcut_rl i, + REPEAT_DETERM_N (n-k) (etac rev_mp i), + etac (if symopt then ssubst else subst) i, + REPEAT_DETERM_N n (rtac imp_intr i)] + end + handle THM _ => no_tac | EQ_VAR => no_tac)); + +(*Substitutes for Free or Bound variables*) +val action_hyp_subst_tac = + (* gen_hyp_subst_tac false ORELSE' *) vars_gen_hyp_subst_tac false; + +(*Substitutes for Bound variables only -- this is always safe*) +val action_bound_hyp_subst_tac = + (* gen_hyp_subst_tac true ORELSE' *) vars_gen_hyp_subst_tac true; + +end +end; +