# HG changeset patch
# User paulson
# Date 1057747307 -7200
# Node ID 33147ecac5f90906bb09461902f15fc090db48bb
# Parent  24382760fd89f49d509d074d953f1bc46820eefb
~= to neq

diff -r 24382760fd89 -r 33147ecac5f9 src/HOL/UNITY/Comp/Counter.thy
--- 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
 
diff -r 24382760fd89 -r 33147ecac5f9 src/HOL/UNITY/Comp/Counterc.thy
--- 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