# HG changeset patch # User paulson # Date 1056732025 -7200 # Node ID 37c964462747301c2f308cc7306d15d2650846f2 # Parent 5cfc8b9fb880d4682583d5c4007e641120acbfa3 Conversion of theory UNITY to Isar script diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/IsaMakefile --- 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\ diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Comp.ML --- 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]; diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Distributor.thy --- 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 diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Follows.ML --- 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. :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. :r} LeadsTo {s:state. :r}) <= \ diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Increasing.ML --- 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; diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Merge.thy --- 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 diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/UNITY.ML --- 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); :act |] ==> s:state & s':state"; -by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1); -qed "ActsD"; - -Goal "[| act:AllowedActs(F); :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 == {:A*B. P(s, s')} |] ==> \ -\ (:act) <-> (: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); :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"; diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/UNITY.thy --- 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 == {: - 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) \ acts & id(state) \ 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 \ state, acts \ Pow(state*state), etc. *} "mk_program(init, acts, allowed) == - " + state, cons(id(state), acts \ Pow(state*state)), + cons(id(state), allowed \ 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 \ 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 \ program. Acts(G) \ AllowedActs(F)}" - initially :: i=>i - "initially(A) == {F:program. Init(F)<=A}" - - stable :: i=>i + initially :: "i=>i" + "initially(A) == {F \ program. Init(F)\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 \ Pow(state). F \ A co B})" - invariant :: i => i - "invariant(A) == initially(A) Int stable(A)" - + invariant :: "i => i" + "invariant(A) == initially(A) \ 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 \ program. (\act \ Acts(F). act``A\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 \ 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 \ program ==> programify(F)=F" +by (force simp add: programify_def) + +lemma programify_in_program [iff,TC]: "programify(F) \ 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 \ program ==>id(state) \ RawActs(F)" +by (auto simp add: program_def RawActs_def) + +lemma id_in_Acts [iff,TC]: "id(state) \ Acts(F)" +by (simp add: id_in_RawActs Acts_def) + +lemma id_in_RawAllowedActs: "F \ program ==>id(state) \ RawAllowedActs(F)" +by (auto simp add: program_def RawAllowedActs_def) + +lemma id_in_AllowedActs [iff,TC]: "id(state) \ 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 \ program ==> RawInit(F)\state" +by (auto simp add: program_def RawInit_def) + +lemma RawActs_type: "F \ program ==> RawActs(F)\Pow(state*state)" +by (auto simp add: program_def RawActs_def) + +lemma RawAllowedActs_type: + "F \ program ==> RawAllowedActs(F)\Pow(state*state)" +by (auto simp add: program_def RawAllowedActs_def) + +lemma Init_type: "Init(F)\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)\Pow(state*state)" +by (simp add: RawActs_type Acts_def) + +lemma AllowedActs_type: "AllowedActs(F) \ Pow(state*state)" +by (simp add: RawAllowedActs_type AllowedActs_def) + +(* Needed in Behaviors *) +lemma ActsD: "[| act \ Acts(F); \ act |] ==> s \ state & s' \ state" +by (blast dest: Acts_type [THEN subsetD]) + +lemma AllowedActsD: + "[| act \ AllowedActs(F); \ act |] ==> s \ state & s' \ 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 \ 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) \ 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) \ AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)" +by (cut_tac F = F in AllowedActs_type, auto) + +subsubsection{*Eliminating @{text "\ state"} from expressions*} + +lemma Init_Int_state [simp]: "Init(F) \ state = Init(F)" +by (cut_tac F = F in Init_type, blast) + +lemma state_Int_Init [simp]: "state \ Init(F) = Init(F)" +by (cut_tac F = F in Init_type, blast) + +lemma Acts_Int_Pow_state_times_state [simp]: + "Acts(F) \ Pow(state*state) = Acts(F)" +by (cut_tac F = F in Acts_type, blast) + +lemma state_times_state_Int_Acts [simp]: + "Pow(state*state) \ Acts(F) = Acts(F)" +by (cut_tac F = F in Acts_type, blast) + +lemma AllowedActs_Int_Pow_state_times_state [simp]: + "AllowedActs(F) \ Pow(state*state) = AllowedActs(F)" +by (cut_tac F = F in AllowedActs_type, blast) + +lemma state_times_state_Int_AllowedActs [simp]: + "Pow(state*state) \ 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) \ program" +by (auto simp add: mk_program_def program_def) + +lemma RawInit_eq [simp]: + "RawInit(mk_program(init, acts, allowed)) = init \ state" +by (auto simp add: mk_program_def RawInit_def) + +lemma RawActs_eq [simp]: + "RawActs(mk_program(init, acts, allowed)) = + cons(id(state), acts \ 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 \ Pow(state*state))" +by (auto simp add: mk_program_def RawAllowedActs_def) + +lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \ state" +by (simp add: Init_def) + +lemma Acts_eq [simp]: + "Acts(mk_program(init, acts, allowed)) = + cons(id(state), acts \ Pow(state*state))" +by (simp add: Acts_def) + +lemma AllowedActs_eq [simp]: + "AllowedActs(mk_program(init, acts, allowed))= + cons(id(state), allowed \ 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 \ 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 \ program; G \ 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 \ program; G \ 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 \ state" +by auto + +lemma def_prg_Acts: + "F == mk_program (init,acts,allowed) + ==> Acts(F) = cons(id(state), acts \ Pow(state*state))" +by auto + +lemma def_prg_AllowedActs: + "F == mk_program (init,acts,allowed) + ==> AllowedActs(F) = cons(id(state), allowed \ Pow(state*state))" +by auto + +lemma def_prg_simps: + "[| F == mk_program (init,acts,allowed) |] + ==> Init(F) = init \ state & + Acts(F) = cons(id(state), acts \ Pow(state*state)) & + AllowedActs(F) = cons(id(state), allowed \ 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 == { \ A*B. P(s, s')} |] + ==> ( \ act) <-> ( \ 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 \ A) <-> (x \ B)" +by auto + + +subsection{*The Constrains Operator*} + +lemma constrains_type: "A co B \ program" +by (force simp add: constrains_def) + +lemma constrainsI: + "[|(!!act s s'. [| act: Acts(F); \ act; s \ A|] ==> s' \ A'); + F \ program; st_set(A) |] ==> F \ A co A'" +by (force simp add: constrains_def) + +lemma constrainsD: + "F \ A co B ==> \act \ Acts(F). act``A\B" +by (force simp add: constrains_def) + +lemma constrainsD2: "F \ A co B ==> F \ program & st_set(A)" +by (force simp add: constrains_def) + +lemma constrains_empty [iff]: "F \ 0 co B <-> F \ program" +by (force simp add: constrains_def st_set_def) + +lemma constrains_empty2 [iff]: "(F \ A co 0) <-> (A=0 & F \ program)" +by (force simp add: constrains_def st_set_def) + +lemma constrains_state [iff]: "(F \ state co B) <-> (state\B & F \ program)" +apply (cut_tac F = F in Acts_type) +apply (force simp add: constrains_def st_set_def) +done + +lemma constrains_state2 [iff]: "F \ A co state <-> (F \ 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 \ A co A'; A'\B' |] ==> F \ A co B'" +apply (unfold constrains_def, blast) +done + +(*anti-monotonic in 1st argument*) +lemma constrains_weaken_L: + "[| F \ A co A'; B\A |] ==> F \ B co A'" +apply (unfold constrains_def st_set_def, blast) +done + +lemma constrains_weaken: + "[| F \ A co A'; B\A; A'\B' |] ==> F \ 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 \ A co A'; F \ B co B' |] ==> F \ (A Un B) co (A' Un B')" +by (auto simp add: constrains_def st_set_def, force) + +lemma constrains_UN: + "[|!!i. i \ I ==> F \ A(i) co A'(i); F \ program |] + ==> F \ (\i \ I. A(i)) co (\i \ I. A'(i))" +by (force simp add: constrains_def st_set_def) + +lemma constrains_Un_distrib: + "(A Un B) co C = (A co C) \ (B co C)" +by (force simp add: constrains_def st_set_def) + +lemma constrains_UN_distrib: + "i \ I ==> (\i \ I. A(i)) co B = (\i \ 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 \ B) = (C co A) \ (C co B)" +by (force simp add: constrains_def st_set_def) + +lemma constrains_INT_distrib: + "x \ I ==> A co (\i \ I. B(i)) = (\i \ I. A co B(i))" +by (force simp add: constrains_def st_set_def) + +lemma constrains_Int: + "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')" +by (force simp add: constrains_def st_set_def) + +lemma constrains_INT [rule_format]: + "[| \i \ I. F \ A(i) co A'(i); F \ program|] + ==> F \ (\i \ I. A(i)) co (\i \ 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 (\z. A i) co (\z. B i) *) +lemma constrains_All: +"[| \z. F:{s \ state. P(s, z)} co {s \ state. Q(s, z)}; F \ program |]==> + F:{s \ state. \z. P(s, z)} co {s \ state. \z. Q(s, z)}" +by (unfold constrains_def, blast) + +lemma constrains_imp_subset: + "[| F \ A co A' |] ==> A \ 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 \ A co B; F \ B co C |] ==> F \ A co C" +by (unfold constrains_def st_set_def, auto, blast) + +lemma constrains_cancel: +"[| F \ A co (A' Un B); F \ B co B' |] ==> F \ 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 \ program" +by (force simp add: unless_def constrains_def) + +lemma unlessI: "[| F \ (A-B) co (A Un B) |] ==> F \ A unless B" +apply (unfold unless_def) +apply (blast dest: constrainsD2) +done + +lemma unlessD: "F :A unless B ==> F \ (A-B) co (A Un B)" +by (unfold unless_def, auto) + + +subsection{*The Operator @{term initially}*} + +lemma initially_type: "initially(A) \ program" +by (unfold initially_def, blast) + +lemma initiallyI: "[| F \ program; Init(F)\A |] ==> F \ initially(A)" +by (unfold initially_def, blast) + +lemma initiallyD: "F \ initially(A) ==> Init(F)\A" +by (unfold initially_def, blast) + + +subsection{*The Operator @{term stable}*} + +lemma stable_type: "stable(A)\program" +by (unfold stable_def constrains_def, blast) + +lemma stableI: "F \ A co A ==> F \ stable(A)" +by (unfold stable_def, assumption) + +lemma stableD: "F \ stable(A) ==> F \ A co A" +by (unfold stable_def, assumption) + +lemma stableD2: "F \ stable(A) ==> F \ 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 \ stable(A); F \ stable(A') |] ==> F \ stable(A Un A')" +apply (unfold stable_def) +apply (blast intro: constrains_Un) +done + +lemma stable_UN: + "[|!!i. i\I ==> F \ stable(A(i)); F \ program |] + ==> F \ stable (\i \ I. A(i))" +apply (unfold stable_def) +apply (blast intro: constrains_UN) +done + +lemma stable_Int: + "[| F \ stable(A); F \ stable(A') |] ==> F \ stable (A \ A')" +apply (unfold stable_def) +apply (blast intro: constrains_Int) +done + +lemma stable_INT: + "[| !!i. i \ I ==> F \ stable(A(i)); F \ program |] + ==> F \ stable (\i \ I. A(i))" +apply (unfold stable_def) +apply (blast intro: constrains_INT) +done + +lemma stable_All: + "[|\z. F \ stable({s \ state. P(s, z)}); F \ program|] + ==> F \ stable({s \ state. \z. P(s, z)})" +apply (unfold stable_def) +apply (rule constrains_All, auto) +done + +lemma stable_constrains_Un: + "[| F \ stable(C); F \ A co (C Un A') |] ==> F \ (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 \ stable(C); F \ (C \ A) co A' |] ==> F \ (C \ A) co (C \ A')" +by (unfold stable_def constrains_def st_set_def, blast) + +(* [| F \ stable(C); F \ (C \ A) co A |] ==> F \ stable(C \ A) *) +lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard] + +subsection{*The Operator @{term invariant}*} + +lemma invariant_type: "invariant(A) \ program" +apply (unfold invariant_def) +apply (blast dest: stable_type [THEN subsetD]) +done + +lemma invariantI: "[| Init(F)\A; F \ stable(A) |] ==> F \ invariant(A)" +apply (unfold invariant_def initially_def) +apply (frule stable_type [THEN subsetD], auto) +done + +lemma invariantD: "F \ invariant(A) ==> Init(F)\A & F \ stable(A)" +by (unfold invariant_def initially_def, auto) + +lemma invariantD2: "F \ invariant(A) ==> F \ program & st_set(A)" +apply (unfold invariant_def) +apply (blast dest: stableD2) +done + +text{*Could also say + @{term "invariant(A) \ invariant(B) \ invariant (A \ B)"}*} +lemma invariant_Int: + "[| F \ invariant(A); F \ invariant(B) |] ==> F \ invariant(A \ 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 \m ? Would make it harder + to use in forward proof. **) + +(* The general case easier to prove that le special case! *) +lemma "elimination": + "[| \m \ M. F \ {s \ A. x(s) = m} co B(m); F \ program |] + ==> F \ {s \ A. x(s) \ M} co (\m \ 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: + "[| \m \ M. F \ {s \ state. x(s) = m} co B(m); F \ program |] + ==> F:{s \ state. x(s) \ M} co (\m \ M. B(m))" +by (rule UNITY.elimination, auto) + +subsection{*The Operator @{term strongest_rhs}*} + +lemma constrains_strongest_rhs: + "[| F \ program; st_set(A) |] ==> F \ 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 \ A co B; st_set(B) |] ==> strongest_rhs(F,A) \ 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 - diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/Union.ML --- 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"; diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/UNITY/WFair.thy --- 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 @@ :leads(D, F)" monos Pow_mono - type_intrs "[Union_PowI, UnionI, PowI]" + type_intrs "[Union_Pow_iff RS iffD2, UnionI, PowI]" constdefs diff -r 5cfc8b9fb880 -r 37c964462747 src/ZF/equalities.thy --- 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) \ Pow(B) <-> A \ 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";