--- a/src/ZF/IsaMakefile Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/IsaMakefile Fri Jun 27 18:40:25 2003 +0200
@@ -118,7 +118,7 @@
UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
- UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
+ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy \
UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
UNITY/AllocBase.thy UNITY/AllocImpl.thy\
UNITY/ClientImpl.thy UNITY/Distributor.thy\
--- a/src/ZF/UNITY/Comp.ML Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Comp.ML Fri Jun 27 18:40:25 2003 +0200
@@ -169,11 +169,11 @@
AddIffs [preserves_fun_pair_iff];
Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
-by (simp_tac (simpset() addsimps [fun_pair_def, comp_def]) 1);
+by (simp_tac (simpset() addsimps [fun_pair_def, metacomp_def]) 1);
qed "fun_pair_comp_distrib";
Goal "(f comp g)(x) = f(g(x))";
-by (simp_tac (simpset() addsimps [comp_def]) 1);
+by (simp_tac (simpset() addsimps [metacomp_def]) 1);
qed "comp_apply";
Addsimps [comp_apply];
--- a/src/ZF/UNITY/Distributor.thy Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Distributor.thy Fri Jun 27 18:40:25 2003 +0200
@@ -158,8 +158,9 @@
apply (auto simp add: distr_spec_def distr_follows_def)
apply (drule guaranteesD, assumption)
apply (simp_all cong add: Follows_cong
- add: refl_prefix
- mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+ add: refl_prefix
+ mono_bag_of [THEN subset_Follows_comp, THEN subsetD,
+ unfolded metacomp_def])
done
end
--- a/src/ZF/UNITY/Follows.ML Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Follows.ML Fri Jun 27 18:40:25 2003 +0200
@@ -13,7 +13,7 @@
by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
qed "Follows_cong";
-Goalw [mono1_def, comp_def]
+Goalw [mono1_def, metacomp_def]
"[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
\ Always({x:state. <f(x), g(x)>:r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
by (auto_tac (claset(), simpset() addsimps
@@ -40,7 +40,7 @@
(* comp LeadsTo *)
-Goalw [mono1_def, comp_def]
+Goalw [mono1_def, metacomp_def]
"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
\ ALL x:state. f(x):A & g(x):A |] ==> \
\ (INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}) <= \
--- a/src/ZF/UNITY/Increasing.ML Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Increasing.ML Fri Jun 27 18:40:25 2003 +0200
@@ -37,7 +37,7 @@
Addsimps [increasing_constant];
Goalw [increasing_def, stable_def, part_order_def,
- constrains_def, mono1_def, comp_def]
+ constrains_def, mono1_def, metacomp_def]
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
\ increasing[A](r, f) <= increasing[B](s, g comp f)";
by (Clarify_tac 1);
@@ -113,7 +113,7 @@
Addsimps [Increasing_constant];
Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def,
- constrains_def, mono1_def, comp_def]
+ constrains_def, mono1_def, metacomp_def]
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
\ Increasing[A](r, f) <= Increasing[B](s, g comp f)";
by Safe_tac;
--- a/src/ZF/UNITY/Merge.thy Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy Fri Jun 27 18:40:25 2003 +0200
@@ -183,8 +183,9 @@
apply (drule guaranteesD, assumption)
apply (simp add: merge_spec_def merge_follows_def, blast)
apply (simp cong add: Follows_cong
- add: refl_prefix
- mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+ add: refl_prefix
+ mono_bag_of [THEN subset_Follows_comp, THEN subsetD,
+ unfolded metacomp_def])
done
end
--- a/src/ZF/UNITY/UNITY.ML Fri Jun 27 13:15:40 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,707 +0,0 @@
-(* Title: ZF/UNITY/UNITY.ML
- ID: $Id$
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-The basic UNITY theory (revised version, based upon the "co" operator)
-From Misra, "A Logic for Concurrent Programming", 1994
-
-Proofs ported from HOL
-*)
-
-(** SKIP **)
-Goalw [SKIP_def] "SKIP:program";
-by (rewrite_goal_tac [program_def, mk_program_def] 1);
-by Auto_tac;
-qed "SKIP_in_program";
-AddIffs [SKIP_in_program];
-AddTCs [SKIP_in_program];
-
-(** programify: coersion from anything to program **)
-
-Goalw [programify_def]
-"F:program ==> programify(F)=F";
-by Auto_tac;
-qed "programify_program";
-Addsimps [programify_program];
-
-Goalw [programify_def]
-"programify(F):program";
-by Auto_tac;
-qed "programify_in_program";
-AddIffs [programify_in_program];
-AddTCs [programify_in_program];
-
-(** Collapsing rules: to remove programify from expressions **)
-Goalw [programify_def]
-"programify(programify(F))=programify(F)";
-by Auto_tac;
-qed "programify_idem";
-AddIffs [programify_idem];
-
-Goal
-"Init(programify(F)) = Init(F)";
-by (simp_tac (simpset() addsimps [Init_def]) 1);
-qed "Init_programify";
-AddIffs [Init_programify];
-
-Goal
-"Acts(programify(F)) = Acts(F)";
-by (simp_tac (simpset() addsimps [Acts_def]) 1);
-qed "Acts_programify";
-AddIffs [Acts_programify];
-
-Goal
-"AllowedActs(programify(F)) = AllowedActs(F)";
-by (simp_tac (simpset() addsimps [AllowedActs_def]) 1);
-qed "AllowedActs_programify";
-AddIffs [AllowedActs_programify];
-
-(** program's inspectors **)
-
-Goal "F:program ==>id(state):RawActs(F)";
-by (auto_tac (claset(), simpset()
- addsimps [program_def, RawActs_def]));
-qed "id_in_RawActs";
-
-Goal "id(state):Acts(F)";
-by (simp_tac (simpset()
- addsimps [id_in_RawActs, Acts_def]) 1);
-qed "id_in_Acts";
-
-Goal "F:program ==>id(state):RawAllowedActs(F)";
-by (auto_tac (claset(), simpset()
- addsimps [program_def, RawAllowedActs_def]));
-qed "id_in_RawAllowedActs";
-
-Goal "id(state):AllowedActs(F)";
-by (simp_tac (simpset()
- addsimps [id_in_RawAllowedActs, AllowedActs_def]) 1);
-qed "id_in_AllowedActs";
-
-AddIffs [id_in_Acts, id_in_AllowedActs];
-AddTCs [id_in_Acts, id_in_AllowedActs];
-
-Goal "cons(id(state), Acts(F)) = Acts(F)";
-by (simp_tac (simpset() addsimps [cons_absorb]) 1);
-qed "cons_id_Acts";
-
-Goal "cons(id(state), AllowedActs(F)) = AllowedActs(F)";
-by (simp_tac (simpset() addsimps [cons_absorb]) 1);
-qed "cons_id_AllowedActs";
-
-AddIffs [cons_id_Acts, cons_id_AllowedActs];
-
-(** inspectors's types **)
-Goal
-"F:program ==> RawInit(F)<=state";
-by (auto_tac (claset(), simpset()
- addsimps [program_def, RawInit_def]));
-qed "RawInit_type";
-
-Goal
-"F:program ==> RawActs(F)<=Pow(state*state)";
-by (auto_tac (claset(), simpset()
- addsimps [program_def, RawActs_def]));
-qed "RawActs_type";
-
-Goal
-"F:program ==> RawAllowedActs(F)<=Pow(state*state)";
-by (auto_tac (claset(), simpset()
- addsimps [program_def, RawAllowedActs_def]));
-qed "RawAllowedActs_type";
-
-Goal "Init(F)<=state";
-by (simp_tac (simpset()
- addsimps [RawInit_type, Init_def]) 1);
-qed "Init_type";
-
-bind_thm("InitD", Init_type RS subsetD);
-
-Goalw [st_set_def] "st_set(Init(F))";
-by (rtac Init_type 1);
-qed "st_set_Init";
-AddIffs [st_set_Init];
-
-Goal
-"Acts(F)<=Pow(state*state)";
-by (simp_tac (simpset()
- addsimps [RawActs_type, Acts_def]) 1);
-qed "Acts_type";
-
-Goal
-"AllowedActs(F)<=Pow(state*state)";
-by (simp_tac (simpset()
- addsimps [RawAllowedActs_type, AllowedActs_def]) 1);
-qed "AllowedActs_type";
-
-(* Needed in Behaviors *)
-Goal "[| act:Acts(F); <s,s'>:act |] ==> s:state & s':state";
-by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
-qed "ActsD";
-
-Goal "[| act:AllowedActs(F); <s,s'>:act |] ==> s:state & s':state";
-by (blast_tac (claset() addDs [AllowedActs_type RS subsetD]) 1);
-qed "AllowedActsD";
-
-(** More simplification rules involving state
- and Init, Acts, and AllowedActs **)
-
-Goal "state <= Init(F) <-> Init(F)=state";
-by (cut_inst_tac [("F", "F")] Init_type 1);
-by Auto_tac;
-qed "state_subset_is_Init_iff";
-AddIffs [state_subset_is_Init_iff];
-
-Goal "Pow(state*state) <= Acts(F) <-> Acts(F)=Pow(state*state)";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by Auto_tac;
-qed "Pow_state_times_state_is_subset_Acts_iff";
-AddIffs [Pow_state_times_state_is_subset_Acts_iff];
-
-Goal "Pow(state*state) <= AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)";
-by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
-by Auto_tac;
-qed "Pow_state_times_state_is_subset_AllowedActs_iff";
-AddIffs [Pow_state_times_state_is_subset_AllowedActs_iff];
-
-(** Eliminating `Int state' from expressions **)
-Goal "Init(F) Int state = Init(F)";
-by (cut_inst_tac [("F", "F")] Init_type 1);
-by (Blast_tac 1);
-qed "Init_Int_state";
-AddIffs [Init_Int_state];
-
-Goal "state Int Init(F) = Init(F)";
-by (cut_inst_tac [("F", "F")] Init_type 1);
-by (Blast_tac 1);
-qed "state_Int_Init";
-AddIffs [state_Int_Init];
-
-Goal "Acts(F) Int Pow(state*state) = Acts(F)";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (Blast_tac 1);
-qed "Acts_Int_Pow_state_times_state";
-AddIffs [Acts_Int_Pow_state_times_state];
-
-Goal "Pow(state*state) Int Acts(F) = Acts(F)";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (Blast_tac 1);
-qed "state_times_state_Int_Acts";
-AddIffs [state_times_state_Int_Acts];
-
-Goal "AllowedActs(F) Int Pow(state*state) = AllowedActs(F)";
-by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
-by (Blast_tac 1);
-qed "AllowedActs_Int_Pow_state_times_state";
-AddIffs [AllowedActs_Int_Pow_state_times_state];
-
-Goal "Pow(state*state) Int AllowedActs(F) = AllowedActs(F)";
-by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
-by (Blast_tac 1);
-qed "state_times_state_Int_AllowedActs";
-AddIffs [state_times_state_Int_AllowedActs];
-
-(** mk_program **)
-
-Goalw [mk_program_def, program_def] "mk_program(init, acts, allowed):program";
-by Auto_tac;
-qed "mk_program_in_program";
-AddIffs [mk_program_in_program];
-AddTCs [mk_program_in_program];
-
-Goalw [RawInit_def, mk_program_def]
- "RawInit(mk_program(init, acts, allowed)) = init Int state";
-by Auto_tac;
-qed "RawInit_eq";
-AddIffs [RawInit_eq];
-
-Goalw [RawActs_def, mk_program_def]
-"RawActs(mk_program(init, acts, allowed)) = cons(id(state), acts Int Pow(state*state))";
-by Auto_tac;
-qed "RawActs_eq";
-AddIffs [RawActs_eq];
-
-Goalw [RawAllowedActs_def, mk_program_def]
-"RawAllowedActs(mk_program(init, acts, allowed)) = \
-\ cons(id(state), allowed Int Pow(state*state))";
-by Auto_tac;
-qed "RawAllowedActs_eq";
-AddIffs [RawAllowedActs_eq];
-
-Goalw [Init_def] "Init(mk_program(init, acts, allowed)) = init Int state";
-by (Simp_tac 1);
-qed "Init_eq";
-AddIffs [Init_eq];
-
-Goalw [Acts_def]
-"Acts(mk_program(init, acts, allowed)) = cons(id(state), acts Int Pow(state*state))";
-by (Simp_tac 1);
-qed "Acts_eq";
-AddIffs [Acts_eq];
-
-Goalw [AllowedActs_def]
-"AllowedActs(mk_program(init, acts, allowed))= \
-\ cons(id(state), allowed Int Pow(state*state))";
-by (Simp_tac 1);
-qed "AllowedActs_eq";
-AddIffs [AllowedActs_eq];
-
-(**Init, Acts, and AlowedActs of SKIP **)
-
-Goalw [SKIP_def] "RawInit(SKIP) = state";
-by Auto_tac;
-qed "RawInit_SKIP";
-AddIffs [RawInit_SKIP];
-
-Goalw [SKIP_def] "RawAllowedActs(SKIP) = Pow(state*state)";
-by Auto_tac;
-qed "RawAllowedActs_SKIP";
-AddIffs [RawAllowedActs_SKIP];
-
-Goalw [SKIP_def] "RawActs(SKIP) = {id(state)}";
-by Auto_tac;
-qed "RawActs_SKIP";
-AddIffs [RawActs_SKIP];
-
-Goalw [Init_def] "Init(SKIP) = state";
-by Auto_tac;
-qed "Init_SKIP";
-AddIffs [Init_SKIP];
-
-Goalw [Acts_def] "Acts(SKIP) = {id(state)}";
-by Auto_tac;
-qed "Acts_SKIP";
-AddIffs [Acts_SKIP];
-
-Goalw [AllowedActs_def] "AllowedActs(SKIP) = Pow(state*state)";
-by Auto_tac;
-qed "AllowedActs_SKIP";
-AddIffs [AllowedActs_SKIP];
-
-(** Equality of UNITY programs **)
-
-Goal
-"F:program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F";
-by (rewrite_goal_tac [program_def, mk_program_def,RawInit_def,
- RawActs_def, RawAllowedActs_def] 1);
-by Auto_tac;
-by (REPEAT(Blast_tac 1));
-qed "raw_surjective_mk_program";
-Addsimps [raw_surjective_mk_program];
-
-Goalw [Init_def, Acts_def, AllowedActs_def]
- "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)";
-by Auto_tac;
-qed "surjective_mk_program";
-AddIffs [surjective_mk_program];
-
-Goal "[|Init(F) = Init(G); Acts(F) = Acts(G); \
-\ AllowedActs(F) = AllowedActs(G); F:program; G:program |] ==> F = G";
-by (stac (programify_program RS sym) 1);
-by (rtac sym 2);
-by (stac (programify_program RS sym) 2);
-by (stac (surjective_mk_program RS sym) 3);
-by (stac (surjective_mk_program RS sym) 3);
-by (ALLGOALS(Asm_simp_tac));
-qed "program_equalityI";
-
-val [major,minor] =
-Goal "[| F = G; \
-\ [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]\
-\ ==> P |] ==> P";
-by (rtac minor 1);
-by (auto_tac (claset(), simpset() addsimps [major]));
-qed "program_equalityE";
-
-
-Goal "[| F:program; G:program |] ==>(F=G) <-> \
-\ (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))";
-by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
-qed "program_equality_iff";
-
-(*** These rules allow "lazy" definition expansion
-
-...skipping 1 line
-
-***)
-
-Goal "F == mk_program (init,acts,allowed) ==> Init(F) = init Int state";
-by Auto_tac;
-qed "def_prg_Init";
-
-
-Goal "F == mk_program (init,acts,allowed) ==> \
-\ Acts(F) = cons(id(state), acts Int Pow(state*state))";
-by Auto_tac;
-qed "def_prg_Acts";
-
-
-Goal "F == mk_program (init,acts,allowed) ==> \
-\ AllowedActs(F) = cons(id(state), allowed Int Pow(state*state))";
-by Auto_tac;
-qed "def_prg_AllowedActs";
-
-
-val [rew] = goal thy
- "[| F == mk_program (init,acts,allowed) |] \
-\ ==> Init(F) = init Int state & Acts(F) = cons(id(state), acts Int Pow(state*state)) & \
-\ AllowedActs(F) = cons(id(state), allowed Int Pow(state*state)) ";
-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'>:A*B. P(s, s')} |] ==> \
-\ (<s,s'>:act) <-> (<s,s'>:A*B & 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;
-
-(*** co ***)
-
-Goalw [constrains_def]
-"A co B <= program";
-by Auto_tac;
-qed "constrains_type";
-
-
-val prems = Goalw [constrains_def]
- "[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A|] ==> s':A'); \
- \ F:program; st_set(A) |] ==> F:A co A'";
-by (auto_tac (claset() delrules [subsetI], simpset()));
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems)));
-by (Clarify_tac 1);
-by (blast_tac(claset() addIs prems) 1);
-qed "constrainsI";
-
-Goalw [constrains_def]
- "F:A co B ==> ALL act:Acts(F). act``A<=B";
-by (Blast_tac 1);
-qed "constrainsD";
-
-Goalw [constrains_def]
- "F:A co B ==> F:program & st_set(A)";
-by (Blast_tac 1);
-qed "constrainsD2";
-
-Goalw [constrains_def, st_set_def] "F : 0 co B <-> F:program";
-by (Blast_tac 1);
-qed "constrains_empty";
-
-Goalw [constrains_def, st_set_def]
- "(F : A co 0) <-> (A=0 & F:program)";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by Auto_tac;
-by (Blast_tac 1);
-qed "constrains_empty2";
-
-Goalw [constrains_def, st_set_def]
-"(F: state co B) <-> (state<=B & F:program)";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (Blast_tac 1);
-qed "constrains_state";
-
-Goalw [constrains_def, st_set_def] "F:A co state <-> (F:program & st_set(A))";
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (Blast_tac 1);
-qed "constrains_state2";
-
-AddIffs [constrains_empty, constrains_empty2,
- constrains_state, constrains_state2];
-
-(*monotonic in 2nd argument*)
-Goalw [constrains_def]
- "[| F:A co A'; A'<=B' |] ==> F : A co B'";
-by (Blast_tac 1);
-qed "constrains_weaken_R";
-
-(*anti-monotonic in 1st argument*)
-Goalw [constrains_def, st_set_def]
- "[| F : A co A'; B<=A |] ==> F : B co A'";
-by (Blast_tac 1);
-qed "constrains_weaken_L";
-
-Goal
- "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
-by (dtac constrains_weaken_R 1);
-by (dtac constrains_weaken_L 2);
-by (REPEAT(Blast_tac 1));
-qed "constrains_weaken";
-
-(** Union **)
-
-Goalw [constrains_def, st_set_def]
- "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')";
-by Auto_tac;
-by (Force_tac 1);
-qed "constrains_Un";
-
-val major::minor::_ = Goalw [constrains_def, st_set_def]
-"[|(!!i. i:I ==> F:A(i) co A'(i)); F:program |]==> F:(UN i:I. A(i)) co (UN i:I. A'(i))";
-by (cut_facts_tac [minor] 1);
-by Safe_tac;
-by (ALLGOALS(ftac major ));
-by (ALLGOALS(Asm_full_simp_tac));
-by (REPEAT(Blast_tac 1));
-qed "constrains_UN";
-
-Goalw [constrains_def, st_set_def]
- "(A Un B) co C = (A co C) Int (B co C)";
-by Auto_tac;
-by (Force_tac 1);
-qed "constrains_Un_distrib";
-
-Goalw [constrains_def, st_set_def]
- "i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)";
-by (rtac equalityI 1);
-by (REPEAT(Force_tac 1));
-qed "constrains_UN_distrib";
-
-(** Intersection **)
-Goalw [constrains_def, st_set_def]
- "C co (A Int B) = (C co A) Int (C co B)";
-by (rtac equalityI 1);
-by (ALLGOALS(Clarify_tac)); (* to speed up the proof *)
-by (REPEAT(Blast_tac 1));
-qed "constrains_Int_distrib";
-
-Goalw [constrains_def, st_set_def]
-"x:I ==> A co (INT i:I. B(i)) = (INT i:I. A co B(i))";
-by (rtac equalityI 1);
-by Safe_tac;
-by (REPEAT(Blast_tac 1));
-qed "constrains_INT_distrib";
-
-Goalw [constrains_def, st_set_def]
- "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')";
-by (Clarify_tac 1);
-by (Blast_tac 1);
-qed "constrains_Int";
-
-val major::minor::_ = Goalw [constrains_def, st_set_def]
-"[| (!!i. i:I==>F:A(i) co A'(i)); F:program|]==> F:(INT i:I. A(i)) co (INT i:I. A'(i))";
-by (cut_facts_tac [minor] 1);
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (case_tac "I=0" 1);
-by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
-by (etac not_emptyE 1);
-by Safe_tac;
-by (forw_inst_tac [("i", "xd")] major 1);
-by (ftac major 2);
-by (ftac major 3);
-by (REPEAT(Force_tac 1));
-qed "constrains_INT";
-
-(* The rule below simulates the HOL's one for (INT z. A i) co (INT z. B i) *)
-Goalw [constrains_def]
-"[| ALL z. F:{s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |]==>\
-\ F:{s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}";
-by (Blast_tac 1);
-qed "constrains_All";
-
-Goalw [constrains_def, st_set_def]
- "[| F:A co A' |] ==> A <= A'";
-by (Force_tac 1);
-qed "constrains_imp_subset";
-
-(*The reasoning is by subsets since "co" refers to single actions
- only. So this rule isn't that useful.*)
-
-Goalw [constrains_def, st_set_def]
- "[| F : A co B; F : B co C |] ==> F : A co C";
-by Auto_tac;
-by (Blast_tac 1);
-qed "constrains_trans";
-
-Goal
-"[| F : A co (A' Un B); F : B co B' |] ==> F:A co (A' Un B')";
-by (dres_inst_tac [("A", "B")] constrains_imp_subset 1);
-by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
-qed "constrains_cancel";
-
-(*** unless ***)
-
-Goalw [unless_def, constrains_def]
- "A unless B <= program";
-by Auto_tac;
-qed "unless_type";
-
-Goalw [unless_def] "[| F:(A-B) co (A Un B) |] ==> F : A unless B";
-by (blast_tac (claset() addDs [constrainsD2]) 1);
-qed "unlessI";
-
-Goalw [unless_def] "F :A unless B ==> F : (A-B) co (A Un B)";
-by Auto_tac;
-qed "unlessD";
-
-(*** initially ***)
-
-Goalw [initially_def]
-"initially(A) <= program";
-by (Blast_tac 1);
-qed "initially_type";
-
-Goalw [initially_def]
-"[| F:program; Init(F)<=A |] ==> F:initially(A)";
-by (Blast_tac 1);
-qed "initiallyI";
-
-Goalw [initially_def]
-"F:initially(A) ==> Init(F)<=A";
-by (Blast_tac 1);
-qed "initiallyD";
-
-(*** stable ***)
-
-Goalw [stable_def, constrains_def]
- "stable(A)<=program";
-by (Blast_tac 1);
-qed "stable_type";
-
-Goalw [stable_def]
- "F : A co A ==> F : stable(A)";
-by (assume_tac 1);
-qed "stableI";
-
-Goalw [stable_def] "F:stable(A) ==> F : A co A";
-by (assume_tac 1);
-qed "stableD";
-
-Goalw [stable_def, constrains_def] "F:stable(A) ==> F:program & st_set(A)";
-by Auto_tac;
-qed "stableD2";
-
-Goalw [stable_def, constrains_def] "stable(state) = program";
-by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
-qed "stable_state";
-AddIffs [stable_state];
-
-Goalw [unless_def, stable_def]
- "stable(A)= A unless 0";
-by Auto_tac;
-qed "stable_unless";
-
-
-(** Union **)
-
-Goalw [stable_def]
- "[| F : stable(A); F:stable(A') |] ==> F : stable(A Un A')";
-by (blast_tac (claset() addIs [constrains_Un]) 1);
-qed "stable_Un";
-
-val [major, minor] = Goalw [stable_def]
-"[|(!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))";
-by (cut_facts_tac [minor] 1);
-by (blast_tac (claset() addIs [constrains_UN, major]) 1);
-qed "stable_UN";
-
-Goalw [stable_def]
- "[| F : stable(A); F : stable(A') |] ==> F : stable (A Int A')";
-by (blast_tac (claset() addIs [constrains_Int]) 1);
-qed "stable_Int";
-
-val [major, minor] = Goalw [stable_def]
-"[| (!!i. i:I ==> F:stable(A(i))); F:program |] ==> F : stable (INT i:I. A(i))";
-by (cut_facts_tac [minor] 1);
-by (blast_tac (claset() addIs [constrains_INT, major]) 1);
-qed "stable_INT";
-
-Goalw [stable_def]
-"[|ALL z. F:stable({s:state. P(s, z)}); F:program|]==>F:stable({s:state. ALL z. P(s, z)})";
-by (rtac constrains_All 1);
-by Auto_tac;
-qed "stable_All";
-
-Goalw [stable_def, constrains_def, st_set_def]
-"[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
-by Auto_tac;
-by (blast_tac (claset() addSDs [bspec]) 1);
-qed "stable_constrains_Un";
-
-Goalw [stable_def, constrains_def, st_set_def]
- "[| F : stable(C); F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
-by (Clarify_tac 1);
-by (Blast_tac 1);
-qed "stable_constrains_Int";
-
-(* [| F:stable(C); F :(C Int A) co A |] ==> F:stable(C Int A) *)
-bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
-
-(** invariant **)
-
-Goalw [invariant_def]
- "invariant(A) <= program";
-by (blast_tac (claset() addDs [stable_type RS subsetD]) 1);
-qed "invariant_type";
-
-Goalw [invariant_def, initially_def]
- "[| Init(F)<=A; F:stable(A) |] ==> F : invariant(A)";
-by (forward_tac [stable_type RS subsetD] 1);
-by Auto_tac;
-qed "invariantI";
-
-Goalw [invariant_def, initially_def]
-"F:invariant(A) ==> Init(F)<=A & F:stable(A)";
-by Auto_tac;
-qed "invariantD";
-
-Goalw [invariant_def]
- "F:invariant(A) ==> F:program & st_set(A)";
-by (blast_tac (claset() addDs [stableD2]) 1);
-qed "invariantD2";
-
-(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
-Goalw [invariant_def, initially_def]
- "[| F : invariant(A); F : invariant(B) |] ==> F : invariant(A Int B)";
-by (asm_full_simp_tac (simpset() addsimps [stable_Int]) 1);
-by (Blast_tac 1);
-qed "invariant_Int";
-
-(** The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder
- to use in forward proof. **)
-
-(* The general case easier to prove that le special case! *)
-Goalw [constrains_def, st_set_def]
- "[| ALL m:M. F : {s:A. x(s) = m} co B(m); F:program |] \
-\ ==> F:{s:A. x(s):M} co (UN m:M. B(m))";
-by Safe_tac;
-by Auto_tac;
-by (Blast_tac 1);
-qed "elimination";
-
-(* As above, but for the special case of A=state *)
-Goal "[| ALL m:M. F : {s:state. x(s) = m} co B(m); F:program |] \
-\ ==> F:{s:state. x(s):M} co (UN m:M. B(m))";
-by (rtac elimination 1);
-by (ALLGOALS(Clarify_tac));
-qed "eliminiation2";
-
-(** strongest_rhs **)
-
-Goalw [constrains_def, strongest_rhs_def, st_set_def]
- "[| F:program; st_set(A) |] ==> F:A co (strongest_rhs(F,A))";
-by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
-qed "constrains_strongest_rhs";
-
-Goalw [constrains_def, strongest_rhs_def, st_set_def]
-"[| F:A co B; st_set(B) |] ==> strongest_rhs(F,A) <= B";
-by Safe_tac;
-by (dtac InterD 1);
-by Auto_tac;
-qed "strongest_rhs_is_strongest";
-
-(* Used in WFair.thy *)
-Goal "A:Pow(Pow(B)) ==> Union(A):Pow(B)";
-by Auto_tac;
-qed "Union_PowI";
--- a/src/ZF/UNITY/UNITY.thy Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/UNITY.thy Fri Jun 27 18:40:25 2003 +0200
@@ -9,75 +9,698 @@
Theory ported from HOL.
*)
-UNITY = State +
+header {*The Basic UNITY Theory*}
+
+theory UNITY = State:
consts
constrains :: "[i, i] => i" (infixl "co" 60)
op_unless :: "[i, i] => i" (infixl "unless" 60)
constdefs
- program :: i
+ program :: i
"program == {<init, acts, allowed>:
- Pow(state)*Pow(Pow(state*state))*Pow(Pow(state*state)).
- id(state):acts & id(state):allowed}"
+ Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
+ id(state) \<in> acts & id(state) \<in> allowed}"
- (* The definition below yields a program thanks to the coercions
- init Int state, acts Int Pow(state*state), etc. *)
- mk_program :: [i,i,i]=>i
+ mk_program :: "[i,i,i]=>i"
+ --{* The definition yields a program thanks to the coercions
+ init \<inter> state, acts \<inter> Pow(state*state), etc. *}
"mk_program(init, acts, allowed) ==
- <init Int state, cons(id(state), acts Int Pow(state*state)),
- cons(id(state), allowed Int Pow(state*state))>"
+ <init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
+ cons(id(state), allowed \<inter> Pow(state*state))>"
SKIP :: i
"SKIP == mk_program(state, 0, Pow(state*state))"
(* Coercion from anything to program *)
- programify :: i=>i
- "programify(F) == if F:program then F else SKIP"
+ programify :: "i=>i"
+ "programify(F) == if F \<in> program then F else SKIP"
- RawInit :: i=>i
+ RawInit :: "i=>i"
"RawInit(F) == fst(F)"
-
- Init :: i=>i
+
+ Init :: "i=>i"
"Init(F) == RawInit(programify(F))"
- RawActs :: i=>i
+ RawActs :: "i=>i"
"RawActs(F) == cons(id(state), fst(snd(F)))"
- Acts :: i=>i
+ Acts :: "i=>i"
"Acts(F) == RawActs(programify(F))"
- RawAllowedActs :: i=>i
+ RawAllowedActs :: "i=>i"
"RawAllowedActs(F) == cons(id(state), snd(snd(F)))"
- AllowedActs :: i=>i
+ AllowedActs :: "i=>i"
"AllowedActs(F) == RawAllowedActs(programify(F))"
-
- Allowed :: i =>i
- "Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}"
+
+ Allowed :: "i =>i"
+ "Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}"
- initially :: i=>i
- "initially(A) == {F:program. Init(F)<=A}"
-
- stable :: i=>i
+ initially :: "i=>i"
+ "initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
+
+ stable :: "i=>i"
"stable(A) == A co A"
- strongest_rhs :: [i, i] => i
- "strongest_rhs(F, A) == Inter({B:Pow(state). F:A co B})"
+ strongest_rhs :: "[i, i] => i"
+ "strongest_rhs(F, A) == Inter({B \<in> Pow(state). F \<in> A co B})"
- invariant :: i => i
- "invariant(A) == initially(A) Int stable(A)"
-
+ invariant :: "i => i"
+ "invariant(A) == initially(A) \<inter> stable(A)"
+
(* meta-function composition *)
- comp :: "[i=>i, i=>i] => (i=>i)" (infixl 65)
+ metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65)
"f comp g == %x. f(g(x))"
pg_compl :: "i=>i"
"pg_compl(X)== program - X"
-
+
defs
- (* Condition `st_set(A)' makes the definition slightly stronger than the HOL one *)
- constrains_def "A co B == {F:program. (ALL act:Acts(F). act``A<=B) & st_set(A)}"
- unless_def "A unless B == (A - B) co (A Un B)"
+ constrains_def:
+ "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
+ --{* the condition @{term "st_set(A)"} makes the definition slightly
+ stronger than the HOL one *}
+
+ unless_def: "A unless B == (A - B) co (A Un B)"
+
+
+(** SKIP **)
+lemma SKIP_in_program [iff,TC]: "SKIP \<in> program"
+by (force simp add: SKIP_def program_def mk_program_def)
+
+
+subsection{*The function @{term programify}, the coercion from anything to
+ program*}
+
+lemma programify_program [simp]: "F \<in> program ==> programify(F)=F"
+by (force simp add: programify_def)
+
+lemma programify_in_program [iff,TC]: "programify(F) \<in> program"
+by (force simp add: programify_def)
+
+(** Collapsing rules: to remove programify from expressions **)
+lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
+by (force simp add: programify_def)
+
+lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"
+by (simp add: Init_def)
+
+lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"
+by (simp add: Acts_def)
+
+lemma AllowedActs_programify [simp]:
+ "AllowedActs(programify(F)) = AllowedActs(F)"
+by (simp add: AllowedActs_def)
+
+subsection{*The Inspectors for Programs*}
+
+lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)"
+by (auto simp add: program_def RawActs_def)
+
+lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)"
+by (simp add: id_in_RawActs Acts_def)
+
+lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)"
+by (auto simp add: program_def RawAllowedActs_def)
+
+lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)"
+by (simp add: id_in_RawAllowedActs AllowedActs_def)
+
+lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"
+by (simp add: cons_absorb)
+
+lemma cons_id_AllowedActs [simp]:
+ "cons(id(state), AllowedActs(F)) = AllowedActs(F)"
+by (simp add: cons_absorb)
+
+
+subsection{*Types of the Inspectors*}
+
+lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state"
+by (auto simp add: program_def RawInit_def)
+
+lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)"
+by (auto simp add: program_def RawActs_def)
+
+lemma RawAllowedActs_type:
+ "F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)"
+by (auto simp add: program_def RawAllowedActs_def)
+
+lemma Init_type: "Init(F)\<subseteq>state"
+by (simp add: RawInit_type Init_def)
+
+lemmas InitD = Init_type [THEN subsetD, standard]
+
+lemma st_set_Init [iff]: "st_set(Init(F))"
+apply (unfold st_set_def)
+apply (rule Init_type)
+done
+
+lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)"
+by (simp add: RawActs_type Acts_def)
+
+lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)"
+by (simp add: RawAllowedActs_type AllowedActs_def)
+
+(* Needed in Behaviors *)
+lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
+by (blast dest: Acts_type [THEN subsetD])
+
+lemma AllowedActsD:
+ "[| act \<in> AllowedActs(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
+by (blast dest: AllowedActs_type [THEN subsetD])
+
+subsection{*Simplification rules involving @{term state}, @{term Init},
+ @{term Acts}, and @{term AllowedActs}*}
+
+text{*But are they really needed?*}
+
+lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) <-> Init(F)=state"
+by (cut_tac F = F in Init_type, auto)
+
+lemma Pow_state_times_state_is_subset_Acts_iff [iff]:
+ "Pow(state*state) \<subseteq> Acts(F) <-> Acts(F)=Pow(state*state)"
+by (cut_tac F = F in Acts_type, auto)
+
+lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]:
+ "Pow(state*state) \<subseteq> AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)"
+by (cut_tac F = F in AllowedActs_type, auto)
+
+subsubsection{*Eliminating @{text "\<inter> state"} from expressions*}
+
+lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)"
+by (cut_tac F = F in Init_type, blast)
+
+lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)"
+by (cut_tac F = F in Init_type, blast)
+
+lemma Acts_Int_Pow_state_times_state [simp]:
+ "Acts(F) \<inter> Pow(state*state) = Acts(F)"
+by (cut_tac F = F in Acts_type, blast)
+
+lemma state_times_state_Int_Acts [simp]:
+ "Pow(state*state) \<inter> Acts(F) = Acts(F)"
+by (cut_tac F = F in Acts_type, blast)
+
+lemma AllowedActs_Int_Pow_state_times_state [simp]:
+ "AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)"
+by (cut_tac F = F in AllowedActs_type, blast)
+
+lemma state_times_state_Int_AllowedActs [simp]:
+ "Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)"
+by (cut_tac F = F in AllowedActs_type, blast)
+
+
+subsubsection{*The Opoerator @{term mk_program}*}
+
+lemma mk_program_in_program [iff,TC]:
+ "mk_program(init, acts, allowed) \<in> program"
+by (auto simp add: mk_program_def program_def)
+
+lemma RawInit_eq [simp]:
+ "RawInit(mk_program(init, acts, allowed)) = init \<inter> state"
+by (auto simp add: mk_program_def RawInit_def)
+
+lemma RawActs_eq [simp]:
+ "RawActs(mk_program(init, acts, allowed)) =
+ cons(id(state), acts \<inter> Pow(state*state))"
+by (auto simp add: mk_program_def RawActs_def)
+
+lemma RawAllowedActs_eq [simp]:
+ "RawAllowedActs(mk_program(init, acts, allowed)) =
+ cons(id(state), allowed \<inter> Pow(state*state))"
+by (auto simp add: mk_program_def RawAllowedActs_def)
+
+lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state"
+by (simp add: Init_def)
+
+lemma Acts_eq [simp]:
+ "Acts(mk_program(init, acts, allowed)) =
+ cons(id(state), acts \<inter> Pow(state*state))"
+by (simp add: Acts_def)
+
+lemma AllowedActs_eq [simp]:
+ "AllowedActs(mk_program(init, acts, allowed))=
+ cons(id(state), allowed \<inter> Pow(state*state))"
+by (simp add: AllowedActs_def)
+
+(**Init, Acts, and AlowedActs of SKIP **)
+
+lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
+by (simp add: SKIP_def)
+
+lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"
+by (force simp add: SKIP_def)
+
+lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"
+by (force simp add: SKIP_def)
+
+lemma Init_SKIP [simp]: "Init(SKIP) = state"
+by (force simp add: SKIP_def)
+
+lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"
+by (force simp add: SKIP_def)
+
+lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
+by (force simp add: SKIP_def)
+
+(** Equality of UNITY programs **)
+
+lemma raw_surjective_mk_program:
+ "F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
+apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def
+ RawAllowedActs_def, blast+)
+done
+
+lemma surjective_mk_program [simp]:
+ "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"
+by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def)
+
+lemma program_equalityI:
+ "[|Init(F) = Init(G); Acts(F) = Acts(G);
+ AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G"
+apply (subgoal_tac "programify(F) = programify(G)")
+apply simp
+apply (simp only: surjective_mk_program [symmetric])
+done
+
+lemma program_equalityE:
+ "[|F = G;
+ [|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
+ ==> P |]
+ ==> P"
+by force
+
+
+lemma program_equality_iff:
+ "[| F \<in> program; G \<in> program |] ==>(F=G) <->
+ (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"
+by (blast intro: program_equalityI program_equalityE)
+
+subsection{*These rules allow "lazy" definition expansion*}
+
+lemma def_prg_Init:
+ "F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state"
+by auto
+
+lemma def_prg_Acts:
+ "F == mk_program (init,acts,allowed)
+ ==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))"
+by auto
+
+lemma def_prg_AllowedActs:
+ "F == mk_program (init,acts,allowed)
+ ==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
+by auto
+
+lemma def_prg_simps:
+ "[| F == mk_program (init,acts,allowed) |]
+ ==> Init(F) = init \<inter> state &
+ Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) &
+ AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
+by auto
+
+
+(*An action is expanded only if a pair of states is being tested against it*)
+lemma def_act_simp:
+ "[| act == {<s,s'> \<in> A*B. P(s, s')} |]
+ ==> (<s,s'> \<in> act) <-> (<s,s'> \<in> A*B & P(s, s'))"
+by auto
+
+(*A set is expanded only if an element is being tested against it*)
+lemma def_set_simp: "A == B ==> (x \<in> A) <-> (x \<in> B)"
+by auto
+
+
+subsection{*The Constrains Operator*}
+
+lemma constrains_type: "A co B \<subseteq> program"
+by (force simp add: constrains_def)
+
+lemma constrainsI:
+ "[|(!!act s s'. [| act: Acts(F); <s,s'> \<in> act; s \<in> A|] ==> s' \<in> A');
+ F \<in> program; st_set(A) |] ==> F \<in> A co A'"
+by (force simp add: constrains_def)
+
+lemma constrainsD:
+ "F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B"
+by (force simp add: constrains_def)
+
+lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)"
+by (force simp add: constrains_def)
+
+lemma constrains_empty [iff]: "F \<in> 0 co B <-> F \<in> program"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_empty2 [iff]: "(F \<in> A co 0) <-> (A=0 & F \<in> program)"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_state [iff]: "(F \<in> state co B) <-> (state\<subseteq>B & F \<in> program)"
+apply (cut_tac F = F in Acts_type)
+apply (force simp add: constrains_def st_set_def)
+done
+
+lemma constrains_state2 [iff]: "F \<in> A co state <-> (F \<in> program & st_set(A))"
+apply (cut_tac F = F in Acts_type)
+apply (force simp add: constrains_def st_set_def)
+done
+
+(*monotonic in 2nd argument*)
+lemma constrains_weaken_R:
+ "[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'"
+apply (unfold constrains_def, blast)
+done
+
+(*anti-monotonic in 1st argument*)
+lemma constrains_weaken_L:
+ "[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'"
+apply (unfold constrains_def st_set_def, blast)
+done
+
+lemma constrains_weaken:
+ "[| F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' |] ==> F \<in> B co B'"
+apply (drule constrains_weaken_R)
+apply (drule_tac [2] constrains_weaken_L, blast+)
+done
+
+
+subsection{*Constrains and Union*}
+
+lemma constrains_Un:
+ "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A Un B) co (A' Un B')"
+by (auto simp add: constrains_def st_set_def, force)
+
+lemma constrains_UN:
+ "[|!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program |]
+ ==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_Un_distrib:
+ "(A Un B) co C = (A co C) \<inter> (B co C)"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_UN_distrib:
+ "i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)"
+by (force simp add: constrains_def st_set_def)
+
+
+subsection{*Constrains and Intersection*}
+
+lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_INT_distrib:
+ "x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_Int:
+ "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
+by (force simp add: constrains_def st_set_def)
+
+lemma constrains_INT [rule_format]:
+ "[| \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program|]
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))"
+apply (case_tac "I=0")
+ apply (simp add: Inter_def)
+apply (erule not_emptyE)
+apply (auto simp add: constrains_def st_set_def, blast)
+apply (drule bspec, assumption, force)
+done
+
+(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *)
+lemma constrains_All:
+"[| \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program |]==>
+ F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}"
+by (unfold constrains_def, blast)
+
+lemma constrains_imp_subset:
+ "[| F \<in> A co A' |] ==> A \<subseteq> A'"
+by (unfold constrains_def st_set_def, force)
+
+(*The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.*)
+
+lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
+by (unfold constrains_def st_set_def, auto, blast)
+
+lemma constrains_cancel:
+"[| F \<in> A co (A' Un B); F \<in> B co B' |] ==> F \<in> A co (A' Un B')"
+apply (drule_tac A = B in constrains_imp_subset)
+apply (blast intro: constrains_weaken_R)
+done
+
+
+subsection{*The Unless Operator*}
+
+lemma unless_type: "A unless B \<subseteq> program"
+by (force simp add: unless_def constrains_def)
+
+lemma unlessI: "[| F \<in> (A-B) co (A Un B) |] ==> F \<in> A unless B"
+apply (unfold unless_def)
+apply (blast dest: constrainsD2)
+done
+
+lemma unlessD: "F :A unless B ==> F \<in> (A-B) co (A Un B)"
+by (unfold unless_def, auto)
+
+
+subsection{*The Operator @{term initially}*}
+
+lemma initially_type: "initially(A) \<subseteq> program"
+by (unfold initially_def, blast)
+
+lemma initiallyI: "[| F \<in> program; Init(F)\<subseteq>A |] ==> F \<in> initially(A)"
+by (unfold initially_def, blast)
+
+lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A"
+by (unfold initially_def, blast)
+
+
+subsection{*The Operator @{term stable}*}
+
+lemma stable_type: "stable(A)\<subseteq>program"
+by (unfold stable_def constrains_def, blast)
+
+lemma stableI: "F \<in> A co A ==> F \<in> stable(A)"
+by (unfold stable_def, assumption)
+
+lemma stableD: "F \<in> stable(A) ==> F \<in> A co A"
+by (unfold stable_def, assumption)
+
+lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)"
+by (unfold stable_def constrains_def, auto)
+
+lemma stable_state [simp]: "stable(state) = program"
+by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD])
+
+
+lemma stable_unless: "stable(A)= A unless 0"
+by (auto simp add: unless_def stable_def)
+
+
+subsection{*Union and Intersection with @{term stable}*}
+
+lemma stable_Un:
+ "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable(A Un A')"
+apply (unfold stable_def)
+apply (blast intro: constrains_Un)
+done
+
+lemma stable_UN:
+ "[|!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program |]
+ ==> F \<in> stable (\<Union>i \<in> I. A(i))"
+apply (unfold stable_def)
+apply (blast intro: constrains_UN)
+done
+
+lemma stable_Int:
+ "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable (A \<inter> A')"
+apply (unfold stable_def)
+apply (blast intro: constrains_Int)
+done
+
+lemma stable_INT:
+ "[| !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program |]
+ ==> F \<in> stable (\<Inter>i \<in> I. A(i))"
+apply (unfold stable_def)
+apply (blast intro: constrains_INT)
+done
+
+lemma stable_All:
+ "[|\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program|]
+ ==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
+apply (unfold stable_def)
+apply (rule constrains_All, auto)
+done
+
+lemma stable_constrains_Un:
+ "[| F \<in> stable(C); F \<in> A co (C Un A') |] ==> F \<in> (C Un A) co (C Un A')"
+apply (unfold stable_def constrains_def st_set_def, auto)
+apply (blast dest!: bspec)
+done
+
+lemma stable_constrains_Int:
+ "[| F \<in> stable(C); F \<in> (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
+by (unfold stable_def constrains_def st_set_def, blast)
+
+(* [| F \<in> stable(C); F \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *)
+lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
+
+subsection{*The Operator @{term invariant}*}
+
+lemma invariant_type: "invariant(A) \<subseteq> program"
+apply (unfold invariant_def)
+apply (blast dest: stable_type [THEN subsetD])
+done
+
+lemma invariantI: "[| Init(F)\<subseteq>A; F \<in> stable(A) |] ==> F \<in> invariant(A)"
+apply (unfold invariant_def initially_def)
+apply (frule stable_type [THEN subsetD], auto)
+done
+
+lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)"
+by (unfold invariant_def initially_def, auto)
+
+lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)"
+apply (unfold invariant_def)
+apply (blast dest: stableD2)
+done
+
+text{*Could also say
+ @{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}*}
+lemma invariant_Int:
+ "[| F \<in> invariant(A); F \<in> invariant(B) |] ==> F \<in> invariant(A \<inter> B)"
+apply (unfold invariant_def initially_def)
+apply (simp add: stable_Int, blast)
+done
+
+
+subsection{*The Elimination Theorem*}
+
+(** The "free" m has become universally quantified!
+ Should the premise be !!m instead of \<forall>m ? Would make it harder
+ to use in forward proof. **)
+
+(* The general case easier to prove that le special case! *)
+lemma "elimination":
+ "[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program |]
+ ==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
+by (auto simp add: constrains_def st_set_def, blast)
+
+(* As above, but for the special case of A=state *)
+lemma elimination2:
+ "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program |]
+ ==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
+by (rule UNITY.elimination, auto)
+
+subsection{*The Operator @{term strongest_rhs}*}
+
+lemma constrains_strongest_rhs:
+ "[| F \<in> program; st_set(A) |] ==> F \<in> A co (strongest_rhs(F,A))"
+by (auto simp add: constrains_def strongest_rhs_def st_set_def
+ dest: Acts_type [THEN subsetD])
+
+lemma strongest_rhs_is_strongest:
+ "[| F \<in> A co B; st_set(B) |] ==> strongest_rhs(F,A) \<subseteq> B"
+by (auto simp add: constrains_def strongest_rhs_def st_set_def)
+
+ML
+{*
+val constrains_def = thm "constrains_def";
+val stable_def = thm "stable_def";
+val invariant_def = thm "invariant_def";
+val unless_def = thm "unless_def";
+val initially_def = thm "initially_def";
+val SKIP_def = thm "SKIP_def";
+val Allowed_def = thm "Allowed_def";
+val programify_def = thm "programify_def";
+val metacomp_def = thm "metacomp_def";
+
+val id_in_Acts = thm "id_in_Acts";
+val id_in_RawAllowedActs = thm "id_in_RawAllowedActs";
+val id_in_AllowedActs = thm "id_in_AllowedActs";
+val cons_id_Acts = thm "cons_id_Acts";
+val cons_id_AllowedActs = thm "cons_id_AllowedActs";
+val Init_type = thm "Init_type";
+val st_set_Init = thm "st_set_Init";
+val Acts_type = thm "Acts_type";
+val AllowedActs_type = thm "AllowedActs_type";
+val ActsD = thm "ActsD";
+val AllowedActsD = thm "AllowedActsD";
+val mk_program_in_program = thm "mk_program_in_program";
+val Init_eq = thm "Init_eq";
+val Acts_eq = thm "Acts_eq";
+val AllowedActs_eq = thm "AllowedActs_eq";
+val Init_SKIP = thm "Init_SKIP";
+val Acts_SKIP = thm "Acts_SKIP";
+val AllowedActs_SKIP = thm "AllowedActs_SKIP";
+val raw_surjective_mk_program = thm "raw_surjective_mk_program";
+val surjective_mk_program = thm "surjective_mk_program";
+val program_equalityI = thm "program_equalityI";
+val program_equalityE = thm "program_equalityE";
+val program_equality_iff = thm "program_equality_iff";
+val def_prg_Init = thm "def_prg_Init";
+val def_prg_Acts = thm "def_prg_Acts";
+val def_prg_AllowedActs = thm "def_prg_AllowedActs";
+val def_prg_simps = thm "def_prg_simps";
+val def_act_simp = thm "def_act_simp";
+val def_set_simp = thm "def_set_simp";
+val constrains_type = thm "constrains_type";
+val constrainsI = thm "constrainsI";
+val constrainsD = thm "constrainsD";
+val constrainsD2 = thm "constrainsD2";
+val constrains_empty = thm "constrains_empty";
+val constrains_empty2 = thm "constrains_empty2";
+val constrains_state = thm "constrains_state";
+val constrains_state2 = thm "constrains_state2";
+val constrains_weaken_R = thm "constrains_weaken_R";
+val constrains_weaken_L = thm "constrains_weaken_L";
+val constrains_weaken = thm "constrains_weaken";
+val constrains_Un = thm "constrains_Un";
+val constrains_UN = thm "constrains_UN";
+val constrains_Un_distrib = thm "constrains_Un_distrib";
+val constrains_UN_distrib = thm "constrains_UN_distrib";
+val constrains_Int_distrib = thm "constrains_Int_distrib";
+val constrains_INT_distrib = thm "constrains_INT_distrib";
+val constrains_Int = thm "constrains_Int";
+val constrains_INT = thm "constrains_INT";
+val constrains_All = thm "constrains_All";
+val constrains_imp_subset = thm "constrains_imp_subset";
+val constrains_trans = thm "constrains_trans";
+val constrains_cancel = thm "constrains_cancel";
+val unless_type = thm "unless_type";
+val unlessI = thm "unlessI";
+val unlessD = thm "unlessD";
+val initially_type = thm "initially_type";
+val initiallyI = thm "initiallyI";
+val initiallyD = thm "initiallyD";
+val stable_type = thm "stable_type";
+val stableI = thm "stableI";
+val stableD = thm "stableD";
+val stableD2 = thm "stableD2";
+val stable_state = thm "stable_state";
+val stable_unless = thm "stable_unless";
+val stable_Un = thm "stable_Un";
+val stable_UN = thm "stable_UN";
+val stable_Int = thm "stable_Int";
+val stable_INT = thm "stable_INT";
+val stable_All = thm "stable_All";
+val stable_constrains_Un = thm "stable_constrains_Un";
+val stable_constrains_Int = thm "stable_constrains_Int";
+val invariant_type = thm "invariant_type";
+val invariantI = thm "invariantI";
+val invariantD = thm "invariantD";
+val invariantD2 = thm "invariantD2";
+val invariant_Int = thm "invariant_Int";
+val elimination = thm "elimination";
+val elimination2 = thm "elimination2";
+val constrains_strongest_rhs = thm "constrains_strongest_rhs";
+val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
+
+fun simp_of_act def = def RS def_act_simp;
+fun simp_of_set def = def RS def_set_simp;
+*}
+
end
-
--- a/src/ZF/UNITY/Union.ML Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Union.ML Fri Jun 27 18:40:25 2003 +0200
@@ -168,7 +168,9 @@
Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
-by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [INT_Int_distrib]));
+by (auto_tac (claset() addSEs [not_emptyE],
+ simpset() addsimps INT_extend_simps
+ delsimps INT_simps));
qed "Init_JN";
Goalw [JOIN_def]
@@ -496,11 +498,10 @@
qed "ok_Join_commute_I";
Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
-by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
-by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
+by (force_tac (claset() addDs [Acts_type RS subsetD] addSEs [not_emptyE],
+ simpset() addsimps [ok_def]) 1);
qed "ok_JN_iff1";
-
Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)";
by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
@@ -531,11 +532,11 @@
Goal "i:I ==> \
\ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))";
by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+by (Blast_tac 1);
qed "Allowed_JN";
Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
-Goal
-"F ok G <-> (programify(F):Allowed(programify(G)) & \
+Goal "F ok G <-> (programify(F):Allowed(programify(G)) & \
\ programify(G):Allowed(programify(F)))";
by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
qed "ok_iff_Allowed";
--- a/src/ZF/UNITY/WFair.thy Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/WFair.thy Fri Jun 27 18:40:25 2003 +0200
@@ -37,7 +37,7 @@
<Union(S),B>:leads(D, F)"
monos Pow_mono
- type_intrs "[Union_PowI, UnionI, PowI]"
+ type_intrs "[Union_Pow_iff RS iffD2, UnionI, PowI]"
constdefs
--- a/src/ZF/equalities.thy Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/equalities.thy Fri Jun 27 18:40:25 2003 +0200
@@ -922,6 +922,9 @@
lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
by blast
+lemma Union_Pow_iff: "Union(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
+by blast
+
lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
by blast
@@ -1231,6 +1234,7 @@
val UN_Pow_subset = thm "UN_Pow_subset";
val subset_Pow_Union = thm "subset_Pow_Union";
val Union_Pow_eq = thm "Union_Pow_eq";
+val Union_Pow_iff = thm "Union_Pow_iff";
val Pow_Int_eq = thm "Pow_Int_eq";
val Pow_INT_eq = thm "Pow_INT_eq";
val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";