# HG changeset patch # User paulson # Date 1057229808 -7200 # Node ID 61bd46feb919d7b428aa63f0453734fe64c5ff4c # Parent cb07c394866865171b9d526e2bca99dde420c7f9 converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp) diff -r cb07c3948668 -r 61bd46feb919 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jul 03 10:37:25 2003 +0200 +++ b/src/HOL/IsaMakefile Thu Jul 03 12:56:48 2003 +0200 @@ -391,9 +391,8 @@ UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.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 \ - UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \ + UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \ + UNITY/Comp/PriorityAux.thy \ UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ UNITY/Comp/TimerArray.thy @$(ISATOOL) usedir $(OUT)/HOL UNITY diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/Counter.ML --- a/src/HOL/UNITY/Comp/Counter.ML Thu Jul 03 10:37:25 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,113 +0,0 @@ -(* Title: HOL/UNITY/Counter - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -A family of similar counters, version close to the original. - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init, simp_of_act a_def]; - -(* Theorems about sum and sumj *) -Goal "\\n. I sum I (s(c n := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sum_upd_gt"; - - -Goal "sum I (s(c I := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() - addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1); -qed "sum_upd_eq"; - -Goal "sum I (s(C := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum_upd_C"; - -Goal "sumj I i (s(c i := x)) = sumj I i s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() addsimps - [rewrite_rule [fun_upd_def] sum_upd_eq]) 1); -qed "sumj_upd_ci"; - -Goal "sumj I i (s(C := x)) = sumj I i s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() - addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1); -qed "sumj_upd_C"; - -Goal "\\i. I (sumj I i s = sum I s)"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sumj_sum_gt"; - -Goal "(sumj I I s = sum I s)"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1); -qed "sumj_sum_eq"; - -Goal "\\i. i(sum I s = s (c i) + sumj I i s)"; -by (induct_tac "I" 1); -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq])); -qed_spec_mp "sum_sumj"; - -(* Correctness proofs for Components *) -(* p2 and p3 proofs *) -Goal "Component i \\ stable {s. s C = s (c i) + k}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -qed "p2"; - -Goal "Component i \\ stable {s. \\v. v~=c i & v~=C --> s v = k v}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -qed "p3"; - - -Goal -"(\\k. Component i \\ stable ({s. s C = s (c i) + sumj I i k} \ -\ \\ {s. \\v. v~=c i & v~=C --> s v = k v})) \ -\ = (Component i \\ stable {s. s C = s (c i) + sumj I i s})"; -by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1); -by (auto_tac (claset(), simpset() - addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci])); -qed "p2_p3_lemma1"; - -Goal -"\\k. Component i \\ stable ({s. s C = s (c i) + sumj I i k} Int \ -\ {s. \\v. v~=c i & v~=C --> s v = k v})"; -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); -qed "p2_p3_lemma2"; - - -Goal -"Component i \\ stable {s. s C = s (c i) + sumj I i s}"; -by (auto_tac (claset() addSIs [p2_p3_lemma2], - simpset() addsimps [p2_p3_lemma1 RS sym])); -qed "p2_p3"; - -(* Compositional Proof *) - -Goal "(\\i. i < I --> s (c i) = 0) --> sum I s = 0"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum_0'"; -val sum0_lemma = (sum_0' RS mp) RS sym; - -(* I could'nt be empty *) -Goalw [invariant_def] -"!!I. 0 (\\i \\ {i. i invariant {s. s C = sum I s}"; -by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1); -by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1); -qed "safety"; diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Thu Jul 03 10:37:25 2003 +0200 +++ b/src/HOL/UNITY/Comp/Counter.thy Thu Jul 03 12:56:48 2003 +0200 @@ -11,11 +11,11 @@ Spriner LNCS 1586 (1999), pages 1215-1227. *) -Counter = UNITY_Main + +theory Counter = UNITY_Main: (* Variables are names *) datatype name = C | c nat -types state = name=>int +types state = "name=>int" consts sum :: "[nat,state]=>int" @@ -38,6 +38,99 @@ Component :: "nat => state program" "Component i == mk_total_program({s. s C = 0 & s (c i) = 0}, {a i}, - \\G \\ preserves (%s. s (c i)). Acts G)" + \G \ preserves (%s. s (c i)). Acts G)" + + + +declare Component_def [THEN def_prg_Init, simp] +declare a_def [THEN def_act_simp, simp] + +(* Theorems about sum and sumj *) +lemma sum_upd_gt [rule_format (no_asm)]: "\n. I sum I (s(c n := x)) = sum I s" +apply (induct_tac "I") +apply auto +done + + +lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s" +apply (induct_tac "I") +apply (auto simp add: sum_upd_gt [unfolded fun_upd_def]) +done + +lemma sum_upd_C: "sum I (s(C := x)) = sum I s" +apply (induct_tac "I") +apply auto +done + +lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s" +apply (induct_tac "I") +apply (auto simp add: sum_upd_eq [unfolded fun_upd_def]) +done + +lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s" +apply (induct_tac "I") +apply (auto simp add: sum_upd_C [unfolded fun_upd_def]) +done + +lemma sumj_sum_gt [rule_format (no_asm)]: "\i. I (sumj I i s = sum I s)" +apply (induct_tac "I") +apply auto +done + +lemma sumj_sum_eq: "(sumj I I s = sum I s)" +apply (induct_tac "I") +apply auto +apply (simp (no_asm) add: sumj_sum_gt) +done + +lemma sum_sumj [rule_format (no_asm)]: "\i. i(sum I s = s (c i) + sumj I i s)" +apply (induct_tac "I") +apply (auto simp add: linorder_neq_iff sumj_sum_eq) +done + +(* Correctness proofs for Components *) +(* p2 and p3 proofs *) +lemma p2: "Component i \ stable {s. s C = s (c i) + k}" +apply (simp add: Component_def) +apply constrains +done + +lemma p3: "Component i \ stable {s. \v. v~=c i & v~=C --> s v = k v}" +apply (simp add: Component_def) +apply constrains +done + + +lemma p2_p3_lemma1: +"(\k. Component i \ stable ({s. s C = s (c i) + sumj I i k} + \ {s. \v. v~=c i & v~=C --> s v = k v})) + = (Component i \ stable {s. s C = s (c i) + sumj I i s})" +apply (simp add: Component_def mk_total_program_def) +apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci) +done + +lemma p2_p3_lemma2: +"\k. Component i \ stable ({s. s C = s (c i) + sumj I i k} Int + {s. \v. v~=c i & v~=C --> s v = k v})" +by (blast intro: stable_Int [OF p2 p3]) + +lemma p2_p3: "Component i \ stable {s. s C = s (c i) + sumj I i s}" +apply (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric]) +done + +(* Compositional Proof *) + +lemma sum_0' [rule_format]: "(\i. i < I --> s (c i) = 0) --> sum I s = 0" +apply (induct_tac "I") +apply auto +done + +(* I could'nt be empty *) +lemma safety: +"!!I. 0 (\i \ {i. i invariant {s. s C = sum I s}" +apply (unfold invariant_def) +apply (simp (no_asm) add: JN_stable sum_sumj) +apply (force intro: p2_p3 sum_0') +done end diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/Counterc.ML --- a/src/HOL/UNITY/Comp/Counterc.ML Thu Jul 03 10:37:25 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,126 +0,0 @@ -(* Title: HOL/UNITY/Counterc - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -A family of similar counters, version with a full use of "compatibility " - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init, - Component_def RS def_prg_AllowedActs, - simp_of_act a_def]; - -(* Theorems about sum and sumj *) -Goal "\\i. I (sum I s = sumj I i s)"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sum_sumj_eq1"; - -Goal "i sum I s = c s i + sumj I i s"; -by (induct_tac "I" 1); -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1])); -qed_spec_mp "sum_sumj_eq2"; - -Goal "(\\i. i c s' i = c s i) --> (sum I s' = sum I s)"; -by (induct_tac "I" 1 THEN Auto_tac); -qed_spec_mp "sum_ext"; - -Goal "(\\j. j c s' j = c s j) --> (sumj I i s' = sumj I i s)"; -by (induct_tac "I" 1); -by Safe_tac; -by (auto_tac (claset() addSIs [sum_ext], simpset())); -qed_spec_mp "sumj_ext"; - - -Goal "(\\i. i c s i = 0) --> sum I s = 0"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum0"; - - -(* Safety properties for Components *) - -Goal "(Component i ok G) = \ -\ (G \\ preserves (%s. c s i) & Component i \\ Allowed G)"; -by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, Component_def RS def_total_prg_Allowed])); -qed "Component_ok_iff"; -AddIffs [Component_ok_iff]; -AddIffs [OK_iff_ok]; -Addsimps [preserves_def]; - - -Goal "Component i \\ stable {s. C s = (c s) i + k}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -qed "p2"; - -Goal "[| OK I Component; i\\I |] \ -\ ==> Component i \\ stable {s. \\j\\I. j~=i --> c s j = c k j}"; -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (rewrite_goals_tac [Component_def, mk_total_program_def]); -by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1); -by (Blast_tac 1); -qed "p3"; - - -Goal -"[| OK {i. i \ -\ \\k. Component i \\ stable ({s. C s = c s i + sumj I i k} Int \ -\ {s. \\j\\{i. i c s j = c k j})"; -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); -qed "p2_p3_lemma1"; - - -Goal "(\\k. F\\stable ({s. C s = (c s) i + sumj I i k} Int \ -\ {s. \\j\\{i. i c s j = c k j})) \ -\ ==> (F\\stable {s. C s = c s i + sumj I i s})"; -by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1); -by (force_tac (claset() addSIs [sumj_ext], simpset()) 1); -qed "p2_p3_lemma2"; - - -Goal "[| OK {i. i Component i \\ stable {s. C s = c s i + sumj I i s}"; -by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1); -qed "p2_p3"; - - -(* Compositional correctness *) -Goalw [invariant_def] - "[| 0 (\\i\\{i. i invariant {s. C s = sum I s}"; -by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1); -by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3], - simpset())); -qed "safety"; - - - - - - - - - - - - - - - - - - - - - - - - - diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/Counterc.thy --- a/src/HOL/UNITY/Comp/Counterc.thy Thu Jul 03 10:37:25 2003 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.thy Thu Jul 03 12:56:48 2003 +0200 @@ -11,9 +11,9 @@ Spriner LNCS 1586 (1999), pages 1215-1227. *) -Counterc = UNITY_Main + +theory Counterc = UNITY_Main: -types state +typedecl state arities state :: type consts @@ -41,5 +41,90 @@ Component :: "nat => state program" "Component i == mk_total_program({s. C s = 0 & (c s) i = 0}, {a i}, - \\G \\ preserves (%s. (c s) i). Acts G)" + \G \ preserves (%s. (c s) i). Acts G)" + + +declare Component_def [THEN def_prg_Init, simp] +declare Component_def [THEN def_prg_AllowedActs, simp] +declare a_def [THEN def_act_simp, simp] + +(* Theorems about sum and sumj *) +lemma sum_sumj_eq1 [rule_format]: "\i. I (sum I s = sumj I i s)" +by (induct_tac "I", auto) + +lemma sum_sumj_eq2 [rule_format]: "i sum I s = c s i + sumj I i s" +apply (induct_tac "I") +apply (auto simp add: linorder_neq_iff sum_sumj_eq1) +done + +lemma sum_ext [rule_format]: + "(\i. i c s' i = c s i) --> (sum I s' = sum I s)" +by (induct_tac "I", auto) + +lemma sumj_ext [rule_format]: + "(\j. j c s' j = c s j) --> (sumj I i s' = sumj I i s)" +apply (induct_tac "I", safe) +apply (auto intro!: sum_ext) +done + + +lemma sum0 [rule_format]: "(\i. i c s i = 0) --> sum I s = 0" +by (induct_tac "I", auto) + + +(* Safety properties for Components *) + +lemma Component_ok_iff: + "(Component i ok G) = + (G \ preserves (%s. c s i) & Component i \ Allowed G)" +apply (auto simp add: ok_iff_Allowed Component_def [THEN def_total_prg_Allowed]) +done +declare Component_ok_iff [iff] +declare OK_iff_ok [iff] +declare preserves_def [simp] + + +lemma p2: "Component i \ stable {s. C s = (c s) i + k}" +by (simp add: Component_def, constrains) + +lemma p3: + "[| OK I Component; i\I |] + ==> Component i \ stable {s. \j\I. j~=i --> c s j = c k j}" +apply simp +apply (unfold Component_def mk_total_program_def) +apply (simp (no_asm_use) add: stable_def constrains_def) +apply blast +done + + +lemma p2_p3_lemma1: + "[| OK {i. i + \k. Component i \ stable ({s. C s = c s i + sumj I i k} Int + {s. \j\{i. i c s j = c k j})" +by (blast intro: stable_Int [OF p2 p3]) + +lemma p2_p3_lemma2: + "(\k. F \ stable ({s. C s = (c s) i + sumj I i k} Int + {s. \j\{i. i c s j = c k j})) + ==> (F \ stable {s. C s = c s i + sumj I i s})" +apply (simp add: constrains_def stable_def) +apply (force intro!: sumj_ext) +done + + +lemma p2_p3: + "[| OK {i. i Component i \ stable {s. C s = c s i + sumj I i s}" +by (blast intro: p2_p3_lemma1 [THEN p2_p3_lemma2]) + + +(* Compositional correctness *) +lemma safety: + "[| 0 (\i\{i. i invariant {s. C s = sum I s}" +apply (unfold invariant_def) +apply (simp (no_asm) add: JN_stable sum_sumj_eq2) +apply (auto intro!: sum0 p2_p3) +done + end diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 10:37:25 2003 +0200 +++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 12:56:48 2003 +0200 @@ -2,8 +2,6 @@ ID: $Id$ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge - - *) header{*The priority system*} @@ -128,17 +126,16 @@ (* property 14: the 'above set' of a Component that hasn't got priority doesn't increase *) lemma above_not_increase: - "\j. system \ -Highest i Int {s. j\above i s} co {s. j\above i s}" -apply clarify -apply (cut_tac i = j in reach_lemma) + "system \ -Highest i Int {s. j\above i s} co {s. j\above i s}" +apply (insert reach_lemma [of concl: j]) apply (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains) -apply (auto simp add: trancl_converse) +apply (simp add: trancl_converse, blast) done lemma above_not_increase': "system \ -Highest i Int {s. above i s = x} co {s. above i s <= x}" -apply (cut_tac i = i in above_not_increase) +apply (insert above_not_increase [of i]) apply (simp add: trancl_converse constrains_def, blast) done @@ -174,8 +171,7 @@ (* property 17: original one is an invariant *) lemma Acyclic_Maximal_stable: "system \ stable (Acyclic Int Maximal)" -apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) -done +by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) (* propert 5: existential property *) @@ -216,7 +212,7 @@ apply (rule leadsTo_UN) apply (rule single_leadsTo_I, clarify) apply (rule_tac x2 = "above i x" in above_decreases_lemma) -apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0) +apply (simp_all (no_asm_use) add: Highest_iff_above0) apply blast+ done @@ -249,7 +245,7 @@ lemma Progress: "system \ Acyclic leadsTo Highest i" apply (rule_tac f = "%s. above i s" in finite_psubset_induct) -apply (simp del: Highest_def above_def +apply (simp del: above_def add: Highest_iff_above0 vimage_def finite_psubset_def, clarify) apply (case_tac "m={}") apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L]) @@ -265,4 +261,4 @@ suffices that we start from a state which is finite and acyclic.*} -end \ No newline at end of file +end diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/PriorityAux.ML --- a/src/HOL/UNITY/Comp/PriorityAux.ML Thu Jul 03 10:37:25 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,116 +0,0 @@ -(* Title: HOL/UNITY/PriorityAux - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -Auxiliary definitions needed in Priority.thy -*) - -Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def, - above_def, reach_def, reverse_def, neighbors_def]; - -(*All vertex sets are finite \\*) -AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset]; - -(* and relatons over vertex are finite too *) -AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ] - MRS finite_Prod_UNIV] MRS finite_subset]; - - -(* The equalities (above i r = {}) = (A i r = {}) - and (reach i r = {}) = (R i r) rely on the following theorem *) - -Goal "((r^+)``{i} = {}) = (r``{i} = {})"; -by Auto_tac; -by (etac trancl_induct 1); -by Auto_tac; -qed "image0_trancl_iff_image0_r"; - -(* Another form usefull in some situation *) -Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)"; -by Auto_tac; -by (dtac (image0_trancl_iff_image0_r RS ssubst) 1); -by Auto_tac; -qed "image0_r_iff_image0_trancl"; - - -(* In finite universe acyclic coincides with wf *) -Goal -"!!r::(vertex*vertex)set. acyclic r = wf r"; -by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite])); -qed "acyclic_eq_wf"; - -(* derive and derive1 are equivalent *) -Goal "derive i r q = derive1 i r q"; -by Auto_tac; -qed "derive_derive1_eq"; - -(* Lemma 1 *) -Goalw [reach_def] -"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r"; -by (etac ImageE 1); -by (etac trancl_induct 1); -by (case_tac "i=k" 1); -by (auto_tac (claset() addIs [r_into_trancl], simpset())); -by (dres_inst_tac [("x", "y")] spec 1); -by (rotate_tac ~1 1); -by (dres_inst_tac [("x", "z")] spec 1); -by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset())); -qed "lemma1_a"; - -Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))"; -by (REPEAT(rtac allI 1)); -by (rtac impI 1); -by (rtac subsetI 1 THEN dtac lemma1_a 1); -by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq] - delsimps [reach_def, derive_def, derive1_def])); -qed "reach_lemma"; - -(* An other possible formulation of the above theorem based on - the equivalence x:reach y r = y:above x r *) -Goal -"(ALL i. reach i q <= (reach i r Un {k})) =\ -\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))"; -by (auto_tac (claset(), simpset() addsimps [trancl_converse])); -qed "reach_above_lemma"; - -(* Lemma 2 *) -Goal -"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})"; -by Auto_tac; -by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1); -by Auto_tac; -qed "maximal_converse_image0"; - -Goal - "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})"; -by (full_simp_tac (simpset() - addsimps [acyclic_eq_wf, wf_eq_minimal]) 1); -by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1); -by Auto_tac; -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() - addsimps [maximal_converse_image0, trancl_converse]) 1); -qed "above_lemma_a"; - - -Goal - "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})"; -by (dtac above_lemma_a 1); -by (auto_tac (claset(), simpset() - addsimps [image0_trancl_iff_image0_r])); -qed "above_lemma_b"; - - - - - - - - - - - - - - diff -r cb07c3948668 -r 61bd46feb919 src/HOL/UNITY/Comp/PriorityAux.thy --- a/src/HOL/UNITY/Comp/PriorityAux.thy Thu Jul 03 10:37:25 2003 +0200 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy Thu Jul 03 12:56:48 2003 +0200 @@ -6,19 +6,19 @@ Auxiliary definitions needed in Priority.thy *) -PriorityAux = UNITY_Main + +theory PriorityAux = UNITY_Main: -types vertex +typedecl vertex arities vertex :: type constdefs (* symmetric closure: removes the orientation of a relation *) symcl :: "(vertex*vertex)set=>(vertex*vertex)set" - "symcl r == r Un (r^-1)" + "symcl r == r \ (r^-1)" (* Neighbors of a vertex i *) neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" - "neighbors i r == ((r Un r^-1)``{i}) - {i}" + "neighbors i r == ((r \ r^-1)``{i}) - {i}" R :: "[vertex, (vertex*vertex)set]=>vertex set" "R i r == r``{i}" @@ -34,20 +34,107 @@ "above i r == ((r^-1)^+)``{i}" reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" - "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1" + "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" "derive1 i r q == symcl r = symcl q & - (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):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" "derive i r q == A i r = {} & (q = reverse i r)" -rules +axioms (* we assume that the universe of vertices is finite *) - finite_vertex_univ "finite (UNIV :: vertex set)" + finite_vertex_univ: "finite (UNIV :: vertex set)" + +declare derive_def [simp] derive1_def [simp] symcl_def [simp] + A_def [simp] R_def [simp] + above_def [simp] reach_def [simp] + reverse_def [simp] neighbors_def [simp] + +text{*All vertex sets are finite \*} +declare finite_subset [OF subset_UNIV finite_vertex_univ, iff] + +text{* and relatons over vertex are finite too *} + +lemmas finite_UNIV_Prod = + finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ] + +declare finite_subset [OF subset_UNIV finite_UNIV_Prod, iff] + + +(* The equalities (above i r = {}) = (A i r = {}) + and (reach i r = {}) = (R i r) rely on the following theorem *) + +lemma image0_trancl_iff_image0_r: "((r^+)``{i} = {}) = (r``{i} = {})" +apply auto +apply (erule trancl_induct, auto) +done + +(* Another form usefull in some situation *) +lemma image0_r_iff_image0_trancl: "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)" +apply auto +apply (drule image0_trancl_iff_image0_r [THEN ssubst], auto) +done + + +(* In finite universe acyclic coincides with wf *) +lemma acyclic_eq_wf: "!!r::(vertex*vertex)set. acyclic r = wf r" +by (auto simp add: wf_iff_acyclic_if_finite) + +(* derive and derive1 are equivalent *) +lemma derive_derive1_eq: "derive i r q = derive1 i r q" +by auto + +(* Lemma 1 *) +lemma lemma1_a: + "[| x \ reach i q; derive1 k r q |] ==> x\k --> x \ reach i r" +apply (unfold reach_def) +apply (erule ImageE) +apply (erule trancl_induct) + apply (case_tac "i=k", simp_all) + apply (blast intro: r_into_trancl, blast, clarify) +apply (drule_tac x = y in spec) +apply (drule_tac x = z in spec) +apply (blast dest: r_into_trancl intro: trancl_trans) +done + +lemma reach_lemma: "derive k r q ==> reach i q \ (reach i r \ {k})" +apply clarify +apply (drule lemma1_a) +apply (auto simp add: derive_derive1_eq + simp del: reach_def derive_def derive1_def) +done + +(* An other possible formulation of the above theorem based on + the equivalence x \ reach y r = y \ above x r *) +lemma reach_above_lemma: + "(\i. reach i q \ (reach i r \ {k})) = + (\x. x\k --> (\i. i \ above x r --> i \ above x q))" +by (auto simp add: trancl_converse) + +(* Lemma 2 *) +lemma maximal_converse_image0: + "(z, i):r^+ ==> (\y. (y, z):r --> (y,i) \ r^+) = ((r^-1)``{z}={})" +apply auto +apply (frule_tac r = r in trancl_into_trancl2, auto) +done + +lemma above_lemma_a: + "acyclic r ==> A i r\{}-->(\j \ above i r. A j r = {})" +apply (simp add: acyclic_eq_wf wf_eq_minimal) +apply (drule_tac x = " ((r^-1) ^+) ``{i}" in spec) +apply auto +apply (simp add: maximal_converse_image0 trancl_converse) +done + +lemma above_lemma_b: + "acyclic r ==> above i r\{}-->(\j \ above i r. above j r = {})"; +apply (drule above_lemma_a) +apply (auto simp add: image0_trancl_iff_image0_r) +done end