# HG changeset patch # User paulson # Date 1044040364 -3600 # Node ID 4c1a53627500369de333b14ad7e6cebaf9d04a28 # Parent baefae13ad379e78b6bcae1a1bf88f3ccc2ae3bd conversion to new-style theories and tidying diff -r baefae13ad37 -r 4c1a53627500 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/IsaMakefile Fri Jan 31 20:12:44 2003 +0100 @@ -383,8 +383,7 @@ $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \ UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ - UNITY/Extend.thy UNITY/FP.thy \ - UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \ + UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \ UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \ UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \ @@ -394,7 +393,7 @@ UNITY/Simple/Network.thy\ UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\ UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \ - UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \ + UNITY/Comp/AllocBase.thy \ UNITY/Comp/Client.ML UNITY/Comp/Client.thy \ UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \ UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \ diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Fri Jan 31 20:12:44 2003 +0100 @@ -13,6 +13,8 @@ *) +header{*Composition: Basic Primitives*} + theory Comp = Union: instance program :: (type) ord .. @@ -42,7 +44,7 @@ "funPair f g == %x. (f x, g x)" -(*** component <= ***) +subsection{*The component relation*} lemma componentI: "H <= F | H <= G ==> H <= (F Join G)" apply (unfold component_def, auto) @@ -76,8 +78,7 @@ lemma component_Join2: "G <= (F Join G)" apply (unfold component_def) -apply (simp (no_asm) add: Join_commute) -apply blast +apply (simp add: Join_commute, blast) done lemma Join_absorb1: "F<=G ==> F Join G = G" @@ -87,9 +88,7 @@ by (auto simp add: Join_ac component_def) lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)" -apply (simp (no_asm) add: component_eq_subset) -apply blast -done +by (simp add: component_eq_subset, blast) lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))" apply (unfold component_def) @@ -107,9 +106,7 @@ done lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)" -apply (simp (no_asm) add: component_eq_subset) -apply blast -done +by (simp add: component_eq_subset, blast) lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B" by (auto simp add: constrains_def component_eq_subset) @@ -118,7 +115,7 @@ lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq] -(*** preserves ***) +subsection{*The preserves property*} lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v" by (unfold preserves_def, blast) @@ -135,8 +132,7 @@ lemma JN_preserves [iff]: "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)" -apply (simp (no_asm) add: JN_stable preserves_def) -apply blast +apply (simp add: JN_stable preserves_def, blast) done lemma SKIP_preserves [iff]: "SKIP : preserves v" @@ -153,16 +149,13 @@ lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)" -apply (simp (no_asm) add: funPair_def o_def) -done +by (simp add: funPair_def o_def) lemma fst_o_funPair [simp]: "fst o (funPair f g) = f" -apply (simp (no_asm) add: funPair_def o_def) -done +by (simp add: funPair_def o_def) lemma snd_o_funPair [simp]: "snd o (funPair f g) = g" -apply (simp (no_asm) add: funPair_def o_def) -done +by (simp add: funPair_def o_def) lemma subset_preserves_o: "preserves v <= preserves (w o v)" by (force simp add: preserves_def stable_def constrains_def) @@ -244,18 +237,13 @@ (** localize **) lemma localize_Init_eq [simp]: "Init (localize v F) = Init F" -apply (unfold localize_def) -apply (simp (no_asm)) -done +by (simp add: localize_def) lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F" -apply (unfold localize_def) -apply (simp (no_asm)) -done +by (simp add: localize_def) lemma localize_AllowedActs_eq [simp]: "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)" -apply (unfold localize_def, auto) -done +by (unfold localize_def, auto) end diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Comp/AllocBase.ML --- a/src/HOL/UNITY/Comp/AllocBase.ML Thu Jan 30 18:08:09 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,89 +0,0 @@ -(* Title: HOL/UNITY/AllocBase.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Basis declarations for Chandy and Charpentier's Allocator -*) - -Goal "!!f :: nat=>nat. \ -\ (ALL i. i f i <= g i) --> \ -\ setsum f (lessThan n) <= setsum g (lessThan n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc])); -by (dres_inst_tac [("x","n")] spec 1); -by (arith_tac 1); -qed_spec_mp "setsum_fun_mono"; - -Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; -by (induct_tac "ys" 1); -by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); -qed_spec_mp "tokens_mono_prefix"; - -Goalw [mono_def] "mono tokens"; -by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); -qed "mono_tokens"; - - -(** bag_of **) - -Goal "bag_of (l@l') = bag_of l + bag_of l'"; -by (induct_tac "l" 1); - by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2); -by (Simp_tac 1); -qed "bag_of_append"; -Addsimps [bag_of_append]; - -Goal "mono (bag_of :: 'a list => ('a::order) multiset)"; -by (rtac monoI 1); -by (rewtac prefix_def); -by (etac genPrefix.induct 1); -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); -by (etac order_trans 1); -by (rtac (thm "union_upper1") 1); -qed "mono_bag_of"; - -(** setsum **) - -Addcongs [setsum_cong]; - -Goal "(\\i: A Int lessThan k. {#if ii: A Int lessThan k. {#f i#})"; -by (rtac setsum_cong 1); -by Auto_tac; -qed "bag_of_sublist_lemma"; - -Goal "bag_of (sublist l A) = \ -\ (\\i: A Int lessThan (length l). {# l!i #})"; -by (res_inst_tac [("xs","l")] rev_induct 1); -by (Simp_tac 1); -by (asm_simp_tac - (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, - nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1); -qed "bag_of_sublist"; - - -Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \ -\ bag_of (sublist l A) + bag_of (sublist l B)"; -by (subgoal_tac "A Int B Int {..length l(} = \ -\ (A Int {..length l(}) Int (B Int {..length l(})" 1); -by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, - setsum_Un_Int]) 1); -by (Blast_tac 1); -qed "bag_of_sublist_Un_Int"; - -Goal "A Int B = {} \ -\ ==> bag_of (sublist l (A Un B)) = \ -\ bag_of (sublist l A) + bag_of (sublist l B)"; -by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1); -qed "bag_of_sublist_Un_disjoint"; - -Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \ -\ ==> bag_of (sublist l (UNION I A)) = \ -\ (\\i:I. bag_of (sublist l (A i)))"; -by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym]) - addsimps [bag_of_sublist]) 1); -by (stac setsum_UN_disjoint 1); -by Auto_tac; -qed_spec_mp "bag_of_sublist_UN_disjoint"; diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Comp/AllocBase.thy --- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,29 +3,124 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Common declarations for Chandy and Charpentier's Allocator *) -AllocBase = UNITY_Main + +header{*Common Declarations for Chandy and Charpentier's Allocator*} + +theory AllocBase = UNITY_Main: consts NbT :: nat (*Number of tokens in system*) Nclients :: nat (*Number of clients*) -rules - NbT_pos "0 < NbT" +axioms + NbT_pos: "0 < NbT" (*This function merely sums the elements of a list*) -consts tokens :: nat list => nat +consts tokens :: "nat list => nat" primrec "tokens [] = 0" "tokens (x#xs) = x + tokens xs" consts - bag_of :: 'a list => 'a multiset + bag_of :: "'a list => 'a multiset" primrec "bag_of [] = {#}" "bag_of (x#xs) = {#x#} + bag_of xs" +lemma setsum_fun_mono [rule_format]: + "!!f :: nat=>nat. + (ALL i. i f i <= g i) --> + setsum f (lessThan n) <= setsum g (lessThan n)" +apply (induct_tac "n") +apply (auto simp add: lessThan_Suc) +apply (drule_tac x = n in spec, arith) +done + +lemma tokens_mono_prefix [rule_format]: + "ALL xs. xs <= ys --> tokens xs <= tokens ys" +apply (induct_tac "ys") +apply (auto simp add: prefix_Cons) +done + +lemma mono_tokens: "mono tokens" +apply (unfold mono_def) +apply (blast intro: tokens_mono_prefix) +done + + +(** bag_of **) + +lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" +apply (induct_tac "l", simp) + apply (simp add: plus_ac0) +done + +lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" +apply (rule monoI) +apply (unfold prefix_def) +apply (erule genPrefix.induct, auto) +apply (simp add: union_le_mono) +apply (erule order_trans) +apply (rule union_upper1) +done + +(** setsum **) + +declare setsum_cong [cong] + +lemma bag_of_sublist_lemma: + "(\i: A Int lessThan k. {#if ii: A Int lessThan k. {#f i#})" +apply (rule setsum_cong, auto) +done + +lemma bag_of_sublist: + "bag_of (sublist l A) = + (\i: A Int lessThan (length l). {# l!i #})" +apply (rule_tac xs = l in rev_induct, simp) +apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append + bag_of_sublist_lemma plus_ac0) +done + + +lemma bag_of_sublist_Un_Int: + "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = + bag_of (sublist l A) + bag_of (sublist l B)" +apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ") +apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast) +done + +lemma bag_of_sublist_Un_disjoint: + "A Int B = {} + ==> bag_of (sublist l (A Un B)) = + bag_of (sublist l A) + bag_of (sublist l B)" +apply (simp add: bag_of_sublist_Un_Int [symmetric]) +done + +lemma bag_of_sublist_UN_disjoint [rule_format]: + "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] + ==> bag_of (sublist l (UNION I A)) = + (\i:I. bag_of (sublist l (A i)))" +apply (simp del: UN_simps + add: UN_simps [symmetric] add: bag_of_sublist) +apply (subst setsum_UN_disjoint, auto) +done + +ML +{* +val NbT_pos = thm "NbT_pos"; +val setsum_fun_mono = thm "setsum_fun_mono"; +val tokens_mono_prefix = thm "tokens_mono_prefix"; +val mono_tokens = thm "mono_tokens"; +val bag_of_append = thm "bag_of_append"; +val mono_bag_of = thm "mono_bag_of"; +val bag_of_sublist_lemma = thm "bag_of_sublist_lemma"; +val bag_of_sublist = thm "bag_of_sublist"; +val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int"; +val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint"; +val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint"; +*} + end diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Constrains.thy Fri Jan 31 20:12:44 2003 +0100 @@ -6,6 +6,8 @@ Weak safety relations: restricted to the set of reachable states. *) +header{*Weak Safety*} + theory Constrains = UNITY: consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" @@ -50,7 +52,7 @@ "Increasing f == INT z. Stable {s. z <= f s}" -(*** traces and reachable ***) +subsection{*traces and reachable*} lemma reachable_equiv_traces: "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" @@ -82,7 +84,7 @@ done -(*** Co ***) +subsection{*Co*} (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) lemmas constrains_reachable_Int = @@ -184,7 +186,7 @@ by (simp add: Constrains_eq_constrains constrains_def, blast) -(*** Stable ***) +subsection{*Stable*} (*Useful because there's no Stable_weaken. [Tanja Vos]*) lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" @@ -238,7 +240,7 @@ -(*** Increasing ***) +subsection{*Increasing*} lemma IncreasingD: "F : Increasing f ==> F : Stable {s. x <= f s}" @@ -265,14 +267,14 @@ increasing_constant [THEN increasing_imp_Increasing, standard, iff] -(*** 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. ***) +subsection{*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.*) lemma Elimination: "[| ALL m. F : {s. s x = m} Co (B m) |] ==> F : {s. s x : M} Co (UN m:M. B m)" - by (unfold Constrains_def constrains_def, blast) (*As above, but for the trivial case of a one-variable state, in which the @@ -282,7 +284,7 @@ by (unfold Constrains_def constrains_def, blast) -(*** Specialized laws for handling Always ***) +subsection{*Specialized laws for handling Always*} (** Natural deduction rules for "Always A" **) @@ -340,7 +342,7 @@ by (auto simp add: Always_eq_includes_reachable) -(*** "Co" rules involving Always ***) +subsection{*"Co" rules involving Always*} lemma Always_Constrains_pre: "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')" diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Detects.thy --- a/src/HOL/UNITY/Detects.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Detects.thy Fri Jan 31 20:12:44 2003 +0100 @@ -6,6 +6,8 @@ Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo *) +header{*The Detects Relation*} + theory Detects = FP + SubstAx: consts diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/ELT.thy --- a/src/HOL/UNITY/ELT.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/ELT.thy Fri Jan 31 20:12:44 2003 +0100 @@ -22,6 +22,8 @@ monos Pow_mono *) +header{*Progress Under Allowable Sets*} + theory ELT = Project: consts @@ -91,8 +93,7 @@ (*preserving v preserves properties given by v*) lemma preserves_givenBy_imp_stable: "[| F : preserves v; D : givenBy v |] ==> F : stable D" -apply (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect) -done +by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect) lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v" apply (simp (no_asm) add: givenBy_eq_Collect) @@ -212,7 +213,7 @@ apply (blast intro: subset_imp_leadsETo leadsETo_Trans) done -lemma leadsETo_weaken_L [rule_format (no_asm)]: +lemma leadsETo_weaken_L [rule_format]: "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'" apply (blast intro: leadsETo_Trans subset_imp_leadsETo) done @@ -458,13 +459,13 @@ lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard] -lemma LeadsETo_weaken_R [rule_format (no_asm)]: +lemma LeadsETo_weaken_R [rule_format]: "[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'" apply (simp (no_asm_use) add: LeadsETo_def) apply (blast intro: leadsETo_weaken_R) done -lemma LeadsETo_weaken_L [rule_format (no_asm)]: +lemma LeadsETo_weaken_L [rule_format]: "[| F : A LeadsTo[CC] A'; B <= A |] ==> F : B LeadsTo[CC] A'" apply (simp (no_asm_use) add: LeadsETo_def) apply (blast intro: leadsETo_weaken_L) diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Extend.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,11 +3,13 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Extending of state sets +Extending of state setsExtending of state sets function f (forget) maps the extended state to the original state function g (forgotten) maps the extended state to the "extending part" *) +header{*Extending State Sets*} + theory Extend = Guar: constdefs @@ -60,7 +62,8 @@ (** These we prove OUTSIDE the locale. **) -(*** Restrict [MOVE to Relation.thy?] ***) +subsection{*Restrict*} +(*MOVE to Relation.thy?*) lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)" by (unfold Restrict_def, blast) @@ -130,7 +133,7 @@ done -(*** Trivial properties of f, g, h ***) +subsection{*Trivial properties of f, g, h*} lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2]) @@ -163,7 +166,7 @@ -(*** extend_set: basic properties ***) +subsection{*@{term extend_set}: basic properties*} lemma project_set_iff [iff]: "(x : project_set h C) = (EX y. h(x,y) : C)" @@ -210,7 +213,7 @@ apply (auto simp add: split_extended_all) done -(*** project_set: basic properties ***) +subsection{*@{term project_set}: basic properties*} (*project_set is simply image!*) lemma (in Extend) project_set_eq: "project_set h C = f ` C" @@ -221,7 +224,7 @@ by (auto simp add: split_extended_all) -(*** More laws ***) +subsection{*More laws*} (*Because A and B could differ on the "other" part of the state, cannot generalize to @@ -265,7 +268,7 @@ by (unfold extend_set_def, auto) -(*** extend_act ***) +subsection{*@{term extend_act}*} (*Can't strengthen it to ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') @@ -335,9 +338,9 @@ -(**** extend ****) +subsection{*extend ****) -(*** Basic properties ***) +(*** Basic properties*} lemma Init_extend [simp]: "Init (extend h F) = extend_set h (Init F)" @@ -451,7 +454,7 @@ by (simp add: component_eq_subset, blast) -(*** Safety: co, stable ***) +subsection{*Safety: co, stable*} lemma (in Extend) extend_constrains: "(extend h F : (extend_set h A) co (extend_set h B)) = @@ -477,7 +480,7 @@ by (simp add: stable_def extend_constrains_project_set) -(*** Weak safety primitives: Co, Stable ***) +subsection{*Weak safety primitives: Co, Stable*} lemma (in Extend) reachable_extend_f: "p : reachable (extend h F) ==> f p : reachable F" @@ -570,7 +573,7 @@ by (simp add: stable_def project_constrains_project_set) -(*** Progress: transient, ensures ***) +subsection{*Progress: transient, ensures*} lemma (in Extend) extend_transient: "(extend h F : transient (extend_set h A)) = (F : transient A)" @@ -591,7 +594,7 @@ apply (simp add: leadsTo_UN extend_set_Union) done -(*** Proving the converse takes some doing! ***) +subsection{*Proving the converse takes some doing!*} lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)" by (simp (no_asm) add: slice_def) @@ -631,7 +634,7 @@ apply (blast intro: leadsTo_UN) done -lemma (in Extend) extend_leadsTo_slice [rule_format (no_asm)]: +lemma (in Extend) extend_leadsTo_slice [rule_format]: "extend h F : AU leadsTo BU ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)" apply (erule leadsTo_induct) @@ -656,7 +659,7 @@ extend_set_Int_distrib [symmetric]) -(*** preserves ***) +subsection{*preserves*} lemma (in Extend) project_preserves_I: "G : preserves (v o f) ==> project h C G : preserves v" @@ -677,7 +680,7 @@ constrains_def g_def) -(*** Guarantees ***) +subsection{*Guarantees*} lemma (in Extend) project_extend_Join: "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)" diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/FP.thy --- a/src/HOL/UNITY/FP.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/FP.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,11 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Fixed Point of a Program - From Misra, "A Logic for Concurrent Programming", 1994 *) +header{*Fixed Point of a Program*} + theory FP = UNITY: constdefs diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Follows.thy Fri Jan 31 20:12:44 2003 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge +*) -The "Follows" relation of Charpentier and Sivilotte -*) +header{*The Follows Relation of Charpentier and Sivilotte*} theory Follows = SubstAx + ListOrder + Multiset: @@ -35,9 +35,8 @@ apply (blast intro: monoD order_trans)+ done -lemma Follows_constant: "F : (%s. c) Fols (%s. c)" +lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)" by (unfold Follows_def, auto) -declare Follows_constant [iff] lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)" apply (unfold Follows_def, clarify) @@ -60,28 +59,23 @@ done -(** Destructiom rules **) +subsection{*Destruction rules*} -lemma Follows_Increasing1: - "F : f Fols g ==> F : Increasing f" - +lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f" apply (unfold Follows_def, blast) done -lemma Follows_Increasing2: - "F : f Fols g ==> F : Increasing g" +lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g" apply (unfold Follows_def, blast) done -lemma Follows_Bounded: - "F : f Fols g ==> F : Always {s. f s <= g s}" +lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}" apply (unfold Follows_def, blast) done lemma Follows_LeadsTo: "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}" -apply (unfold Follows_def, blast) -done +by (unfold Follows_def, blast) lemma Follows_LeadsTo_pfixLe: "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}" @@ -107,7 +101,8 @@ apply (unfold Follows_def Increasing_def Stable_def, auto) apply (erule_tac [3] Always_LeadsTo_weaken) -apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" in Always_Constrains_weaken, auto) +apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" + in Always_Constrains_weaken, auto) apply (drule Always_Int_I, assumption) apply (force intro: Always_weaken) done @@ -116,13 +111,14 @@ "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'" apply (unfold Follows_def Increasing_def Stable_def, auto) apply (erule_tac [3] Always_LeadsTo_weaken) -apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" in Always_Constrains_weaken, auto) +apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" + in Always_Constrains_weaken, auto) apply (drule Always_Int_I, assumption) apply (force intro: Always_weaken) done -(** Union properties (with the subset ordering) **) +subsection{*Union properties (with the subset ordering)*} (*Can replace "Un" by any sup. But existing max only works for linorders.*) lemma increasing_Un: @@ -137,7 +133,8 @@ lemma Increasing_Un: "[| F : Increasing f; F: Increasing g |] ==> F : Increasing (%s. (f s) Un (g s))" -apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto) +apply (auto simp add: Increasing_def Stable_def Constrains_def + stable_def constrains_def) apply (drule_tac x = "f xa" in spec) apply (drule_tac x = "g xa" in spec) apply (blast dest!: bspec) @@ -147,8 +144,7 @@ lemma Always_Un: "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] ==> F : Always {s. f' s Un g' s <= f s Un g s}" -apply (simp add: Always_eq_includes_reachable, blast) -done +by (simp add: Always_eq_includes_reachable, blast) (*Lemma to re-use the argument that one variable increases (progress) while the other variable doesn't decrease (safety)*) @@ -164,8 +160,7 @@ apply (rule PSP_Stable) apply (erule_tac x = "f s" in spec) apply (erule Stable_Int, assumption) -apply blast -apply blast +apply blast+ done lemma Follows_Un: @@ -180,12 +175,11 @@ done -(** Multiset union properties (with the multiset ordering) **) +subsection{*Multiset union properties (with the multiset ordering)*} lemma increasing_union: "[| F : increasing f; F: increasing g |] ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))" - apply (unfold increasing_def stable_def constrains_def, auto) apply (drule_tac x = "f xa" in spec) apply (drule_tac x = "g xa" in spec) @@ -196,7 +190,8 @@ lemma Increasing_union: "[| F : Increasing f; F: Increasing g |] ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))" -apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto) +apply (auto simp add: Increasing_def Stable_def Constrains_def + stable_def constrains_def) apply (drule_tac x = "f xa" in spec) apply (drule_tac x = "g xa" in spec) apply (drule bspec, assumption) diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/GenPrefix.ML --- a/src/HOL/UNITY/GenPrefix.ML Thu Jan 30 18:08:09 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,424 +0,0 @@ -(* Title: HOL/UNITY/GenPrefix.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Charpentier's Generalized Prefix Relation - (xs,ys) : genPrefix r - if ys = xs' @ zs where length xs = length xs' - and corresponding elements of xs, xs' are pairwise related by r - -Based on Lex/Prefix -*) - -(*** preliminary lemmas ***) - -Goal "([], xs) : genPrefix r"; -by (cut_facts_tac [genPrefix.Nil RS genPrefix.append] 1); -by Auto_tac; -qed "Nil_genPrefix"; -AddIffs[Nil_genPrefix]; - -Goal "(xs,ys) : genPrefix r ==> length xs <= length ys"; -by (etac genPrefix.induct 1); -by Auto_tac; -qed "genPrefix_length_le"; - -Goal "[| (xs', ys'): genPrefix r |] \ -\ ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"; -by (etac genPrefix.induct 1); -by (Blast_tac 1); -by (Blast_tac 1); -by (force_tac (claset() addIs [genPrefix.append], - simpset()) 1); -val lemma = result(); - -(*As usual converting it to an elimination rule is tiresome*) -val major::prems = -Goal "[| (x#xs, zs): genPrefix r; \ -\ !!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [major RS lemma] 1); -by (Full_simp_tac 1); -by (REPEAT (eresolve_tac [exE, conjE] 1)); -by (REPEAT (ares_tac prems 1)); -qed "cons_genPrefixE"; - -AddSEs [cons_genPrefixE]; - -Goal "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"; -by (blast_tac (claset() addIs [genPrefix.prepend]) 1); -qed"Cons_genPrefix_Cons"; -AddIffs [Cons_genPrefix_Cons]; - - -(*** genPrefix is a partial order ***) - -Goalw [refl_def] "reflexive r ==> reflexive (genPrefix r)"; -by Auto_tac; -by (induct_tac "x" 1); -by (blast_tac (claset() addIs [genPrefix.prepend]) 2); -by (blast_tac (claset() addIs [genPrefix.Nil]) 1); -qed "refl_genPrefix"; - -Goal "reflexive r ==> (l,l) : genPrefix r"; -by (etac ([refl_genPrefix,UNIV_I] MRS reflD) 1); -qed "genPrefix_refl"; - -Addsimps [genPrefix_refl]; - -Goal "r<=s ==> genPrefix r <= genPrefix s"; -by (Clarify_tac 1); -by (etac genPrefix.induct 1); -by (auto_tac (claset() addIs [genPrefix.append], simpset())); -qed "genPrefix_mono"; - - -(** Transitivity **) - -(*A lemma for proving genPrefix_trans_O*) -Goal "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"; -by (induct_tac "xs" 1); -by Auto_tac; -qed_spec_mp "append_genPrefix"; - -(*Lemma proving transitivity and more*) -Goalw [prefix_def] - "(x, y) : genPrefix r \ -\ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"; -by (etac genPrefix.induct 1); - by (blast_tac (claset() addDs [append_genPrefix]) 3); - by (blast_tac (claset() addIs [genPrefix.prepend]) 2); -by (Blast_tac 1); -qed_spec_mp "genPrefix_trans_O"; - -Goal "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] \ -\ ==> (x,z) : genPrefix r"; -by (rtac (impOfSubs (trans_O_subset RS genPrefix_mono)) 1); - by (assume_tac 2); -by (blast_tac (claset() addIs [genPrefix_trans_O]) 1); -qed_spec_mp "genPrefix_trans"; - -Goalw [prefix_def] - "[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"; -by (stac (R_O_Id RS sym) 1 THEN etac genPrefix_trans_O 1); -by (assume_tac 1); -qed_spec_mp "prefix_genPrefix_trans"; - -Goalw [prefix_def] - "[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r"; -by (stac (Id_O_R RS sym) 1 THEN etac genPrefix_trans_O 1); -by (assume_tac 1); -qed_spec_mp "genPrefix_prefix_trans"; - -Goal "trans r ==> trans (genPrefix r)"; -by (blast_tac (claset() addIs [transI, genPrefix_trans]) 1); -qed "trans_genPrefix"; - - -(** Antisymmetry **) - -Goal "[| (xs,ys) : genPrefix r; antisym r |] \ -\ ==> (ys,xs) : genPrefix r --> xs = ys"; -by (etac genPrefix.induct 1); -by (full_simp_tac (simpset() addsimps [antisym_def]) 2); -by (Blast_tac 2); -by (Blast_tac 1); -(*append case is hardest*) -by (Clarify_tac 1); -by (subgoal_tac "length zs = 0" 1); -by (Force_tac 1); -by (REPEAT (dtac genPrefix_length_le 1)); -by (full_simp_tac (simpset() delsimps [length_0_conv]) 1); -qed_spec_mp "genPrefix_antisym"; - -Goal "antisym r ==> antisym (genPrefix r)"; -by (blast_tac (claset() addIs [antisymI, genPrefix_antisym]) 1); -qed "antisym_genPrefix"; - - -(*** recursion equations ***) - -Goal "((xs, []) : genPrefix r) = (xs = [])"; -by (induct_tac "xs" 1); -by (Blast_tac 2); -by (Simp_tac 1); -qed "genPrefix_Nil"; -Addsimps [genPrefix_Nil]; - -Goalw [refl_def] - "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "same_genPrefix_genPrefix"; -Addsimps [same_genPrefix_genPrefix]; - -Goal "((xs, y#ys) : genPrefix r) = \ -\ (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"; -by (case_tac "xs" 1); -by Auto_tac; -qed "genPrefix_Cons"; - -Goal "[| reflexive r; (xs,ys) : genPrefix r |] \ -\ ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r"; -by (etac genPrefix.induct 1); -by (ftac genPrefix_length_le 3); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]))); -qed "genPrefix_take_append"; - -Goal "[| reflexive r; (xs,ys) : genPrefix r; length xs = length ys |] \ -\ ==> (xs@zs, ys @ zs) : genPrefix r"; -by (dtac genPrefix_take_append 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [take_all]) 1); -qed "genPrefix_append_both"; - - -(*NOT suitable for rewriting since [y] has the form y#ys*) -Goal "xs @ y # ys = (xs @ [y]) @ ys"; -by Auto_tac; -qed "append_cons_eq"; - -Goal "[| (xs,ys) : genPrefix r; reflexive r |] \ -\ ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"; -by (etac genPrefix.induct 1); -by (Blast_tac 1); -by (Asm_simp_tac 1); -(*Append case is hardest*) -by (Asm_simp_tac 1); -by (forward_tac [genPrefix_length_le RS le_imp_less_or_eq] 1); -by (etac disjE 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [neq_Nil_conv, nth_append]))); -by (blast_tac (claset() addIs [genPrefix.append]) 1); -by Auto_tac; -by (stac append_cons_eq 1); -by (blast_tac (claset() addIs [genPrefix_append_both, genPrefix.append]) 1); -val lemma = result() RS mp; - -Goal "[| (xs,ys) : genPrefix r; length xs < length ys; reflexive r |] \ -\ ==> (xs @ [ys ! length xs], ys) : genPrefix r"; -by (blast_tac (claset() addIs [lemma]) 1); -qed "append_one_genPrefix"; - - - - -(** Proving the equivalence with Charpentier's definition **) - -Goal "ALL i ys. i < length xs \ -\ --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"; -by (induct_tac "xs" 1); -by Auto_tac; -by (case_tac "i" 1); -by Auto_tac; -qed_spec_mp "genPrefix_imp_nth"; - -Goal "ALL ys. length xs <= length ys \ -\ --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r) \ -\ --> (xs, ys) : genPrefix r"; -by (induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, - all_conj_distrib]))); -by (Clarify_tac 1); -by (case_tac "ys" 1); -by (ALLGOALS Force_tac); -qed_spec_mp "nth_imp_genPrefix"; - -Goal "((xs,ys) : genPrefix r) = \ -\ (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"; -by (blast_tac (claset() addIs [genPrefix_length_le, genPrefix_imp_nth, - nth_imp_genPrefix]) 1); -qed "genPrefix_iff_nth"; - - -(** <= is a partial order: **) - -AddIffs [reflexive_Id, antisym_Id, trans_Id]; - -Goalw [prefix_def] "xs <= (xs::'a list)"; -by (Simp_tac 1); -qed "prefix_refl"; -AddIffs[prefix_refl]; - -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"; -by (blast_tac (claset() addIs [genPrefix_trans]) 1); -qed "prefix_trans"; - -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"; -by (blast_tac (claset() addIs [genPrefix_antisym]) 1); -qed "prefix_antisym"; - -Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"; -by Auto_tac; -qed "prefix_less_le"; - -(*Monotonicity of "set" operator WRT prefix*) -Goalw [prefix_def] "xs <= ys ==> set xs <= set ys"; -by (etac genPrefix.induct 1); -by Auto_tac; -qed "set_mono"; - - -(** recursion equations **) - -Goalw [prefix_def] "[] <= xs"; -by (simp_tac (simpset() addsimps [Nil_genPrefix]) 1); -qed "Nil_prefix"; -AddIffs[Nil_prefix]; - -Goalw [prefix_def] "(xs <= []) = (xs = [])"; -by (simp_tac (simpset() addsimps [genPrefix_Nil]) 1); -qed "prefix_Nil"; -Addsimps [prefix_Nil]; - -Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; -by (Simp_tac 1); -qed"Cons_prefix_Cons"; -Addsimps [Cons_prefix_Cons]; - -Goalw [prefix_def] "(xs@ys <= xs@zs) = (ys <= zs)"; -by (Simp_tac 1); -qed "same_prefix_prefix"; -Addsimps [same_prefix_prefix]; - -AddIffs (* (xs@ys <= xs) = (ys <= []) *) - [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)]; - -Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs"; -by (etac genPrefix.append 1); -qed "prefix_appendI"; -Addsimps [prefix_appendI]; - -Goalw [prefix_def] - "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; -by (simp_tac (simpset() addsimps [genPrefix_Cons]) 1); -by Auto_tac; -qed "prefix_Cons"; - -Goalw [prefix_def] - "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"; -by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1); -qed "append_one_prefix"; - -Goalw [prefix_def] "xs <= ys ==> length xs <= length ys"; -by (etac genPrefix_length_le 1); -qed "prefix_length_le"; - -Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys"; -by (etac genPrefix.induct 1); -by Auto_tac; -val lemma = result(); - -Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys"; -by (blast_tac (claset() addIs [lemma RS mp]) 1); -qed "strict_prefix_length_less"; - -Goal "mono length"; -by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1); -qed "mono_length"; - -(*Equivalence to the definition used in Lex/Prefix.thy*) -Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)"; -by (auto_tac (claset(), - simpset() addsimps [genPrefix_iff_nth, nth_append])); -by (res_inst_tac [("x", "drop (length xs) zs")] exI 1); -by (rtac nth_equalityI 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append]))); -qed "prefix_iff"; - -Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; -by (simp_tac (simpset() addsimps [prefix_iff]) 1); -by (rtac iffI 1); - by (etac exE 1); - by (rename_tac "zs" 1); - by (res_inst_tac [("xs","zs")] rev_exhaust 1); - by (Asm_full_simp_tac 1); - by (hyp_subst_tac 1); - by (asm_full_simp_tac (simpset() delsimps [append_assoc] - addsimps [append_assoc RS sym])1); -by (Force_tac 1); -qed "prefix_snoc"; -Addsimps [prefix_snoc]; - -Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"; -by (res_inst_tac [("xs","zs")] rev_induct 1); - by (Force_tac 1); -by (asm_full_simp_tac (simpset() delsimps [append_assoc] - addsimps [append_assoc RS sym])1); -by (Force_tac 1); -qed "prefix_append_iff"; - -(*Although the prefix ordering is not linear, the prefixes of a list - are linearly ordered.*) -Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"; -by (res_inst_tac [("xs","zs")] rev_induct 1); -by Auto_tac; -qed_spec_mp "common_prefix_linear"; - - -(*** pfixLe, pfixGe: properties inherited from the translations ***) - -(** pfixLe **) - -Goalw [refl_def, Le_def] "reflexive Le"; -by Auto_tac; -qed "reflexive_Le"; - -Goalw [antisym_def, Le_def] "antisym Le"; -by Auto_tac; -qed "antisym_Le"; - -Goalw [trans_def, Le_def] "trans Le"; -by Auto_tac; -qed "trans_Le"; - -AddIffs [reflexive_Le, antisym_Le, trans_Le]; - -Goal "x pfixLe x"; -by (Simp_tac 1); -qed "pfixLe_refl"; -AddIffs[pfixLe_refl]; - -Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"; -by (blast_tac (claset() addIs [genPrefix_trans]) 1); -qed "pfixLe_trans"; - -Goal "[| x pfixLe y; y pfixLe x |] ==> x = y"; -by (blast_tac (claset() addIs [genPrefix_antisym]) 1); -qed "pfixLe_antisym"; - -Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys"; -by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1); -qed "prefix_imp_pfixLe"; - -Goalw [refl_def, Ge_def] "reflexive Ge"; -by Auto_tac; -qed "reflexive_Ge"; - -Goalw [antisym_def, Ge_def] "antisym Ge"; -by Auto_tac; -qed "antisym_Ge"; - -Goalw [trans_def, Ge_def] "trans Ge"; -by Auto_tac; -qed "trans_Ge"; - -AddIffs [reflexive_Ge, antisym_Ge, trans_Ge]; - -Goal "x pfixGe x"; -by (Simp_tac 1); -qed "pfixGe_refl"; -AddIffs[pfixGe_refl]; - -Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"; -by (blast_tac (claset() addIs [genPrefix_trans]) 1); -qed "pfixGe_trans"; - -Goal "[| x pfixGe y; y pfixGe x |] ==> x = y"; -by (blast_tac (claset() addIs [genPrefix_antisym]) 1); -qed "pfixGe_antisym"; - -Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys"; -by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1); -qed "prefix_imp_pfixGe"; - diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/GenPrefix.thy --- a/src/HOL/UNITY/GenPrefix.thy Thu Jan 30 18:08:09 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -(* Title: HOL/UNITY/GenPrefix.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Charpentier's Generalized Prefix Relation - (xs,ys) : genPrefix(r) - if ys = xs' @ zs where length xs = length xs' - and corresponding elements of xs, xs' are pairwise related by r - -Also overloads <= and < for lists! - -Based on Lex/Prefix -*) - -GenPrefix = Main + - -consts - genPrefix :: "('a * 'a)set => ('a list * 'a list)set" - -inductive "genPrefix(r)" - intrs - Nil "([],[]) : genPrefix(r)" - - prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> - (x#xs, y#ys) : genPrefix(r)" - - append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" - -instance list :: (type)ord - -defs - prefix_def "xs <= zs == (xs,zs) : genPrefix Id" - - strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" - - -(*Constants for the <= and >= relations, used below in translations*) -constdefs - Le :: "(nat*nat) set" - "Le == {(x,y). x <= y}" - - Ge :: "(nat*nat) set" - "Ge == {(x,y). y <= x}" - -syntax - pfixLe :: [nat list, nat list] => bool (infixl "pfixLe" 50) - pfixGe :: [nat list, nat list] => bool (infixl "pfixGe" 50) - -translations - "xs pfixLe ys" == "(xs,ys) : genPrefix Le" - - "xs pfixGe ys" == "(xs,ys) : genPrefix Ge" - -end diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Guar.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,8 +3,6 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge -Guarantees, etc. - From Chandy and Sanders, "Reasoning About Program Composition", Technical Report 2000-003, University of Florida, 2000. @@ -18,6 +16,8 @@ *) +header{*Guarantees Specifications*} + theory Guar = Comp: instance program :: (type) order @@ -80,7 +80,7 @@ (*** existential properties ***) -lemma ex1 [rule_format (no_asm)]: +lemma ex1 [rule_format]: "[| ex_prop X; finite GG |] ==> GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X" apply (unfold ex_prop_def) diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Lift_prog.thy Fri Jan 31 20:12:44 2003 +0100 @@ -6,6 +6,8 @@ lift_prog, etc: replication of components and arrays of processes. *) +header{*Replication of Components*} + theory Lift_prog = Rename: constdefs @@ -38,9 +40,7 @@ declare insert_map_def [simp] delete_map_def [simp] lemma insert_map_inverse: "delete_map i (insert_map i x f) = f" -apply (rule ext) -apply (simp (no_asm)) -done +by (rule ext, simp) lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)" apply (rule ext) @@ -50,13 +50,11 @@ (*** Injectiveness proof ***) lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y" -apply (drule_tac x = i in fun_cong) -apply (simp (no_asm_use)) -done +by (drule_tac x = i in fun_cong, simp) lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g" apply (drule_tac f = "delete_map i" in arg_cong) -apply (simp (no_asm_use) add: insert_map_inverse) +apply (simp add: insert_map_inverse) done lemma insert_map_inject': @@ -69,8 +67,7 @@ lemma lift_map_eq_iff [iff]: "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) = (uu = uu' & insert_map i s f = insert_map i' s' f')" -apply (unfold lift_map_def, auto) -done +by (unfold lift_map_def, auto) (*The !!s allows the automatic splitting of the bound variable*) lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s" @@ -91,9 +88,7 @@ done lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'" -apply (drule_tac f = "lift_map i" in arg_cong) -apply (simp (no_asm_use)) -done +by (drule_tac f = "lift_map i" in arg_cong, simp) lemma surj_lift_map: "surj (lift_map i)" apply (rule surjI) @@ -101,8 +96,7 @@ done lemma bij_lift_map [iff]: "bij (lift_map i)" -apply (simp (no_asm) add: bij_def inj_lift_map surj_lift_map) -done +by (simp add: bij_def inj_lift_map surj_lift_map) lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i" by (rule inv_equality, auto) @@ -115,8 +109,7 @@ (*sub's main property!*) lemma sub_apply [simp]: "sub i f = f i" -apply (simp (no_asm) add: sub_def) -done +by (simp add: sub_def) (*** lift_set ***) @@ -131,7 +124,7 @@ (*Do we really need both this one and its predecessor?*) lemma lift_set_iff2 [iff]: "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)" -by (simp (no_asm_simp) add: lift_set_def mem_rename_set_iff drop_map_def) +by (simp add: lift_set_def mem_rename_set_iff drop_map_def) lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B" @@ -141,7 +134,7 @@ lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B" apply (unfold lift_set_def) -apply (simp (no_asm_simp) add: image_Un) +apply (simp add: image_Un) done lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B" @@ -153,91 +146,71 @@ (*** the lattice operations ***) lemma bij_lift [iff]: "bij (lift i)" -apply (simp (no_asm) add: lift_def) -done +by (simp add: lift_def) lemma lift_SKIP [simp]: "lift i SKIP = SKIP" -apply (unfold lift_def) -apply (simp (no_asm_simp)) -done +by (simp add: lift_def) lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G" -apply (unfold lift_def) -apply (simp (no_asm_simp)) -done +by (simp add: lift_def) lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))" -apply (unfold lift_def) -apply (simp (no_asm_simp)) -done +by (simp add: lift_def) (*** Safety: co, stable, invariant ***) lemma lift_constrains: "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)" -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_constrains) -done +by (simp add: lift_def lift_set_def rename_constrains) lemma lift_stable: "(lift i F : stable (lift_set i A)) = (F : stable A)" -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_stable) -done +by (simp add: lift_def lift_set_def rename_stable) lemma lift_invariant: "(lift i F : invariant (lift_set i A)) = (F : invariant A)" apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_invariant) +apply (simp add: rename_invariant) done lemma lift_Constrains: "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)" apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_Constrains) +apply (simp add: rename_Constrains) done lemma lift_Stable: "(lift i F : Stable (lift_set i A)) = (F : Stable A)" apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_Stable) +apply (simp add: rename_Stable) done lemma lift_Always: "(lift i F : Always (lift_set i A)) = (F : Always A)" apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_Always) +apply (simp add: rename_Always) done (*** Progress: transient, ensures ***) lemma lift_transient: "(lift i F : transient (lift_set i A)) = (F : transient A)" - -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_transient) -done +by (simp add: lift_def lift_set_def rename_transient) lemma lift_ensures: "(lift i F : (lift_set i A) ensures (lift_set i B)) = (F : A ensures B)" -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_ensures) -done +by (simp add: lift_def lift_set_def rename_ensures) lemma lift_leadsTo: "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = (F : A leadsTo B)" -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_leadsTo) -done +by (simp add: lift_def lift_set_def rename_leadsTo) lemma lift_LeadsTo: "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = (F : A LeadsTo B)" -apply (unfold lift_def lift_set_def) -apply (simp (no_asm_simp) add: rename_LeadsTo) -done +by (simp add: lift_def lift_set_def rename_LeadsTo) (** guarantees **) @@ -245,10 +218,9 @@ lemma lift_lift_guarantees_eq: "(lift i F : (lift i ` X) guarantees (lift i ` Y)) = (F : X guarantees Y)" - apply (unfold lift_def) apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric]) -apply (simp (no_asm_simp) add: o_def) +apply (simp add: o_def) done lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) = @@ -266,14 +238,14 @@ change function components other than i*) lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd" apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD]) -apply (simp (no_asm_simp) add: lift_def rename_preserves) -apply (simp (no_asm_use) add: lift_map_def o_def split_def) +apply (simp add: lift_def rename_preserves) +apply (simp add: lift_map_def o_def split_def) done lemma delete_map_eqE': "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)" apply (drule_tac f = "insert_map i (g i) " in arg_cong) -apply (simp (no_asm_use) add: insert_map_delete_map_eq) +apply (simp add: insert_map_delete_map_eq) apply (erule exI) done @@ -302,7 +274,8 @@ lemma preserves_snd_lift_stable: "[| F : preserves snd; i~=j |] ==> lift j F : stable (lift_set i (A <*> UNIV))" -apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff) +apply (auto simp add: lift_def lift_set_def stable_def constrains_def + rename_def extend_def mem_rename_set_iff) apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def) apply (drule_tac x = i in fun_cong, auto) done @@ -315,7 +288,8 @@ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))" apply (case_tac "i=j") apply (simp add: lift_def lift_set_def rename_constrains) -apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], assumption) +apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], + assumption) apply (erule constrains_imp_subset [THEN lift_set_mono]) done @@ -329,8 +303,9 @@ (if i=j then insert_map i s f else if i UNIV) | A={})" apply (case_tac "i=j") apply (auto simp add: lift_transient) -apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act) +apply (auto simp add: lift_set_def lift_def transient_def rename_def + extend_def Domain_extend_act) apply (drule subsetD, blast, auto) apply (rename_tac s f uu s' f' uu') apply (subgoal_tac "f'=f & uu'=uu") @@ -387,7 +363,8 @@ (if i=j then F : preserves (v o fst) else True)" apply (drule subset_preserves_o [THEN subsetD]) apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq) -apply (simp cong del: if_weak_cong add: lift_map_def eq_commute split_def o_def, auto) +apply (auto cong del: if_weak_cong + simp add: lift_map_def eq_commute split_def o_def) done @@ -443,7 +420,7 @@ ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] ==> OK I (%i. lift i (F i))" apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend) -apply (simp (no_asm) add: Extend.AllowedActs_extend project_act_extend_act) +apply (simp add: Extend.AllowedActs_extend project_act_extend_act) apply (rename_tac "act") apply (subgoal_tac "{(x, x'). \s f u s' f' u'. @@ -468,6 +445,6 @@ lemma lift_image_preserves: "lift i ` preserves v = preserves (v o drop_map i)" -by (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq) +by (simp add: rename_image_preserves lift_def inv_lift_map_eq) end diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/ListOrder.thy --- a/src/HOL/UNITY/ListOrder.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/ListOrder.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,12 +3,425 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Lists are partially ordered by the prefix relation +Lists are partially ordered by Charpentier's Generalized Prefix Relation + (xs,ys) : genPrefix(r) + if ys = xs' @ zs where length xs = length xs' + and corresponding elements of xs, xs' are pairwise related by r + +Also overloads <= and < for lists! + +Based on Lex/Prefix *) -ListOrder = GenPrefix + +header {*The Prefix Ordering on Lists*} + +theory ListOrder = Main: + +consts + genPrefix :: "('a * 'a)set => ('a list * 'a list)set" + +inductive "genPrefix(r)" + intros + Nil: "([],[]) : genPrefix(r)" + + prepend: "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> + (x#xs, y#ys) : genPrefix(r)" + + append: "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" + +instance list :: (type)ord .. + +defs + prefix_def: "xs <= zs == (xs,zs) : genPrefix Id" + + strict_prefix_def: "xs < zs == xs <= zs & xs ~= (zs::'a list)" + + +(*Constants for the <= and >= relations, used below in translations*) +constdefs + Le :: "(nat*nat) set" + "Le == {(x,y). x <= y}" + + Ge :: "(nat*nat) set" + "Ge == {(x,y). y <= x}" + +syntax + pfixLe :: "[nat list, nat list] => bool" (infixl "pfixLe" 50) + pfixGe :: "[nat list, nat list] => bool" (infixl "pfixGe" 50) + +translations + "xs pfixLe ys" == "(xs,ys) : genPrefix Le" + + "xs pfixGe ys" == "(xs,ys) : genPrefix Ge" + + +subsection{*preliminary lemmas*} + +lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r" +by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto) + +lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys" +by (erule genPrefix.induct, auto) + +lemma cdlemma: + "[| (xs', ys'): genPrefix r |] + ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))" +apply (erule genPrefix.induct, blast, blast) +apply (force intro: genPrefix.append) +done + +(*As usual converting it to an elimination rule is tiresome*) +lemma cons_genPrefixE [elim!]: + "[| (x#xs, zs): genPrefix r; + !!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P + |] ==> P" +by (drule cdlemma, simp, blast) + +lemma Cons_genPrefix_Cons [iff]: + "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)" +by (blast intro: genPrefix.prepend) + + +subsection{*genPrefix is a partial order*} + +lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)" + +apply (unfold refl_def, auto) +apply (induct_tac "x") +prefer 2 apply (blast intro: genPrefix.prepend) +apply (blast intro: genPrefix.Nil) +done + +lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r" +by (erule reflD [OF refl_genPrefix UNIV_I]) + +lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s" +apply clarify +apply (erule genPrefix.induct) +apply (auto intro: genPrefix.append) +done + + +(** Transitivity **) + +(*A lemma for proving genPrefix_trans_O*) +lemma append_genPrefix [rule_format]: + "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r" +by (induct_tac "xs", auto) + +(*Lemma proving transitivity and more*) +lemma genPrefix_trans_O [rule_format]: + "(x, y) : genPrefix r + ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)" +apply (erule genPrefix.induct) + prefer 3 apply (blast dest: append_genPrefix) + prefer 2 apply (blast intro: genPrefix.prepend, blast) +done + +lemma genPrefix_trans [rule_format]: + "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] + ==> (x,z) : genPrefix r" +apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD]) + apply assumption +apply (blast intro: genPrefix_trans_O) +done + +lemma prefix_genPrefix_trans [rule_format]: + "[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r" +apply (unfold prefix_def) +apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption) +done + +lemma genPrefix_prefix_trans [rule_format]: + "[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r" +apply (unfold prefix_def) +apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption) +done + +lemma trans_genPrefix: "trans r ==> trans (genPrefix r)" +by (blast intro: transI genPrefix_trans) + + +(** Antisymmetry **) + +lemma genPrefix_antisym [rule_format]: + "[| (xs,ys) : genPrefix r; antisym r |] + ==> (ys,xs) : genPrefix r --> xs = ys" +apply (erule genPrefix.induct) + txt{*Base case*} + apply blast + txt{*prepend case*} + apply (simp add: antisym_def) +txt{*append case is the hardest*} +apply clarify +apply (subgoal_tac "length zs = 0", force) +apply (drule genPrefix_length_le)+ +apply (simp del: length_0_conv) +done + +lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)" +by (blast intro: antisymI genPrefix_antisym) + + +subsection{*recursion equations*} + +lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])" +apply (induct_tac "xs") +prefer 2 apply blast +apply simp +done + +lemma same_genPrefix_genPrefix [simp]: + "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)" +apply (unfold refl_def) +apply (induct_tac "xs") +apply (simp_all (no_asm_simp)) +done + +lemma genPrefix_Cons: + "((xs, y#ys) : genPrefix r) = + (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))" +by (case_tac "xs", auto) + +lemma genPrefix_take_append: + "[| reflexive r; (xs,ys) : genPrefix r |] + ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r" +apply (erule genPrefix.induct) +apply (frule_tac [3] genPrefix_length_le) +apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2]) +done + +lemma genPrefix_append_both: + "[| reflexive r; (xs,ys) : genPrefix r; length xs = length ys |] + ==> (xs@zs, ys @ zs) : genPrefix r" +apply (drule genPrefix_take_append, assumption) +apply (simp add: take_all) +done + + +(*NOT suitable for rewriting since [y] has the form y#ys*) +lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys" +by auto + +lemma aolemma: + "[| (xs,ys) : genPrefix r; reflexive r |] + ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r" +apply (erule genPrefix.induct) + apply blast + apply simp +txt{*Append case is hardest*} +apply simp +apply (frule genPrefix_length_le [THEN le_imp_less_or_eq]) +apply (erule disjE) +apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append) +apply (blast intro: genPrefix.append, auto) +apply (subst append_cons_eq) +apply (blast intro: genPrefix_append_both genPrefix.append) +done + +lemma append_one_genPrefix: + "[| (xs,ys) : genPrefix r; length xs < length ys; reflexive r |] + ==> (xs @ [ys ! length xs], ys) : genPrefix r" +by (blast intro: aolemma [THEN mp]) + + +(** Proving the equivalence with Charpentier's definition **) + +lemma genPrefix_imp_nth [rule_format]: + "ALL i ys. i < length xs + --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r" +apply (induct_tac "xs", auto) +apply (case_tac "i", auto) +done + +lemma nth_imp_genPrefix [rule_format]: + "ALL ys. length xs <= length ys + --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r) + --> (xs, ys) : genPrefix r" +apply (induct_tac "xs") +apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib) +apply clarify +apply (case_tac "ys") +apply (force+) +done + +lemma genPrefix_iff_nth: + "((xs,ys) : genPrefix r) = + (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))" +apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix) +done + + +subsection{*The type of lists is partially ordered*} + +declare reflexive_Id [iff] + antisym_Id [iff] + trans_Id [iff] + +lemma prefix_refl [iff]: "xs <= (xs::'a list)" +by (simp add: prefix_def) + +lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs" +apply (unfold prefix_def) +apply (blast intro: genPrefix_trans) +done + +lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys" +apply (unfold prefix_def) +apply (blast intro: genPrefix_antisym) +done + +lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)" +by (unfold strict_prefix_def, auto) instance list :: (type) order - (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le) + by (intro_classes, + (assumption | rule prefix_refl prefix_trans prefix_antisym + prefix_less_le)+) + +(*Monotonicity of "set" operator WRT prefix*) +lemma set_mono: "xs <= ys ==> set xs <= set ys" +apply (unfold prefix_def) +apply (erule genPrefix.induct, auto) +done + + +(** recursion equations **) + +lemma Nil_prefix [iff]: "[] <= xs" +apply (unfold prefix_def) +apply (simp add: Nil_genPrefix) +done + +lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" +apply (unfold prefix_def) +apply (simp add: genPrefix_Nil) +done + +lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" +by (simp add: prefix_def) + +lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)" +by (simp add: prefix_def) + +lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])" +by (insert same_prefix_prefix [of xs ys "[]"], simp) + +lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs" +apply (unfold prefix_def) +apply (erule genPrefix.append) +done + +lemma prefix_Cons: + "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))" +by (simp add: prefix_def genPrefix_Cons) + +lemma append_one_prefix: + "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys" +apply (unfold prefix_def) +apply (simp add: append_one_genPrefix) +done + +lemma prefix_length_le: "xs <= ys ==> length xs <= length ys" +apply (unfold prefix_def) +apply (erule genPrefix_length_le) +done + +lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys" +apply (unfold prefix_def) +apply (erule genPrefix.induct, auto) +done + +lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys" +apply (unfold strict_prefix_def) +apply (blast intro: splemma [THEN mp]) +done + +lemma mono_length: "mono length" +by (blast intro: monoI prefix_length_le) + +(*Equivalence to the definition used in Lex/Prefix.thy*) +lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)" +apply (unfold prefix_def) +apply (auto simp add: genPrefix_iff_nth nth_append) +apply (rule_tac x = "drop (length xs) zs" in exI) +apply (rule nth_equalityI) +apply (simp_all (no_asm_simp) add: nth_append) +done + +lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)" +apply (simp add: prefix_iff) +apply (rule iffI) + apply (erule exE) + apply (rename_tac "zs") + apply (rule_tac xs = zs in rev_exhaust) + apply simp + apply clarify + apply (simp del: append_assoc add: append_assoc [symmetric], force) +done + +lemma prefix_append_iff: + "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))" +apply (rule_tac xs = zs in rev_induct) + apply force +apply (simp del: append_assoc add: append_assoc [symmetric], force) +done + +(*Although the prefix ordering is not linear, the prefixes of a list + are linearly ordered.*) +lemma common_prefix_linear [rule_format]: + "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs" +by (rule_tac xs = zs in rev_induct, auto) + + +subsection{*pfixLe, pfixGe: properties inherited from the translations*} + +(** pfixLe **) + +lemma reflexive_Le [iff]: "reflexive Le" +by (unfold refl_def Le_def, auto) + +lemma antisym_Le [iff]: "antisym Le" +by (unfold antisym_def Le_def, auto) + +lemma trans_Le [iff]: "trans Le" +by (unfold trans_def Le_def, auto) + +lemma pfixLe_refl [iff]: "x pfixLe x" +by simp + +lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z" +by (blast intro: genPrefix_trans) + +lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y" +by (blast intro: genPrefix_antisym) + +lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys" +apply (unfold prefix_def Le_def) +apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) +done + +lemma reflexive_Ge [iff]: "reflexive Ge" +by (unfold refl_def Ge_def, auto) + +lemma antisym_Ge [iff]: "antisym Ge" +by (unfold antisym_def Ge_def, auto) + +lemma trans_Ge [iff]: "trans Ge" +by (unfold trans_def Ge_def, auto) + +lemma pfixGe_refl [iff]: "x pfixGe x" +by simp + +lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z" +by (blast intro: genPrefix_trans) + +lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y" +by (blast intro: genPrefix_antisym) + +lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys" +apply (unfold prefix_def Ge_def) +apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) +done end diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/PPROD.thy Fri Jan 31 20:12:44 2003 +0100 @@ -59,7 +59,8 @@ (** Safety & Progress: but are they used anywhere? **) -lemma PLam_constrains: "[| i : I; ALL j. F j : preserves snd |] ==> +lemma PLam_constrains: + "[| i : I; ALL j. F j : preserves snd |] ==> (PLam I F : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))) = (F i : (A <*> UNIV) co (B <*> UNIV))" @@ -69,25 +70,29 @@ apply (blast intro: constrains_imp_lift_constrains) done -lemma PLam_stable: "[| i : I; ALL j. F j : preserves snd |] +lemma PLam_stable: + "[| i : I; ALL j. F j : preserves snd |] ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = (F i : stable (A <*> UNIV))" apply (simp (no_asm_simp) add: stable_def PLam_constrains) done -lemma PLam_transient: "i : I ==> +lemma PLam_transient: + "i : I ==> PLam I F : transient A = (EX i:I. lift i (F i) : transient A)" apply (simp (no_asm_simp) add: JN_transient PLam_def) done (*This holds because the F j cannot change (lift_set i)*) -lemma PLam_ensures: "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); +lemma PLam_ensures: + "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); ALL j. F j : preserves snd |] ==> PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)" apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) done -lemma PLam_leadsTo_Basis: "[| i : I; +lemma PLam_leadsTo_Basis: + "[| i : I; F i : ((A <*> UNIV) - (B <*> UNIV)) co ((A <*> UNIV) Un (B <*> UNIV)); F i : transient ((A <*> UNIV) - (B <*> UNIV)); @@ -99,7 +104,8 @@ (** invariant **) -lemma invariant_imp_PLam_invariant: "[| F i : invariant (A <*> UNIV); i : I; +lemma invariant_imp_PLam_invariant: + "[| F i : invariant (A <*> UNIV); i : I; ALL j. F j : preserves snd |] ==> PLam I F : invariant (lift_set i (A <*> UNIV))" by (auto simp add: PLam_stable invariant_def) @@ -143,21 +149,24 @@ (**UNUSED (*The f0 premise ensures that the product is well-defined.*) - lemma PLam_invariant_imp_invariant: "[| PLam I F : invariant (lift_set i A); i : I; + lemma PLam_invariant_imp_invariant: + "[| PLam I F : invariant (lift_set i A); i : I; f0: Init (PLam I F) |] ==> F i : invariant A" apply (auto simp add: invariant_def) apply (drule_tac c = "f0 (i:=x) " in subsetD) apply auto done - lemma PLam_invariant: "[| i : I; f0: Init (PLam I F) |] + lemma PLam_invariant: + "[| i : I; f0: Init (PLam I F) |] ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)" apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant) done (*The f0 premise isn't needed if F is a constant program because then we get an initial state by replicating that of F*) - lemma reachable_PLam: "i : I + lemma reachable_PLam: + "i : I ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)" apply (auto simp add: invariant_def) done @@ -173,16 +182,17 @@ done (*Result to justify a re-organization of this file*) - lemma ??unknown??: "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))" - apply auto - result() + lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))" + by auto - lemma reachable_PLam_subset1: "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))" + lemma reachable_PLam_subset1: + "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))" apply (force dest!: reachable_PLam) done (*simplify using reachable_lift??*) - lemma reachable_lift_Join_PLam [rule_format (no_asm)]: "[| i ~: I; A : reachable (F i) |] + lemma reachable_lift_Join_PLam [rule_format]: + "[| i ~: I; A : reachable (F i) |] ==> ALL f. f : reachable (PLam I F) --> f(i:=A) : reachable (lift i (F i) Join PLam I F)" apply (erule reachable.induct) @@ -212,14 +222,16 @@ (*The index set must be finite: otherwise infinitely many copies of F can perform actions, and PLam can never catch up in finite time.*) - lemma reachable_PLam_subset2: "finite I + lemma reachable_PLam_subset2: + "finite I ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)" apply (erule finite_induct) apply (simp (no_asm)) apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert) done - lemma reachable_PLam_eq: "finite I ==> + lemma reachable_PLam_eq: + "finite I ==> reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))" apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2])) done @@ -227,7 +239,8 @@ (** Co **) - lemma Constrains_imp_PLam_Constrains: "[| F i : A Co B; i: I; finite I |] + lemma Constrains_imp_PLam_Constrains: + "[| F i : A Co B; i: I; finite I |] ==> PLam I F : (lift_set i A) Co (lift_set i B)" apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq) apply (auto simp add: constrains_def PLam_def) @@ -236,13 +249,15 @@ - lemma PLam_Constrains: "[| i: I; finite I; f0: Init (PLam I F) |] + lemma PLam_Constrains: + "[| i: I; finite I; f0: Init (PLam I F) |] ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = (F i : A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains) done - lemma PLam_Stable: "[| i: I; finite I; f0: Init (PLam I F) |] + lemma PLam_Stable: + "[| i: I; finite I; f0: Init (PLam I F) |] ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)" apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains) done @@ -250,13 +265,15 @@ (** const_PLam (no dependence on i) doesn't require the f0 premise **) - lemma const_PLam_Constrains: "[| i: I; finite I |] + lemma const_PLam_Constrains: + "[| i: I; finite I |] ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = (F : A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains) done - lemma const_PLam_Stable: "[| i: I; finite I |] + lemma const_PLam_Stable: + "[| i: I; finite I |] ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)" apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains) done diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Project.thy --- a/src/HOL/UNITY/Project.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Project.thy Fri Jan 31 20:12:44 2003 +0100 @@ -8,6 +8,8 @@ Inheritance of GUARANTEES properties under extension *) +header{*Projections of State Sets*} + theory Project = Extend: constdefs @@ -32,10 +34,10 @@ done -(** Safety **) +subsection{*Safety*} (*used below to prove Join_project_ensures*) -lemma (in Extend) project_unless [rule_format (no_asm)]: +lemma (in Extend) project_unless [rule_format]: "[| G : stable C; project h C G : A unless B |] ==> G : (C Int extend_set h A) unless (extend_set h B)" apply (simp add: unless_def project_constrains) @@ -98,7 +100,7 @@ by (simp add: project_constrains extend_constrains) -(*** "projecting" and union/intersection (no converses) ***) +subsection{*"projecting" and union/intersection (no converses)*} lemma projecting_Int: "[| projecting C h F XA' XA; projecting C h F XB' XB |] @@ -198,7 +200,7 @@ by (force simp only: extending_def Join_project_increasing) -(** Reachability and project **) +subsection{*Reachability and project*} (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_imp_reachable_project: @@ -247,7 +249,7 @@ done -(** Converse results for weak safety: benefits of the argument C *) +subsection{*Converse results for weak safety: benefits of the argument C *} (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_project_imp_reachable: @@ -329,8 +331,8 @@ apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) done -(** A lot of redundant theorems: all are proved to facilitate reasoning - about guarantees. **) +subsection{*A lot of redundant theorems: all are proved to facilitate reasoning + about guarantees.*} lemma (in Extend) projecting_Constrains: "projecting (%G. reachable (extend h F Join G)) h F @@ -390,9 +392,9 @@ done -(*** leadsETo in the precondition (??) ***) +subsection{*leadsETo in the precondition (??)*} -(** transient **) +subsubsection{*transient*} lemma (in Extend) transient_extend_set_imp_project_transient: "[| G : transient (C Int extend_set h A); G : stable C |] @@ -422,7 +424,7 @@ done -(** ensures -- a primitive combining progress with safety **) +subsubsection{*ensures -- a primitive combining progress with safety*} (*Used to prove project_leadsETo_I*) lemma (in Extend) ensures_extend_set_imp_project_ensures: @@ -456,7 +458,7 @@ done (*Used to prove project_leadsETo_D*) -lemma (in Extend) Join_project_ensures [rule_format (no_asm)]: +lemma (in Extend) Join_project_ensures [rule_format]: "[| project h C G ~: transient (A-B) | A<=B; extend h F Join G : stable C; F Join project h C G : A ensures B |] @@ -470,8 +472,8 @@ simp add: ensures_def Join_transient) done -(** Lemma useful for both STRONG and WEAK progress, but the transient - condition's very strong **) +text{*Lemma useful for both STRONG and WEAK progress, but the transient + condition's very strong*} (*The strange induction formula allows induction over the leadsTo assumption's non-atomic precondition*) @@ -505,7 +507,7 @@ project_set_reachable_extend_eq) -(*** Towards project_Ensures_D ***) +subsection{*Towards the theorem @{text project_Ensures_D}*} lemma (in Extend) act_subset_imp_project_act_subset: @@ -544,7 +546,7 @@ apply (force simp add: split_extended_all) done -lemma (in Extend) project_unless2 [rule_format (no_asm)]: +lemma (in Extend) project_unless2 [rule_format]: "[| G : stable C; project h C G : (project_set h C Int A) unless B |] ==> G : (C Int extend_set h A) unless (extend_set h B)" by (auto dest: stable_constrains_Int intro: constrains_weaken @@ -589,7 +591,7 @@ done -(*** Guarantees ***) +subsection{*Guarantees*} lemma (in Extend) project_act_Restrict_subset_project_act: "project_act h (Restrict C act) <= project_act h act" @@ -641,9 +643,9 @@ (*It seems that neither "guarantees" law can be proved from the other.*) -(*** guarantees corollaries ***) +subsection{*guarantees corollaries*} -(** Some could be deleted: the required versions are easy to prove **) +subsubsection{*Some could be deleted: the required versions are easy to prove*} lemma (in Extend) extend_guar_increasing: "[| F : UNIV guarantees increasing func; @@ -682,8 +684,8 @@ done -(** Guarantees with a leadsTo postcondition - THESE ARE ALL TOO WEAK because G can't affect F's variables at all**) +subsubsection{*Guarantees with a leadsTo postcondition + ALL TOO WEAK because G can't affect F's variables at all**) lemma (in Extend) project_leadsTo_D: "[| F Join project h UNIV G : A leadsTo B; diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Rename.thy --- a/src/HOL/UNITY/Rename.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Rename.thy Fri Jan 31 20:12:44 2003 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge +*) -Renaming of state sets -*) +header{*Renaming of State Sets*} theory Rename = Extend: @@ -42,7 +42,7 @@ by (simp add: rename_def) -(*** inverse properties ***) +subsection{*inverse properties*} lemma extend_set_inv: "bij h @@ -166,7 +166,7 @@ by (blast intro: bij_rename bij_rename_imp_bij) -(*** the lattice operations ***) +subsection{*the lattice operations*} lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP" by (simp add: rename_def Extend.extend_SKIP) @@ -180,7 +180,7 @@ by (simp add: rename_def Extend.extend_JN) -(*** Strong Safety: co, stable ***) +subsection{*Strong Safety: co, stable*} lemma rename_constrains: "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)" @@ -205,7 +205,7 @@ done -(*** Weak Safety: Co, Stable ***) +subsection{*Weak Safety: Co, Stable*} lemma reachable_rename_eq: "bij h ==> reachable (rename h F) = h ` (reachable F)" @@ -230,7 +230,7 @@ bij_is_surj [THEN surj_f_inv_f]) -(*** Progress: transient, ensures ***) +subsection{*Progress: transient, ensures*} lemma rename_transient: "bij h ==> (rename h F : transient (h`A)) = (F : transient A)" @@ -290,7 +290,7 @@ by (simp add: Extend.OK_extend_iff rename_def) -(*** "image" versions of the rules, for lifting "guarantees" properties ***) +subsection{*"image" versions of the rules, for lifting "guarantees" properties*} (*All the proofs are similar. Better would have been to prove one meta-theorem, but how can we handle the polymorphism? E.g. in diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Fri Jan 31 20:12:44 2003 +0100 @@ -6,6 +6,8 @@ Weak LeadsTo relation (restricted to the set of reachable states) *) +header{*Weak Progress*} + theory SubstAx = WFair + Constrains: constdefs @@ -27,7 +29,7 @@ done -(*** Specialized laws for handling invariants ***) +subsection{*Specialized laws for handling invariants*} (** Conjoining an Always property **) @@ -46,7 +48,7 @@ lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard] -(*** Introduction rules: Basis, Trans, Union ***) +subsection{*Introduction rules: Basis, Trans, Union*} lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B" apply (simp add: LeadsTo_def) @@ -67,7 +69,7 @@ done -(*** Derived rules ***) +subsection{*Derived rules*} lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV" by (simp add: LeadsTo_def) @@ -302,7 +304,7 @@ done -(*** Induction rules ***) +subsection{*Induction rules*} (** Meta or object quantifier ????? **) lemma LeadsTo_wf_induct: @@ -368,7 +370,7 @@ done -(*** Completion: Binary and General Finite versions ***) +subsection{*Completion: Binary and General Finite versions*} lemma Completion: "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C); diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/UNITY.thy Fri Jan 31 20:12:44 2003 +0100 @@ -8,6 +8,8 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) +header {*The Basic UNITY Theory*} + theory UNITY = Main: typedef (Program) diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/UNITY_Main.thy Fri Jan 31 20:12:44 2003 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2003 University of Cambridge +*) -Inclusive UNITY theory -*) +header{*Comprehensive UNITY Theory*} theory UNITY_Main = Detects + PPROD + Follows files "UNITY_tactics.ML": diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Jan 31 20:12:44 2003 +0100 @@ -6,6 +6,71 @@ Specialized UNITY tactics, and ML bindings of theorems *) +(*ListOrder*) +val Le_def = thm "Le_def"; +val Ge_def = thm "Ge_def"; +val prefix_def = thm "prefix_def"; +val Nil_genPrefix = thm "Nil_genPrefix"; +val genPrefix_length_le = thm "genPrefix_length_le"; +val cons_genPrefixE = thm "cons_genPrefixE"; +val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons"; +val refl_genPrefix = thm "refl_genPrefix"; +val genPrefix_refl = thm "genPrefix_refl"; +val genPrefix_mono = thm "genPrefix_mono"; +val append_genPrefix = thm "append_genPrefix"; +val genPrefix_trans_O = thm "genPrefix_trans_O"; +val genPrefix_trans = thm "genPrefix_trans"; +val prefix_genPrefix_trans = thm "prefix_genPrefix_trans"; +val genPrefix_prefix_trans = thm "genPrefix_prefix_trans"; +val trans_genPrefix = thm "trans_genPrefix"; +val genPrefix_antisym = thm "genPrefix_antisym"; +val antisym_genPrefix = thm "antisym_genPrefix"; +val genPrefix_Nil = thm "genPrefix_Nil"; +val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix"; +val genPrefix_Cons = thm "genPrefix_Cons"; +val genPrefix_take_append = thm "genPrefix_take_append"; +val genPrefix_append_both = thm "genPrefix_append_both"; +val append_cons_eq = thm "append_cons_eq"; +val append_one_genPrefix = thm "append_one_genPrefix"; +val genPrefix_imp_nth = thm "genPrefix_imp_nth"; +val nth_imp_genPrefix = thm "nth_imp_genPrefix"; +val genPrefix_iff_nth = thm "genPrefix_iff_nth"; +val prefix_refl = thm "prefix_refl"; +val prefix_trans = thm "prefix_trans"; +val prefix_antisym = thm "prefix_antisym"; +val prefix_less_le = thm "prefix_less_le"; +val set_mono = thm "set_mono"; +val Nil_prefix = thm "Nil_prefix"; +val prefix_Nil = thm "prefix_Nil"; +val Cons_prefix_Cons = thm "Cons_prefix_Cons"; +val same_prefix_prefix = thm "same_prefix_prefix"; +val append_prefix = thm "append_prefix"; +val prefix_appendI = thm "prefix_appendI"; +val prefix_Cons = thm "prefix_Cons"; +val append_one_prefix = thm "append_one_prefix"; +val prefix_length_le = thm "prefix_length_le"; +val strict_prefix_length_less = thm "strict_prefix_length_less"; +val mono_length = thm "mono_length"; +val prefix_iff = thm "prefix_iff"; +val prefix_snoc = thm "prefix_snoc"; +val prefix_append_iff = thm "prefix_append_iff"; +val common_prefix_linear = thm "common_prefix_linear"; +val reflexive_Le = thm "reflexive_Le"; +val antisym_Le = thm "antisym_Le"; +val trans_Le = thm "trans_Le"; +val pfixLe_refl = thm "pfixLe_refl"; +val pfixLe_trans = thm "pfixLe_trans"; +val pfixLe_antisym = thm "pfixLe_antisym"; +val prefix_imp_pfixLe = thm "prefix_imp_pfixLe"; +val reflexive_Ge = thm "reflexive_Ge"; +val antisym_Ge = thm "antisym_Ge"; +val trans_Ge = thm "trans_Ge"; +val pfixGe_refl = thm "pfixGe_refl"; +val pfixGe_trans = thm "pfixGe_trans"; +val pfixGe_antisym = thm "pfixGe_antisym"; +val prefix_imp_pfixGe = thm "prefix_imp_pfixGe"; + + (*UNITY*) val constrains_def = thm "constrains_def"; val stable_def = thm "stable_def"; @@ -105,7 +170,6 @@ val leadsTo_refl = thm "leadsTo_refl"; val empty_leadsTo = thm "empty_leadsTo"; val leadsTo_UNIV = thm "leadsTo_UNIV"; -val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma"; val leadsTo_induct_pre = thm "leadsTo_induct_pre"; val leadsTo_weaken_R = thm "leadsTo_weaken_R"; val leadsTo_weaken_L = thm "leadsTo_weaken_L"; @@ -127,7 +191,6 @@ val psp = thm "psp"; val psp2 = thm "psp2"; val psp_unless = thm "psp_unless"; -val leadsTo_wf_induct_lemma = thm "leadsTo_wf_induct_lemma"; val leadsTo_wf_induct = thm "leadsTo_wf_induct"; val bounded_induct = thm "bounded_induct"; val lessThan_induct = thm "lessThan_induct"; @@ -137,12 +200,9 @@ val leadsTo_subset = thm "leadsTo_subset"; val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt"; val wlt_increasing = thm "wlt_increasing"; -val lemma1 = thm "lemma1"; val leadsTo_123 = thm "leadsTo_123"; val wlt_constrains_wlt = thm "wlt_constrains_wlt"; -val completion_lemma = thm "completion_lemma"; val completion = thm "completion"; -val finite_completion_lemma = thm "finite_completion_lemma"; val finite_completion = thm "finite_completion"; val stable_completion = thm "stable_completion"; val finite_stable_completion = thm "finite_stable_completion"; @@ -276,7 +336,6 @@ val LessThan_bounded_induct = thm "LessThan_bounded_induct"; val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct"; val Completion = thm "Completion"; -val Finite_completion_lemma = thm "Finite_completion_lemma"; val Finite_completion = thm "Finite_completion"; val Stable_completion = thm "Stable_completion"; val Finite_stable_completion = thm "Finite_stable_completion"; @@ -670,12 +729,10 @@ val increasing_Un = thm "increasing_Un"; val Increasing_Un = thm "Increasing_Un"; val Always_Un = thm "Always_Un"; -val Follows_Un_lemma = thm "Follows_Un_lemma"; val Follows_Un = thm "Follows_Un"; val increasing_union = thm "increasing_union"; val Increasing_union = thm "Increasing_union"; val Always_union = thm "Always_union"; -val Follows_union_lemma = thm "Follows_union_lemma"; val Follows_union = thm "Follows_union"; val Follows_setsum = thm "Follows_setsum"; val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe"; diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/Union.thy Fri Jan 31 20:12:44 2003 +0100 @@ -3,11 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Unions of programs - Partly from Misra's Chapter 5: Asynchronous Compositions of Programs *) +header{*Unions of Programs*} + theory Union = SubstAx + FP: constdefs @@ -52,7 +52,7 @@ "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _:_./ _)" 10) -(** SKIP **) +subsection{*SKIP*} lemma Init_SKIP [simp]: "Init SKIP = UNIV" by (simp add: SKIP_def) @@ -66,7 +66,7 @@ lemma reachable_SKIP [simp]: "reachable SKIP = UNIV" by (force elim: reachable.induct intro: reachable.intros) -(** SKIP and safety properties **) +subsection{*SKIP and safety properties*} lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)" by (unfold constrains_def, auto) @@ -80,7 +80,7 @@ declare SKIP_in_stable [THEN stable_imp_Stable, iff] -(** Join **) +subsection{*Join*} lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G" by (simp add: Join_def) @@ -93,7 +93,7 @@ by (auto simp add: Join_def) -(** JN **) +subsection{*JN*} lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP" by (unfold JOIN_def SKIP_def, auto) @@ -119,7 +119,7 @@ by (simp add: JOIN_def) -(** Algebraic laws **) +subsection{*Algebraic laws*} lemma Join_commute: "F Join G = G Join F" by (simp add: Join_def Un_commute Int_commute) @@ -156,7 +156,7 @@ lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute -(*** JN laws ***) +subsection{*JN laws*} (*Also follows by JN_insert and insert_absorb, but the proof is longer*) lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)" @@ -183,7 +183,7 @@ done -(*** Safety: co, stable, FP ***) +subsection{*Safety: co, stable, FP*} (*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an alternative precondition is A<=B, but most proofs using this rule require @@ -245,7 +245,7 @@ by (simp add: FP_def JN_stable INTER_def) -(*** Progress: transient, ensures ***) +subsection{*Progress: transient, ensures*} lemma JN_transient: "i : I ==> @@ -313,7 +313,7 @@ done -(*** the ok and OK relations ***) +subsection{*the ok and OK relations*} lemma ok_SKIP1 [iff]: "SKIP ok F" by (auto simp add: ok_def) @@ -357,7 +357,7 @@ by (auto simp add: OK_iff_ok) -(*** Allowed ***) +subsection{*Allowed*} lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" by (auto simp add: Allowed_def) @@ -374,7 +374,8 @@ lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))" by (auto simp add: OK_iff_ok ok_iff_Allowed) -(*** safety_prop, for reasoning about given instances of "ok" ***) +subsection{*@{text safety_prop}, for reasoning about + given instances of "ok"*} lemma safety_prop_Acts_iff: "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)" diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Thu Jan 30 18:08:09 2003 +0100 +++ b/src/HOL/UNITY/WFair.thy Fri Jan 31 20:12:44 2003 +0100 @@ -8,6 +8,8 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) +header{*Progress under Weak Fairness*} + theory WFair = UNITY: constdefs @@ -51,11 +53,10 @@ "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\" 60) -(*** transient ***) +subsection{*transient*} lemma stable_transient_empty: "[| F : stable A; F : transient A |] ==> A = {}" - by (unfold stable_def constrains_def transient_def, blast) lemma transient_strengthen: @@ -81,7 +82,7 @@ by (unfold transient_def, auto) -(*** ensures ***) +subsection{*ensures*} lemma ensuresI: "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B" @@ -117,7 +118,7 @@ by (simp (no_asm) add: ensures_def unless_def) -(*** leadsTo ***) +subsection{*leadsTo*} lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B" apply (unfold leadsTo_def) @@ -235,7 +236,7 @@ lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'" by (blast intro: subset_imp_leadsTo leadsTo_Trans) -lemma leadsTo_weaken_L [rule_format (no_asm)]: +lemma leadsTo_weaken_L [rule_format]: "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'" by (blast intro: leadsTo_Trans subset_imp_leadsTo) @@ -372,7 +373,7 @@ done -(*** Proving the induction rules ***) +subsection{*Proving the induction rules*} (** The most general rule: r is any wf relation; f is any variant function **) @@ -449,7 +450,7 @@ done -(*** wlt ****) +subsection{*wlt*} (*Misra's property W3*) lemma wlt_leadsTo: "F : (wlt F B) leadsTo B" @@ -497,21 +498,33 @@ apply (auto intro: leadsTo_UN) (*Blast_tac says PROOF FAILED*) apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" - in constrains_UN [THEN constrains_weaken]) -apply (auto ); + in constrains_UN [THEN constrains_weaken], auto) done (*Misra's property W5*) lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)" -apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], clarify) -apply (subgoal_tac "Ba = wlt F B") -prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify) -apply (simp add: wlt_increasing Un_absorb2) -done +proof - + from wlt_leadsTo [of F B, THEN leadsTo_123] + show ?thesis + proof (elim exE conjE) +(* assumes have to be in exactly the form as in the goal displayed at + this point. Isar doesn't give you any automation. *) + fix C + assume wlt: "wlt F B \ C" + and lt: "F \ C leadsTo B" + and co: "F \ C - B co C \ B" + have eq: "C = wlt F B" + proof - + from lt and wlt show ?thesis + by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1]) + qed + from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2) + qed +qed -(*** Completion: Binary and General Finite versions ***) +subsection{*Completion: Binary and General Finite versions*} lemma completion_lemma : "[| W = wlt F (B' Un C);