eliminated theory UNITY/Traces
authorpaulson
Wed Apr 28 13:36:31 1999 +0200 (1999-04-28)
changeset 6535880f31a62784
parent 6534 5a838c1d9d2f
child 6536 281d44905cab
eliminated theory UNITY/Traces
src/HOL/IsaMakefile
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Apr 27 15:39:43 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Apr 28 13:36:31 1999 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4    UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
     1.5    UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
     1.6    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
     1.7 -  UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
     1.8 +  UNITY/UNITY.ML UNITY/UNITY.thy\
     1.9    UNITY/WFair.ML UNITY/WFair.thy UNITY/Lift.ML UNITY/Lift.thy\
    1.10    UNITY/PPROD.ML UNITY/PPROD.thy UNITY/NSP_Bad.ML UNITY/NSP_Bad.thy
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL UNITY
     2.1 --- a/src/HOL/UNITY/Constrains.ML	Tue Apr 27 15:39:43 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Constrains.ML	Wed Apr 28 13:36:31 1999 +0200
     2.3 @@ -7,6 +7,40 @@
     2.4  *)
     2.5  
     2.6  
     2.7 +(*** traces and reachable ***)
     2.8 +
     2.9 +Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
    2.10 +by Safe_tac;
    2.11 +by (etac traces.induct 2);
    2.12 +by (etac reachable.induct 1);
    2.13 +by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
    2.14 +qed "reachable_equiv_traces";
    2.15 +
    2.16 +Goal "Init F <= reachable F";
    2.17 +by (blast_tac (claset() addIs reachable.intrs) 1);
    2.18 +qed "Init_subset_reachable";
    2.19 +
    2.20 +Goal "Acts G <= Acts F ==> G : stable (reachable F)";
    2.21 +by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
    2.22 +qed "stable_reachable";
    2.23 +
    2.24 +
    2.25 +(*The set of all reachable states is an invariant...*)
    2.26 +Goal "F : invariant (reachable F)";
    2.27 +by (simp_tac (simpset() addsimps [invariant_def]) 1);
    2.28 +by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
    2.29 +qed "invariant_reachable";
    2.30 +
    2.31 +(*...in fact the strongest invariant!*)
    2.32 +Goal "F : invariant A ==> reachable F <= A";
    2.33 +by (full_simp_tac 
    2.34 +    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
    2.35 +by (rtac subsetI 1);
    2.36 +by (etac reachable.induct 1);
    2.37 +by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
    2.38 +qed "invariant_includes_reachable";
    2.39 +
    2.40 +
    2.41  (*** Constrains ***)
    2.42  
    2.43  overload_1st_set "Constrains.Constrains";
     3.1 --- a/src/HOL/UNITY/Constrains.thy	Tue Apr 27 15:39:43 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Constrains.thy	Wed Apr 28 13:36:31 1999 +0200
     3.3 @@ -6,7 +6,30 @@
     3.4  Safety relations: restricted to the set of reachable states.
     3.5  *)
     3.6  
     3.7 -Constrains = UNITY + Traces + 
     3.8 +Constrains = UNITY + 
     3.9 +
    3.10 +consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    3.11 +
    3.12 +  (*Initial states and program => (final state, reversed trace to it)...
    3.13 +    Arguments MUST be curried in an inductive definition*)
    3.14 +
    3.15 +inductive "traces init acts"  
    3.16 +  intrs 
    3.17 +         (*Initial trace is empty*)
    3.18 +    Init  "s: init ==> (s,[]) : traces init acts"
    3.19 +
    3.20 +    Acts  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
    3.21 +	   ==> (s', s#evs) : traces init acts"
    3.22 +
    3.23 +
    3.24 +consts reachable :: "'a program => 'a set"
    3.25 +
    3.26 +inductive "reachable F"
    3.27 +  intrs 
    3.28 +    Init  "s: Init F ==> s : reachable F"
    3.29 +
    3.30 +    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
    3.31 +	   ==> s' : reachable F"
    3.32  
    3.33  constdefs
    3.34  
     4.1 --- a/src/HOL/UNITY/Reach.thy	Tue Apr 27 15:39:43 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Reach.thy	Wed Apr 28 13:36:31 1999 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
     4.5  *)
     4.6  
     4.7 -Reach = FP + Traces + SubstAx +
     4.8 +Reach = FP + SubstAx +
     4.9  
    4.10  types   vertex
    4.11          state = "vertex=>bool"
     5.1 --- a/src/HOL/UNITY/Traces.ML	Tue Apr 27 15:39:43 1999 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,102 +0,0 @@
     5.4 -(*  Title:      HOL/UNITY/Traces
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1998  University of Cambridge
     5.8 -
     5.9 -Definitions of
    5.10 -  * traces: the possible execution traces
    5.11 -  * reachable: the set of reachable states
    5.12 -
    5.13 -*)
    5.14 -
    5.15 -
    5.16 -
    5.17 -(*** The abstract type of programs ***)
    5.18 -
    5.19 -val rep_ss = simpset() addsimps 
    5.20 -                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
    5.21 -		 Rep_Program_inverse, Abs_Program_inverse];
    5.22 -
    5.23 -
    5.24 -Goal "Id : Acts F";
    5.25 -by (cut_inst_tac [("x", "F")] Rep_Program 1);
    5.26 -by (auto_tac (claset(), rep_ss));
    5.27 -qed "Id_in_Acts";
    5.28 -AddIffs [Id_in_Acts];
    5.29 -
    5.30 -Goal "insert Id (Acts F) = Acts F";
    5.31 -by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
    5.32 -qed "insert_Id_Acts";
    5.33 -AddIffs [insert_Id_Acts];
    5.34 -
    5.35 -(** Inspectors for type "program" **)
    5.36 -
    5.37 -Goal "Init (mk_program (init,acts)) = init";
    5.38 -by (auto_tac (claset(), rep_ss));
    5.39 -qed "Init_eq";
    5.40 -
    5.41 -Goal "Acts (mk_program (init,acts)) = insert Id acts";
    5.42 -by (auto_tac (claset(), rep_ss));
    5.43 -qed "Acts_eq";
    5.44 -
    5.45 -Addsimps [Acts_eq, Init_eq];
    5.46 -
    5.47 -
    5.48 -(** The notation of equality for type "program" **)
    5.49 -
    5.50 -Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
    5.51 -by (subgoals_tac ["EX x. Rep_Program F = x",
    5.52 -		  "EX x. Rep_Program G = x"] 1);
    5.53 -by (REPEAT (Blast_tac 2));
    5.54 -by (Clarify_tac 1);
    5.55 -by (auto_tac (claset(), rep_ss));
    5.56 -by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
    5.57 -by (asm_full_simp_tac rep_ss 1);
    5.58 -qed "program_equalityI";
    5.59 -
    5.60 -val [major,minor] =
    5.61 -Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
    5.62 -by (rtac minor 1);
    5.63 -by (auto_tac (claset(), simpset() addsimps [major]));
    5.64 -qed "program_equalityE";
    5.65 -
    5.66 -
    5.67 -(*** These rules allow "lazy" definition expansion 
    5.68 -     They avoid expanding the full program, which is a large expression
    5.69 -***)
    5.70 -
    5.71 -Goal "F == mk_program (init,acts) ==> Init F = init";
    5.72 -by Auto_tac;
    5.73 -qed "def_prg_Init";
    5.74 -
    5.75 -(*The program is not expanded, but its Init and Acts are*)
    5.76 -val [rew] = goal thy
    5.77 -    "[| F == mk_program (init,acts) |] \
    5.78 -\    ==> Init F = init & Acts F = insert Id acts";
    5.79 -by (rewtac rew);
    5.80 -by Auto_tac;
    5.81 -qed "def_prg_simps";
    5.82 -
    5.83 -(*An action is expanded only if a pair of states is being tested against it*)
    5.84 -Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
    5.85 -by Auto_tac;
    5.86 -qed "def_act_simp";
    5.87 -
    5.88 -fun simp_of_act def = def RS def_act_simp;
    5.89 -
    5.90 -(*A set is expanded only if an element is being tested against it*)
    5.91 -Goal "A == B ==> (x : A) = (x : B)";
    5.92 -by Auto_tac;
    5.93 -qed "def_set_simp";
    5.94 -
    5.95 -fun simp_of_set def = def RS def_set_simp;
    5.96 -
    5.97 -
    5.98 -(*** traces and reachable ***)
    5.99 -
   5.100 -Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
   5.101 -by Safe_tac;
   5.102 -by (etac traces.induct 2);
   5.103 -by (etac reachable.induct 1);
   5.104 -by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
   5.105 -qed "reachable_equiv_traces";
     6.1 --- a/src/HOL/UNITY/Traces.thy	Tue Apr 27 15:39:43 1999 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,50 +0,0 @@
     6.4 -(*  Title:      HOL/UNITY/Traces
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1998  University of Cambridge
     6.8 -
     6.9 -Inductive definitions of
    6.10 -  * traces: the possible execution traces
    6.11 -  * reachable: the set of reachable states
    6.12 -*)
    6.13 -
    6.14 -Traces = LessThan +
    6.15 -
    6.16 -consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    6.17 -
    6.18 -  (*Initial states and program => (final state, reversed trace to it)...
    6.19 -    Arguments MUST be curried in an inductive definition*)
    6.20 -
    6.21 -inductive "traces Init Acts"  
    6.22 -  intrs 
    6.23 -         (*Initial trace is empty*)
    6.24 -    Init  "s: Init ==> (s,[]) : traces Init Acts"
    6.25 -
    6.26 -    Acts  "[| act: Acts;  (s,evs) : traces Init Acts;  (s,s'): act |]
    6.27 -	   ==> (s', s#evs) : traces Init Acts"
    6.28 -
    6.29 -
    6.30 -typedef (Program)
    6.31 -  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    6.32 -
    6.33 -constdefs
    6.34 -    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
    6.35 -    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
    6.36 -
    6.37 -  Init :: "'a program => 'a set"
    6.38 -    "Init F == (%(init, acts). init) (Rep_Program F)"
    6.39 -
    6.40 -  Acts :: "'a program => ('a * 'a)set set"
    6.41 -    "Acts F == (%(init, acts). acts) (Rep_Program F)"
    6.42 -
    6.43 -
    6.44 -consts reachable :: "'a program => 'a set"
    6.45 -
    6.46 -inductive "reachable F"
    6.47 -  intrs 
    6.48 -    Init  "s: Init F ==> s : reachable F"
    6.49 -
    6.50 -    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
    6.51 -	   ==> s' : reachable F"
    6.52 -
    6.53 -end
     7.1 --- a/src/HOL/UNITY/UNITY.ML	Tue Apr 27 15:39:43 1999 +0200
     7.2 +++ b/src/HOL/UNITY/UNITY.ML	Wed Apr 28 13:36:31 1999 +0200
     7.3 @@ -30,6 +30,87 @@
     7.4  Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
     7.5  
     7.6  
     7.7 +(*** The abstract type of programs ***)
     7.8 +
     7.9 +val rep_ss = simpset() addsimps 
    7.10 +                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
    7.11 +		 Rep_Program_inverse, Abs_Program_inverse];
    7.12 +
    7.13 +
    7.14 +Goal "Id : Acts F";
    7.15 +by (cut_inst_tac [("x", "F")] Rep_Program 1);
    7.16 +by (auto_tac (claset(), rep_ss));
    7.17 +qed "Id_in_Acts";
    7.18 +AddIffs [Id_in_Acts];
    7.19 +
    7.20 +Goal "insert Id (Acts F) = Acts F";
    7.21 +by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
    7.22 +qed "insert_Id_Acts";
    7.23 +AddIffs [insert_Id_Acts];
    7.24 +
    7.25 +(** Inspectors for type "program" **)
    7.26 +
    7.27 +Goal "Init (mk_program (init,acts)) = init";
    7.28 +by (auto_tac (claset(), rep_ss));
    7.29 +qed "Init_eq";
    7.30 +
    7.31 +Goal "Acts (mk_program (init,acts)) = insert Id acts";
    7.32 +by (auto_tac (claset(), rep_ss));
    7.33 +qed "Acts_eq";
    7.34 +
    7.35 +Addsimps [Acts_eq, Init_eq];
    7.36 +
    7.37 +
    7.38 +(** The notation of equality for type "program" **)
    7.39 +
    7.40 +Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
    7.41 +by (subgoals_tac ["EX x. Rep_Program F = x",
    7.42 +		  "EX x. Rep_Program G = x"] 1);
    7.43 +by (REPEAT (Blast_tac 2));
    7.44 +by (Clarify_tac 1);
    7.45 +by (auto_tac (claset(), rep_ss));
    7.46 +by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
    7.47 +by (asm_full_simp_tac rep_ss 1);
    7.48 +qed "program_equalityI";
    7.49 +
    7.50 +val [major,minor] =
    7.51 +Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
    7.52 +by (rtac minor 1);
    7.53 +by (auto_tac (claset(), simpset() addsimps [major]));
    7.54 +qed "program_equalityE";
    7.55 +
    7.56 +
    7.57 +(*** These rules allow "lazy" definition expansion 
    7.58 +     They avoid expanding the full program, which is a large expression
    7.59 +***)
    7.60 +
    7.61 +Goal "F == mk_program (init,acts) ==> Init F = init";
    7.62 +by Auto_tac;
    7.63 +qed "def_prg_Init";
    7.64 +
    7.65 +(*The program is not expanded, but its Init and Acts are*)
    7.66 +val [rew] = goal thy
    7.67 +    "[| F == mk_program (init,acts) |] \
    7.68 +\    ==> Init F = init & Acts F = insert Id acts";
    7.69 +by (rewtac rew);
    7.70 +by Auto_tac;
    7.71 +qed "def_prg_simps";
    7.72 +
    7.73 +(*An action is expanded only if a pair of states is being tested against it*)
    7.74 +Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
    7.75 +by Auto_tac;
    7.76 +qed "def_act_simp";
    7.77 +
    7.78 +fun simp_of_act def = def RS def_act_simp;
    7.79 +
    7.80 +(*A set is expanded only if an element is being tested against it*)
    7.81 +Goal "A == B ==> (x : A) = (x : B)";
    7.82 +by Auto_tac;
    7.83 +qed "def_set_simp";
    7.84 +
    7.85 +fun simp_of_set def = def RS def_set_simp;
    7.86 +
    7.87 +
    7.88  (*** constrains ***)
    7.89  
    7.90  overload_1st_set "UNITY.constrains";
    7.91 @@ -167,14 +248,6 @@
    7.92  by (Blast_tac 1);
    7.93  qed "stable_constrains_Int";
    7.94  
    7.95 -Goal "Init F <= reachable F";
    7.96 -by (blast_tac (claset() addIs reachable.intrs) 1);
    7.97 -qed "Init_subset_reachable";
    7.98 -
    7.99 -Goal "Acts G <= Acts F ==> G : stable (reachable F)";
   7.100 -by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
   7.101 -qed "stable_reachable";
   7.102 -
   7.103  (*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
   7.104  bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
   7.105  
   7.106 @@ -190,21 +263,6 @@
   7.107  by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
   7.108  qed "invariant_Int";
   7.109  
   7.110 -(*The set of all reachable states is an invariant...*)
   7.111 -Goal "F : invariant (reachable F)";
   7.112 -by (simp_tac (simpset() addsimps [invariant_def]) 1);
   7.113 -by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
   7.114 -qed "invariant_reachable";
   7.115 -
   7.116 -(*...in fact the strongest invariant!*)
   7.117 -Goal "F : invariant A ==> reachable F <= A";
   7.118 -by (full_simp_tac 
   7.119 -    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
   7.120 -by (rtac subsetI 1);
   7.121 -by (etac reachable.induct 1);
   7.122 -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   7.123 -qed "invariant_includes_reachable";
   7.124 -
   7.125  
   7.126  (*** increasing ***)
   7.127  
     8.1 --- a/src/HOL/UNITY/UNITY.thy	Tue Apr 27 15:39:43 1999 +0200
     8.2 +++ b/src/HOL/UNITY/UNITY.thy	Wed Apr 28 13:36:31 1999 +0200
     8.3 @@ -8,9 +8,21 @@
     8.4  From Misra, "A Logic for Concurrent Programming", 1994
     8.5  *)
     8.6  
     8.7 -UNITY = Traces + Prefix +
     8.8 +UNITY = LessThan + Prefix +
     8.9 +
    8.10 +
    8.11 +typedef (Program)
    8.12 +  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    8.13  
    8.14  constdefs
    8.15 +    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
    8.16 +    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
    8.17 +
    8.18 +  Init :: "'a program => 'a set"
    8.19 +    "Init F == (%(init, acts). init) (Rep_Program F)"
    8.20 +
    8.21 +  Acts :: "'a program => ('a * 'a)set set"
    8.22 +    "Acts F == (%(init, acts). acts) (Rep_Program F)"
    8.23  
    8.24    constrains :: "['a set, 'a set] => 'a program set"
    8.25      "constrains A B == {F. ALL act: Acts F. act^^A <= B}"