--- a/src/HOL/IsaMakefile Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/IsaMakefile Wed Apr 28 13:36:31 1999 +0200
@@ -176,7 +176,7 @@
UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
- UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
+ UNITY/UNITY.ML UNITY/UNITY.thy\
UNITY/WFair.ML UNITY/WFair.thy UNITY/Lift.ML UNITY/Lift.thy\
UNITY/PPROD.ML UNITY/PPROD.thy UNITY/NSP_Bad.ML UNITY/NSP_Bad.thy
@$(ISATOOL) usedir $(OUT)/HOL UNITY
--- a/src/HOL/UNITY/Constrains.ML Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML Wed Apr 28 13:36:31 1999 +0200
@@ -7,6 +7,40 @@
*)
+(*** traces and reachable ***)
+
+Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
+by Safe_tac;
+by (etac traces.induct 2);
+by (etac reachable.induct 1);
+by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
+qed "reachable_equiv_traces";
+
+Goal "Init F <= reachable F";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_subset_reachable";
+
+Goal "Acts G <= Acts F ==> G : stable (reachable F)";
+by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
+qed "stable_reachable";
+
+
+(*The set of all reachable states is an invariant...*)
+Goal "F : invariant (reachable F)";
+by (simp_tac (simpset() addsimps [invariant_def]) 1);
+by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
+qed "invariant_reachable";
+
+(*...in fact the strongest invariant!*)
+Goal "F : invariant A ==> reachable F <= A";
+by (full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "invariant_includes_reachable";
+
+
(*** Constrains ***)
overload_1st_set "Constrains.Constrains";
--- a/src/HOL/UNITY/Constrains.thy Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy Wed Apr 28 13:36:31 1999 +0200
@@ -6,7 +6,30 @@
Safety relations: restricted to the set of reachable states.
*)
-Constrains = UNITY + Traces +
+Constrains = UNITY +
+
+consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
+
+ (*Initial states and program => (final state, reversed trace to it)...
+ Arguments MUST be curried in an inductive definition*)
+
+inductive "traces init acts"
+ intrs
+ (*Initial trace is empty*)
+ Init "s: init ==> (s,[]) : traces init acts"
+
+ Acts "[| act: acts; (s,evs) : traces init acts; (s,s'): act |]
+ ==> (s', s#evs) : traces init acts"
+
+
+consts reachable :: "'a program => 'a set"
+
+inductive "reachable F"
+ intrs
+ Init "s: Init F ==> s : reachable F"
+
+ Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
+ ==> s' : reachable F"
constdefs
--- a/src/HOL/UNITY/Reach.thy Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/UNITY/Reach.thy Wed Apr 28 13:36:31 1999 +0200
@@ -6,7 +6,7 @@
Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
*)
-Reach = FP + Traces + SubstAx +
+Reach = FP + SubstAx +
types vertex
state = "vertex=>bool"
--- a/src/HOL/UNITY/Traces.ML Tue Apr 27 15:39:43 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(* Title: HOL/UNITY/Traces
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Definitions of
- * traces: the possible execution traces
- * reachable: the set of reachable states
-
-*)
-
-
-
-(*** The abstract type of programs ***)
-
-val rep_ss = simpset() addsimps
- [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program,
- Rep_Program_inverse, Abs_Program_inverse];
-
-
-Goal "Id : Acts F";
-by (cut_inst_tac [("x", "F")] Rep_Program 1);
-by (auto_tac (claset(), rep_ss));
-qed "Id_in_Acts";
-AddIffs [Id_in_Acts];
-
-Goal "insert Id (Acts F) = Acts F";
-by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
-qed "insert_Id_Acts";
-AddIffs [insert_Id_Acts];
-
-(** Inspectors for type "program" **)
-
-Goal "Init (mk_program (init,acts)) = init";
-by (auto_tac (claset(), rep_ss));
-qed "Init_eq";
-
-Goal "Acts (mk_program (init,acts)) = insert Id acts";
-by (auto_tac (claset(), rep_ss));
-qed "Acts_eq";
-
-Addsimps [Acts_eq, Init_eq];
-
-
-(** The notation of equality for type "program" **)
-
-Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
-by (subgoals_tac ["EX x. Rep_Program F = x",
- "EX x. Rep_Program G = x"] 1);
-by (REPEAT (Blast_tac 2));
-by (Clarify_tac 1);
-by (auto_tac (claset(), rep_ss));
-by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
-by (asm_full_simp_tac rep_ss 1);
-qed "program_equalityI";
-
-val [major,minor] =
-Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
-by (rtac minor 1);
-by (auto_tac (claset(), simpset() addsimps [major]));
-qed "program_equalityE";
-
-
-(*** These rules allow "lazy" definition expansion
- They avoid expanding the full program, which is a large expression
-***)
-
-Goal "F == mk_program (init,acts) ==> Init F = init";
-by Auto_tac;
-qed "def_prg_Init";
-
-(*The program is not expanded, but its Init and Acts are*)
-val [rew] = goal thy
- "[| F == mk_program (init,acts) |] \
-\ ==> Init F = init & Acts F = insert Id acts";
-by (rewtac rew);
-by Auto_tac;
-qed "def_prg_simps";
-
-(*An action is expanded only if a pair of states is being tested against it*)
-Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
-by Auto_tac;
-qed "def_act_simp";
-
-fun simp_of_act def = def RS def_act_simp;
-
-(*A set is expanded only if an element is being tested against it*)
-Goal "A == B ==> (x : A) = (x : B)";
-by Auto_tac;
-qed "def_set_simp";
-
-fun simp_of_set def = def RS def_set_simp;
-
-
-(*** traces and reachable ***)
-
-Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
-by Safe_tac;
-by (etac traces.induct 2);
-by (etac reachable.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
-qed "reachable_equiv_traces";
--- a/src/HOL/UNITY/Traces.thy Tue Apr 27 15:39:43 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/UNITY/Traces
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Inductive definitions of
- * traces: the possible execution traces
- * reachable: the set of reachable states
-*)
-
-Traces = LessThan +
-
-consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
-
- (*Initial states and program => (final state, reversed trace to it)...
- Arguments MUST be curried in an inductive definition*)
-
-inductive "traces Init Acts"
- intrs
- (*Initial trace is empty*)
- Init "s: Init ==> (s,[]) : traces Init Acts"
-
- Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |]
- ==> (s', s#evs) : traces Init Acts"
-
-
-typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
-
-constdefs
- mk_program :: "('a set * ('a * 'a)set set) => 'a program"
- "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
-
- Init :: "'a program => 'a set"
- "Init F == (%(init, acts). init) (Rep_Program F)"
-
- Acts :: "'a program => ('a * 'a)set set"
- "Acts F == (%(init, acts). acts) (Rep_Program F)"
-
-
-consts reachable :: "'a program => 'a set"
-
-inductive "reachable F"
- intrs
- Init "s: Init F ==> s : reachable F"
-
- Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
- ==> s' : reachable F"
-
-end
--- a/src/HOL/UNITY/UNITY.ML Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML Wed Apr 28 13:36:31 1999 +0200
@@ -30,6 +30,87 @@
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
+(*** The abstract type of programs ***)
+
+val rep_ss = simpset() addsimps
+ [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program,
+ Rep_Program_inverse, Abs_Program_inverse];
+
+
+Goal "Id : Acts F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
+by (auto_tac (claset(), rep_ss));
+qed "Id_in_Acts";
+AddIffs [Id_in_Acts];
+
+Goal "insert Id (Acts F) = Acts F";
+by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
+qed "insert_Id_Acts";
+AddIffs [insert_Id_Acts];
+
+(** Inspectors for type "program" **)
+
+Goal "Init (mk_program (init,acts)) = init";
+by (auto_tac (claset(), rep_ss));
+qed "Init_eq";
+
+Goal "Acts (mk_program (init,acts)) = insert Id acts";
+by (auto_tac (claset(), rep_ss));
+qed "Acts_eq";
+
+Addsimps [Acts_eq, Init_eq];
+
+
+(** The notation of equality for type "program" **)
+
+Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+by (subgoals_tac ["EX x. Rep_Program F = x",
+ "EX x. Rep_Program G = x"] 1);
+by (REPEAT (Blast_tac 2));
+by (Clarify_tac 1);
+by (auto_tac (claset(), rep_ss));
+by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
+by (asm_full_simp_tac rep_ss 1);
+qed "program_equalityI";
+
+val [major,minor] =
+Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
+by (rtac minor 1);
+by (auto_tac (claset(), simpset() addsimps [major]));
+qed "program_equalityE";
+
+
+(*** These rules allow "lazy" definition expansion
+ They avoid expanding the full program, which is a large expression
+***)
+
+Goal "F == mk_program (init,acts) ==> Init F = init";
+by Auto_tac;
+qed "def_prg_Init";
+
+(*The program is not expanded, but its Init and Acts are*)
+val [rew] = goal thy
+ "[| F == mk_program (init,acts) |] \
+\ ==> Init F = init & Acts F = insert Id acts";
+by (rewtac rew);
+by Auto_tac;
+qed "def_prg_simps";
+
+(*An action is expanded only if a pair of states is being tested against it*)
+Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
+by Auto_tac;
+qed "def_act_simp";
+
+fun simp_of_act def = def RS def_act_simp;
+
+(*A set is expanded only if an element is being tested against it*)
+Goal "A == B ==> (x : A) = (x : B)";
+by Auto_tac;
+qed "def_set_simp";
+
+fun simp_of_set def = def RS def_set_simp;
+
+
(*** constrains ***)
overload_1st_set "UNITY.constrains";
@@ -167,14 +248,6 @@
by (Blast_tac 1);
qed "stable_constrains_Int";
-Goal "Init F <= reachable F";
-by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "Init_subset_reachable";
-
-Goal "Acts G <= Acts F ==> G : stable (reachable F)";
-by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
-qed "stable_reachable";
-
(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
@@ -190,21 +263,6 @@
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
qed "invariant_Int";
-(*The set of all reachable states is an invariant...*)
-Goal "F : invariant (reachable F)";
-by (simp_tac (simpset() addsimps [invariant_def]) 1);
-by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
-qed "invariant_reachable";
-
-(*...in fact the strongest invariant!*)
-Goal "F : invariant A ==> reachable F <= A";
-by (full_simp_tac
- (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
-by (rtac subsetI 1);
-by (etac reachable.induct 1);
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "invariant_includes_reachable";
-
(*** increasing ***)
--- a/src/HOL/UNITY/UNITY.thy Tue Apr 27 15:39:43 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy Wed Apr 28 13:36:31 1999 +0200
@@ -8,9 +8,21 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = Traces + Prefix +
+UNITY = LessThan + Prefix +
+
+
+typedef (Program)
+ 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
constdefs
+ mk_program :: "('a set * ('a * 'a)set set) => 'a program"
+ "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+
+ Init :: "'a program => 'a set"
+ "Init F == (%(init, acts). init) (Rep_Program F)"
+
+ Acts :: "'a program => ('a * 'a)set set"
+ "Acts F == (%(init, acts). acts) (Rep_Program F)"
constrains :: "['a set, 'a set] => 'a program set"
"constrains A B == {F. ALL act: Acts F. act^^A <= B}"