# HG changeset patch # User paulson # Date 1099929230 -3600 # Node ID c18f5b076e5315f975e8f3edc8bcb4a8dec4d0ee # Parent 771af451a06226fabd794f0e28d092f8aeb996ac tidied comments diff -r 771af451a062 -r c18f5b076e53 src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Fri Nov 05 15:37:25 2004 +0100 +++ b/src/HOL/UNITY/Comp/Priority.thy Mon Nov 08 16:53:50 2004 +0100 @@ -17,27 +17,30 @@ types command = "vertex=>(state*state)set" consts - (* the initial state *) init :: "(vertex*vertex)set" + --{* the initial state *} + +text{*Following the definitions given in section 4.4 *} constdefs - (* from the definitions given in section 4.4 *) - (* i has highest priority in r *) highest :: "[vertex, (vertex*vertex)set]=>bool" "highest i r == A i r = {}" + --{* i has highest priority in r *} - (* i has lowest priority in r *) lowest :: "[vertex, (vertex*vertex)set]=>bool" "lowest i r == R i r = {}" + --{* i has lowest priority in r *} act :: command "act i == {(s, s'). s'=reverse i s & highest i s}" - (* All components start with the same initial state *) Component :: "vertex=>state program" "Component i == mk_total_program({init}, {act i}, UNIV)" + --{* All components start with the same initial state *} - (* Abbreviations *) + +text{*Some Abbreviations *} +constdefs Highest :: "vertex=>state set" "Highest i == {s. highest i s}" @@ -47,12 +50,13 @@ Acyclic :: "state set" "Acyclic == {s. acyclic s}" - (* Every above set has a maximal vertex: two equivalent defs. *) Maximal :: "state set" + --{* Every ``above'' set has a maximal vertex*} "Maximal == \i. {s. ~highest i s-->(\j \ above i s. highest j s)}" Maximal' :: "state set" + --{* Maximal vertex: equivalent definition*} "Maximal' == \i. Highest i Un (\j. {s. j \ above i s} Int Highest j)" @@ -78,16 +82,16 @@ subsection{*Component correctness proofs*} -(* neighbors is stable *) +text{* neighbors is stable *} lemma Component_neighbors_stable: "Component i \ stable {s. neighbors k s = n}" by (simp add: Component_def, constrains, auto) -(* property 4 *) +text{* property 4 *} lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}" by (simp add: Component_def, constrains) -(* property 5: charpentier and Chandy mistakenly express it as - 'transient Highest i'. Consider the case where i has neighbors *) +text{* property 5: charpentier and Chandy mistakenly express it as + 'transient Highest i'. Consider the case where i has neighbors *} lemma Component_yields_priority: "Component i: {s. neighbors i s \ {}} Int Highest i ensures - Highest i" @@ -95,23 +99,23 @@ apply (ensures_tac "act i", blast+) done -(* or better *) +text{* or better *} lemma Component_yields_priority': "Component i \ Highest i ensures Lowest i" apply (simp add: Component_def) apply (ensures_tac "act i", blast+) done -(* property 6: Component doesn't introduce cycle *) +text{* property 6: Component doesn't introduce cycle *} lemma Component_well_behaves: "Component i \ Highest i co Highest i Un Lowest i" by (simp add: Component_def, constrains, fast) -(* property 7: local axiom *) +text{* property 7: local axiom *} lemma locality: "Component i \ stable {s. \j k. j\i & k\i--> ((j,k):s) = b j k}" by (simp add: Component_def, constrains) subsection{*System properties*} -(* property 8: strictly universal *) +text{* property 8: strictly universal *} lemma Safety: "system \ stable Safety" apply (unfold Safety_def) @@ -119,12 +123,12 @@ apply (simp add: system_def, constrains, fast) done -(* property 13: universal *) +text{* property 13: universal *} lemma p13: "system \ {s. s = q} co {s. s=q} Un {s. \i. derive i q s}" by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast) -(* property 14: the 'above set' of a Component that hasn't got - priority doesn't increase *) +text{* property 14: the 'above set' of a Component that hasn't got + priority doesn't increase *} lemma above_not_increase: "system \ -Highest i Int {s. j\above i s} co {s. j\above i s}" apply (insert reach_lemma [of concl: j]) @@ -141,7 +145,7 @@ -(* p15: universal property: all Components well behave *) +text{* p15: universal property: all Components well behave *} lemma system_well_behaves [rule_format]: "\i. system \ Highest i co Highest i Un Lowest i" apply clarify @@ -169,23 +173,23 @@ apply (drule above_lemma_b, auto) done -(* property 17: original one is an invariant *) +text{* property 17: original one is an invariant *} lemma Acyclic_Maximal_stable: "system \ stable (Acyclic Int Maximal)" by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) -(* propert 5: existential property *) +text{* property 5: existential property *} lemma Highest_leadsTo_Lowest: "system \ Highest i leadsTo Lowest i" apply (simp add: system_def Component_def mk_total_program_def totalize_JN) apply (ensures_tac "act i", auto) done -(* a lowest i can never be in any abover set *) +text{* a lowest i can never be in any abover set *} lemma Lowest_above_subset: "Lowest i <= (\k. {s. i\above k s})" by (auto simp add: image0_r_iff_image0_trancl trancl_converse) -(* property 18: a simpler proof than the original, one which uses psp *) +text{* property 18: a simpler proof than the original, one which uses psp *} lemma Highest_escapes_above: "system \ Highest i leadsTo (\k. {s. i\above k s})" apply (rule leadsTo_weaken_R) apply (rule_tac [2] Lowest_above_subset) @@ -196,8 +200,9 @@ "system \ Highest j Int {s. j \ above i s} leadsTo {s. j\above i s}" by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) -(*** The main result: above set decreases ***) -(* The original proof of the following formula was wrong *) +subsection{*The main result: above set decreases*} + +text{* The original proof of the following formula was wrong *} lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" by (auto simp add: image0_trancl_iff_image0_r) diff -r 771af451a062 -r c18f5b076e53 src/HOL/UNITY/Comp/PriorityAux.thy --- a/src/HOL/UNITY/Comp/PriorityAux.thy Fri Nov 05 15:37:25 2004 +0100 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy Mon Nov 08 16:53:50 2004 +0100 @@ -6,19 +6,21 @@ Auxiliary definitions needed in Priority.thy *) -theory PriorityAux = UNITY_Main: +theory PriorityAux +imports "../UNITY_Main" +begin typedecl vertex arities vertex :: type constdefs - (* symmetric closure: removes the orientation of a relation *) symcl :: "(vertex*vertex)set=>(vertex*vertex)set" "symcl r == r \ (r^-1)" + --{* symmetric closure: removes the orientation of a relation*} - (* Neighbors of a vertex i *) neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" - "neighbors i r == ((r \ r^-1)``{i}) - {i}" + "neighbors i r == ((r \ r^-1)``{i}) - {i}" + --{* Neighbors of a vertex i *} R :: "[vertex, (vertex*vertex)set]=>vertex set" "R i r == r``{i}" @@ -26,9 +28,9 @@ A :: "[vertex, (vertex*vertex)set]=>vertex set" "A i r == (r^-1)``{i}" - (* reachable and above vertices: the original notation was R* and A* *) reach :: "[vertex, (vertex*vertex)set]=> vertex set" "reach i r == (r^+)``{i}" + --{* reachable and above vertices: the original notation was R* and A* *} above :: "[vertex, (vertex*vertex)set]=> vertex set" "above i r == ((r^-1)^+)``{i}" @@ -36,19 +38,19 @@ reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" "reverse i r == (r - {(x,y). x=i | y=i} \ r) \ ({(x,y). x=i|y=i} \ r)^-1" - (* The original definition *) derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" + --{* The original definition *} "derive1 i r q == symcl r = symcl q & (\k k'. k\i & k'\i -->((k,k'):r) = ((k,k'):q)) & A i r = {} & R i q = {}" - (* Our alternative definition *) derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" + --{* Our alternative definition *} "derive i r q == A i r = {} & (q = reverse i r)" axioms - (* we assume that the universe of vertices is finite *) finite_vertex_univ: "finite (UNIV :: vertex set)" + --{* we assume that the universe of vertices is finite *} declare derive_def [simp] derive1_def [simp] symcl_def [simp] A_def [simp] R_def [simp]