--- a/src/HOL/UNITY/Comp/Priority.ML Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/Comp/Priority.ML Thu Jan 30 10:35:56 2003 +0100
@@ -12,7 +12,6 @@
*)
Addsimps [Component_def RS def_prg_Init];
-program_defs_ref := [Component_def, system_def];
Addsimps [highest_def, lowest_def];
Addsimps [simp_of_act act_def];
Addsimps (map simp_of_set [Highest_def, Lowest_def]);
@@ -24,13 +23,14 @@
(* neighbors is stable *)
Goal "Component i: stable {s. neighbors k s = n}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "Component_neighbors_stable";
(* property 4 *)
-Goal
-"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
+Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "Component_waits_priority";
@@ -39,24 +39,28 @@
Goal
"Component i: {s. neighbors i s ~= {}} Int Highest i \
\ ensures - Highest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (ensures_tac "act i" 1);
by (REPEAT(Fast_tac 1));
qed "Component_yields_priority";
(* or better *)
Goal "Component i: Highest i ensures Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (ensures_tac "act i" 1);
by (REPEAT(Fast_tac 1));
qed "Component_yields_priority'";
(* property 6: Component doesn't introduce cycle *)
Goal "Component i: Highest i co Highest i Un Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
by (Fast_tac 1);
qed "Component_well_behaves";
(* property 7: local axiom *)
Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "locality";
@@ -64,16 +68,16 @@
(**** System properties ****)
(* property 8: strictly universal *)
-Goalw [Safety_def]
- "system: stable Safety";
+Goalw [Safety_def] "system: stable Safety";
by (rtac stable_INT 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
by (constrains_tac 1);
by (Fast_tac 1);
qed "Safety";
(* property 13: universal *)
-Goal
-"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
+Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by (Blast_tac 1);
qed "p13";
@@ -84,6 +88,7 @@
"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
by (Clarify_tac 1);
by (cut_inst_tac [("i", "j")] reach_lemma 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
qed "above_not_increase";
@@ -101,6 +106,7 @@
(* p15: universal property: all Components well behave *)
Goal "ALL i. system: Highest i co Highest i Un Lowest i";
by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "system_well_behaves";
@@ -141,6 +147,7 @@
(* propert 5: existential property *)
Goal "system: Highest i leadsTo Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
by (ensures_tac "act i" 1);
by (auto_tac (claset(), simpset() addsimps [Component_def]));
qed "Highest_leadsTo_Lowest";