--- a/src/HOL/UNITY/Comp/Counter.thy Wed Jul 09 11:39:34 2003 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Wed Jul 09 12:41:47 2003 +0200
@@ -3,14 +3,14 @@
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.
*)
+header{*A Family of Similar Counters: Original Version*}
+
theory Counter = UNITY_Main:
(* Variables are names *)
@@ -46,10 +46,8 @@
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_gt [rule_format]: "\<forall>n. I<n --> sum I (s(c n := x)) = sum I s"
+by (induct_tac "I", auto)
lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
@@ -58,9 +56,7 @@
done
lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
-apply (induct_tac "I")
-apply auto
-done
+by (induct_tac "I", auto)
lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
apply (induct_tac "I")
@@ -72,18 +68,15 @@
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_gt [rule_format]: "\<forall>i. I<i--> (sumj I i s = sum I s)"
+by (induct_tac "I", auto)
lemma sumj_sum_eq: "(sumj I I s = sum I s)"
-apply (induct_tac "I")
-apply auto
+apply (induct_tac "I", 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)"
+lemma sum_sumj [rule_format]: "\<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
@@ -91,19 +84,15 @@
(* 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
+by (simp add: Component_def, constrains)
-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 p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"
+by (simp add: Component_def, constrains)
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}))
+ \<inter> {s. \<forall>v. v\<noteq>c i & v\<noteq>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)
@@ -111,25 +100,21 @@
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})"
+ {s. \<forall>v. v\<noteq>c i & v\<noteq>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
+by (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric])
(* 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
+by (induct_tac "I", auto)
-(* 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)
+(* I cannot be empty *)
+lemma safety:
+ "0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}"
+apply (simp (no_asm) add: invariant_def JN_stable sum_sumj)
apply (force intro: p2_p3 sum_0')
done
--- a/src/HOL/UNITY/Comp/Counterc.thy Wed Jul 09 11:39:34 2003 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy Wed Jul 09 12:41:47 2003 +0200
@@ -11,6 +11,8 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
+header{*A Family of Similar Counters: Version with Compatibility*}
+
theory Counterc = UNITY_Main:
typedecl state
@@ -62,7 +64,7 @@
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)"
+ "(\<forall>j. j<I & j\<noteq>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
@@ -89,7 +91,7 @@
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}"
+ ==> Component i \<in> stable {s. \<forall>j\<in>I. j\<noteq>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)
@@ -100,12 +102,12 @@
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})"
+ {s. \<forall>j\<in>{i. i<I}. j\<noteq>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}))
+ {s. \<forall>j\<in>{i. i<I}. j\<noteq>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)
@@ -122,8 +124,7 @@
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 (simp (no_asm) add: invariant_def JN_stable sum_sumj_eq2)
apply (auto intro!: sum0 p2_p3)
done