author paulson Wed, 09 Jul 2003 12:41:47 +0200 changeset 14094 33147ecac5f9 parent 14093 24382760fd89 child 14095 a1ba833d6b61
~= to neq
 src/HOL/UNITY/Comp/Counter.thy file | annotate | diff | comparison | revisions src/HOL/UNITY/Comp/Counterc.thy file | annotate | diff | comparison | revisions
```--- 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

-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)
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 constrains
-done

-lemma p3: "Component i \<in> stable {s. \<forall>v. v~=c i & v~=C --> s v = k v}"
-apply constrains
-done
+lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"

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 (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})"