--- 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
--- 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 "\\<forall>n. I<n --> 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 "\\<forall>i. 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 "\\<forall>i. 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 \\<in> 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 \\<in> stable {s. \\<forall>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
-"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
-\ \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
-\ = (Component i \\<in> 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
-"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
-\ {s. \\<forall>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 \\<in> 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 "(\\<forall>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 ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> 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";
--- 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},
- \\<Union>G \\<in> preserves (%s. s (c i)). Acts G)"
+ \<Union>G \<in> 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)]: "\<forall>n. I<n --> 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)]: "\<forall>i. 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)]: "\<forall>i. 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 \<in> stable {s. s C = s (c i) + k}"
+apply (simp add: Component_def)
+apply constrains
+done
+
+lemma p3: "Component i \<in> stable {s. \<forall>v. v~=c i & v~=C --> s v = k v}"
+apply (simp add: Component_def)
+apply constrains
+done
+
+
+lemma p2_p3_lemma1:
+"(\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k}
+ \<inter> {s. \<forall>v. v~=c i & v~=C --> s v = k v}))
+ = (Component i \<in> 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:
+"\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} Int
+ {s. \<forall>v. v~=c i & v~=C --> s v = k v})"
+by (blast intro: stable_Int [OF p2 p3])
+
+lemma p2_p3: "Component i \<in> 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]: "(\<forall>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 ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> 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
--- 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 "\\<forall>i. 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<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 "(\\<forall>i. 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 "(\\<forall>j. j<I & j~=i --> 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 "(\\<forall>i. 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 \\<in> preserves (%s. c s i) & Component i \\<in> 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 \\<in> 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\\<in>I |] \
-\ ==> Component i \\<in> stable {s. \\<forall>j\\<in>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<I} Component; i<I |] ==> \
-\ \\<forall>k. Component i \\<in> stable ({s. C s = c s i + sumj I i k} Int \
-\ {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})";
-by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
-qed "p2_p3_lemma1";
-
-
-Goal "(\\<forall>k. F\\<in>stable ({s. C s = (c s) i + sumj I i k} Int \
-\ {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})) \
-\ ==> (F\\<in>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<I} Component; i<I |] \
-\ ==> Component i \\<in> 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; OK {i. i<I} Component |] \
-\ ==> (\\<Squnion>i\\<in>{i. i<I}. (Component i)) \\<in> 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";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- 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},
- \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
+ \<Union>G \<in> 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]: "\<forall>i. I<i--> (sum I s = sumj I i s)"
+by (induct_tac "I", auto)
+
+lemma sum_sumj_eq2 [rule_format]: "i<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]:
+ "(\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)"
+by (induct_tac "I", auto)
+
+lemma sumj_ext [rule_format]:
+ "(\<forall>j. j<I & j~=i --> 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]: "(\<forall>i. 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 \<in> preserves (%s. c s i) & Component i \<in> 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 \<in> stable {s. C s = (c s) i + k}"
+by (simp add: Component_def, constrains)
+
+lemma p3:
+ "[| OK I Component; i\<in>I |]
+ ==> Component i \<in> stable {s. \<forall>j\<in>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<I} Component; i<I |] ==>
+ \<forall>k. Component i \<in> stable ({s. C s = c s i + sumj I i k} Int
+ {s. \<forall>j\<in>{i. i<I}. j~=i --> c s j = c k j})"
+by (blast intro: stable_Int [OF p2 p3])
+
+lemma p2_p3_lemma2:
+ "(\<forall>k. F \<in> stable ({s. C s = (c s) i + sumj I i k} Int
+ {s. \<forall>j\<in>{i. i<I}. j~=i --> c s j = c k j}))
+ ==> (F \<in> 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<I} Component; i<I |]
+ ==> Component i \<in> 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; OK {i. i<I} Component |]
+ ==> (\<Squnion>i\<in>{i. i<I}. (Component i)) \<in> 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
--- 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:
- "\<forall>j. system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
-apply clarify
-apply (cut_tac i = j in reach_lemma)
+ "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>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 \<in> -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 \<in> 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 \<in> 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
--- 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 \\<dots>*)
-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";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- 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 \<union> (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 \<union> 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} \<inter> r) \<union> ({(x,y). x=i|y=i} \<inter> 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)) &
+ (\<forall>k k'. k\<noteq>i & k'\<noteq>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 \<dots>*}
+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 \<in> reach i q; derive1 k r q |] ==> x\<noteq>k --> x \<in> 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 \<subseteq> (reach i r \<union> {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 \<in> reach y r = y \<in> above x r *)
+lemma reach_above_lemma:
+ "(\<forall>i. reach i q \<subseteq> (reach i r \<union> {k})) =
+ (\<forall>x. x\<noteq>k --> (\<forall>i. i \<notin> above x r --> i \<notin> above x q))"
+by (auto simp add: trancl_converse)
+
+(* Lemma 2 *)
+lemma maximal_converse_image0:
+ "(z, i):r^+ ==> (\<forall>y. (y, z):r --> (y,i) \<notin> 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\<noteq>{}-->(\<exists>j \<in> 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\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})";
+apply (drule above_lemma_a)
+apply (auto simp add: image0_trancl_iff_image0_r)
+done
end