src/HOL/IOA/NTP/Correctness.ML
changeset 1328 9a449a91425d
parent 1266 3ae9fe3c0f68
child 1342 f6651b6b0482
--- a/src/HOL/IOA/NTP/Correctness.ML	Sun Nov 12 16:29:12 1995 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Mon Nov 13 12:06:57 1995 +0100
@@ -6,29 +6,21 @@
 The main correctness proof: Impl implements Spec
 *)
 
-open Impl;
-open Spec;
+
+open Impl Spec;
 
 val hom_ioas = [Spec.ioa_def, Spec.trans_def,
                 Sender.sender_trans_def,Receiver.receiver_trans_def]
                @ impl_ioas;
 
-Addsimps hom_ioas;
-
 val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
-                   Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
+                  Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
 
-val ss =
-  !simpset delsimps ([trans_of_def, starts_of_def, srch_asig_def,rsch_asig_def,
-                      asig_of_def, actions_def, srch_trans_def, rsch_trans_def,
-                      impl_def, srch_ioa_thm, rsch_ioa_thm, srch_ioa_def,
-                      rsch_ioa_def, Sender.sender_trans_def,
-                      Receiver.receiver_trans_def] @ set_lemmas);
+(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
 
-val ss' = !simpset delsimps [trans_of_def, srch_asig_def, rsch_asig_def,
-                             srch_trans_def, rsch_trans_def, asig_of_def,
-                             actions_def]
-                   addcongs [let_weak_cong];
+Delsimps [split_paired_All];
+
+val ss' = (!simpset addsimps hom_ioas);
 
 
 (* A lemma about restricting the action signature of the implementation
@@ -47,44 +39,50 @@
 \   | C_m_r => False          \
 \   | C_r_s => False          \
 \   | C_r_r(m) => False)";
- by(simp_tac (ss addcongs [if_weak_cong] 
-                 addsimps ([externals_def, restrict_def,
-                            restrict_asig_def, Spec.sig_def])) 1);
+ by(simp_tac (!simpset addsimps ([externals_def, restrict_def,
+                            restrict_asig_def, Spec.sig_def]
+                            @asig_projections)) 1);
 
   by(Action.action.induct_tac "a" 1);
-  by(ALLGOALS(simp_tac (ss addsimps (actions_def :: set_lemmas))));
+  by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
  (* 2 *)
-  by (simp_tac (ss addsimps impl_ioas) 1);
-  by (simp_tac (ss addsimps impl_asigs) 1);
-  by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1);
-  by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1); 
+  by (simp_tac (!simpset addsimps impl_ioas) 1);
+  by (simp_tac (!simpset addsimps impl_asigs) 1);
+  by (simp_tac (!simpset addsimps 
+             [asig_of_par, asig_comp_def]@asig_projections) 1);
+  by (simp_tac rename_ss 1); 
  (* 1 *)
-  by (simp_tac (ss addsimps impl_ioas) 1);
-  by (simp_tac (ss addsimps impl_asigs) 1); 
-  by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1);
-  by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1); 
+  by (simp_tac (!simpset addsimps impl_ioas) 1);
+  by (simp_tac (!simpset addsimps impl_asigs) 1);
+  by (simp_tac (!simpset addsimps 
+             [asig_of_par, asig_comp_def]@asig_projections) 1);
 qed "externals_lemma"; 
 
 
 val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def,
             Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def];
 
+
+
 (* Proof of correctness *)
 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]
   "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by(simp_tac (ss delsimps [trans_def] addsimps 
-             (Correctness.hom_def::[cancel_restrict,externals_lemma])) 1);
+by(simp_tac (!simpset addsimps 
+    [Correctness.hom_def,
+     cancel_restrict,externals_lemma]) 1);
 br conjI 1;
-by(simp_tac (ss addsimps impl_ioas) 1);
+by(simp_tac ss' 1);
 br ballI 1;
 bd CollectD 1;
 by(asm_simp_tac (!simpset addsimps sels) 1);
 by(REPEAT(rtac allI 1));
 br imp_conj_lemma 1;   (* from lemmas.ML *)
+
 by(Action.action.induct_tac "a"  1);
 by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
 by(forward_tac [inv4] 1);
-by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by(asm_full_simp_tac (!simpset addsimps 
+                 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
 by(simp_tac ss' 1);
 by(simp_tac ss' 1);
 by(simp_tac ss' 1);
@@ -97,8 +95,8 @@
 by(forward_tac [inv4] 1);
 by(forward_tac [inv2] 1);
 be disjE 1;
-by(asm_simp_tac ss 1);
-by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by(Asm_simp_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
 
 by(asm_simp_tac ss' 1);
 by(forward_tac [inv2] 1);
@@ -112,11 +110,11 @@
 
 by(case_tac "m = hd(sq(sen(s)))" 1);
 
-by(asm_full_simp_tac (ss addsimps 
+by(asm_full_simp_tac (!simpset addsimps 
                      [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
 
-by(asm_full_simp_tac ss 1);
+by(Asm_full_simp_tac 1);
 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
 
-by(asm_full_simp_tac ss 1);
+by(Asm_full_simp_tac 1);
 result();