src/HOL/UNITY/Comp/Counter.ML
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
     1.1 --- a/src/HOL/UNITY/Comp/Counter.ML	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Counter.ML	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -11,11 +11,10 @@
     1.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     1.5  *)
     1.6  
     1.7 -Addsimps [Component_def RS def_prg_Init];
     1.8 -Addsimps (map simp_of_act  [a_def]);
     1.9 +Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
    1.10  
    1.11  (* Theorems about sum and sumj *)
    1.12 -Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
    1.13 +Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s";
    1.14  by (induct_tac "I" 1);
    1.15  by Auto_tac;
    1.16  qed_spec_mp "sum_upd_gt";
    1.17 @@ -47,7 +46,7 @@
    1.18      addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
    1.19  qed "sumj_upd_C";
    1.20  
    1.21 -Goal "ALL i. I<i--> (sumj I i s = sum I s)";
    1.22 +Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)";
    1.23  by (induct_tac "I" 1);
    1.24  by Auto_tac;
    1.25  qed_spec_mp  "sumj_sum_gt";
    1.26 @@ -58,49 +57,49 @@
    1.27  by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
    1.28  qed "sumj_sum_eq";
    1.29  
    1.30 -Goal "ALL i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    1.31 +Goal "\\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    1.32  by (induct_tac "I" 1);
    1.33  by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));  
    1.34  qed_spec_mp "sum_sumj";
    1.35  
    1.36  (* Correctness proofs for Components *)
    1.37  (* p2 and p3 proofs *)
    1.38 -Goal "Component i : stable {s. s C = s (c i) + k}";
    1.39 +Goal "Component i \\<in> stable {s. s C = s (c i) + k}";
    1.40  by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    1.41  by (constrains_tac 1);
    1.42  qed "p2";
    1.43  
    1.44 -Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
    1.45 +Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}";
    1.46  by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    1.47  by (constrains_tac 1);
    1.48  qed "p3";
    1.49  
    1.50  
    1.51  Goal 
    1.52 -"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
    1.53 -\                  Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
    1.54 -\  = (Component i: stable {s. s C = s (c i) + sumj I i s})";
    1.55 +"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
    1.56 +\                  \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
    1.57 +\  = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})";
    1.58 +by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1);
    1.59  by (auto_tac (claset(), simpset() 
    1.60 -     addsimps [constrains_def, stable_def,Component_def,
    1.61 -               sumj_upd_C, sumj_upd_ci]));
    1.62 +     addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci]));
    1.63  qed "p2_p3_lemma1";
    1.64  
    1.65  Goal 
    1.66 -"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
    1.67 -\                             {s. ALL v. v~=c i & v~=C --> s v = k v})";
    1.68 +"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
    1.69 +\                             {s. \\<forall>v. v~=c i & v~=C --> s v = k v})";
    1.70  by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    1.71  qed "p2_p3_lemma2";
    1.72  
    1.73  
    1.74  Goal 
    1.75 -"Component i: stable {s.  s C = s (c i) + sumj I i s}";
    1.76 +"Component i \\<in> stable {s.  s C = s (c i) + sumj I i s}";
    1.77  by (auto_tac (claset() addSIs [p2_p3_lemma2],
    1.78                simpset() addsimps [p2_p3_lemma1 RS sym]));
    1.79  qed "p2_p3";
    1.80  
    1.81  (* Compositional Proof *)
    1.82  
    1.83 -Goal "(ALL i. i < I --> s (c i) = 0) --> sum I s = 0";
    1.84 +Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0";
    1.85  by (induct_tac "I" 1);
    1.86  by Auto_tac;
    1.87  qed "sum_0'";
    1.88 @@ -108,33 +107,7 @@
    1.89  
    1.90  (* I could'nt be empty *)
    1.91  Goalw [invariant_def] 
    1.92 -"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
    1.93 -by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
    1.94 +"!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}";
    1.95 +by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1);
    1.96  by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
    1.97  qed "safety";
    1.98 -
    1.99 -
   1.100 -
   1.101 -
   1.102 -
   1.103 -
   1.104 -
   1.105 -
   1.106 -
   1.107 -
   1.108 -
   1.109 -
   1.110 -
   1.111 -
   1.112 -
   1.113 -
   1.114 -
   1.115 -
   1.116 -
   1.117 -
   1.118 -
   1.119 - 
   1.120 -
   1.121 -
   1.122 -
   1.123 -