# HG changeset patch
# User oheimb
# Date 893172054 -7200
# Node ID 0277a026f99d9bcf9575d5a8673695d000a558b3
# Parent  14cea5b1d12f33981e56fe87f35e10a389d2c2bf
made modifications of the simpset() local
significantly simplified (and stabilized) proof of is_asig_of_rename

diff -r 14cea5b1d12f -r 0277a026f99d src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Apr 21 17:20:28 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Apr 21 17:20:54 1998 +0200
@@ -6,10 +6,10 @@
 The I/O automata of Lynch and Tuttle.
 *)
 
-(* Has been removed from HOL-simpset, who knows why? *)
-Addsimps [Let_def];
+(* this modification of the simpset is local to this file *)
 Delsimps [split_paired_Ex];
 
+
 open reachable;
 
 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
@@ -171,7 +171,7 @@
 goalw thy [input_enabled_def] 
 "!!A. [| compatible A B; input_enabled A; input_enabled B|] \
 \     ==> input_enabled (A||B)";
-by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1);
+by (asm_full_simp_tac (simpset()addsimps[Let_def,inputs_of_par,trans_of_par])1);
 by (safe_tac set_cs);
 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2);
@@ -403,9 +403,8 @@
 section "proof obligation generator for IOA requirements";  
 
 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
-goalw thy [is_trans_of_def] 
-"is_trans_of (A||B)";
-by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1);
+goalw thy [is_trans_of_def] "is_trans_of (A||B)";
+by (simp_tac (simpset() addsimps [Let_def,actions_of_par,trans_of_par]) 1);
 qed"is_trans_of_par";
 
 goalw thy [is_trans_of_def] 
@@ -416,7 +415,7 @@
 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
 "!!A. is_trans_of A ==> is_trans_of (rename A f)";
 by (asm_full_simp_tac
-    (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
+    (simpset() addsimps [Let_def,actions_def,trans_of_def, asig_internals_def,
 			 asig_outputs_def,asig_inputs_def,externals_def,
 			 asig_of_def,rename_def,rename_set_def]) 1);
 by (Blast_tac 1);
@@ -445,18 +444,8 @@
      rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
      asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
 by Auto_tac; 
-by (dres_inst_tac [("s","Some xb")] sym 1);
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
-by (dres_inst_tac [("s","Some xb")] sym 1);
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
-by (dres_inst_tac [("s","Some xb")] sym 1);
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by   (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac));
+by   (ALLGOALS(best_tac (set_cs addEs [equalityCE])));
 qed"is_asig_of_rename";
 
 
@@ -488,4 +477,6 @@
           externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
 by (auto_tac (claset() addEs [equalityCE],simpset()));
 qed"compatible_restrict";
- 
\ No newline at end of file
+
+
+Addsimps [split_paired_Ex];