# HG changeset patch # User paulson # Date 925299391 -7200 # Node ID 880f31a62784f5a2d163eb39523cc1abadb52ed6 # Parent 5a838c1d9d2fe41f00576b5f8a951868d24ab510 eliminated theory UNITY/Traces diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/IsaMakefile --- 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 diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/Constrains.ML --- 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"; diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/Constrains.thy --- 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 diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/Reach.thy --- 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" diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/Traces.ML --- 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"; diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/Traces.thy --- 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 diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/UNITY.ML --- 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 ***) diff -r 5a838c1d9d2f -r 880f31a62784 src/HOL/UNITY/UNITY.thy --- 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}"