src/HOLCF/IOA/meta_theory/SimCorrectness.ML

 section"properties of move";
 
 Delsimps [Let_def];
 
 Goalw [is_simulation_def]
-   "!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
 \     let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
 
 (* Does not perform conditional rewriting on assumptions automatically as
    usual. Instantiate all variables per hand. Ask Tobias?? *)

 
 
 Addsimps [Let_def];
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \    is_exec_frag A (s',@x. move A x s' a T')";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
 qed"move_subprop1_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \   Finite (@x. move A x s' a T')";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
 qed"move_subprop2_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \    laststate (s',@x. move A x s' a T') = T'";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
 qed"move_subprop3_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     mk_trace A`((@x. move A x s' a T')) = \
 \       (if a:ext A then a>>nil else nil)";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
 qed"move_subprop4_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     (t,T'):R";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);

                  Lemma 1 :Traces coincide  
    ------------------------------------------------------- *)
 
 Delsplits[split_if];
 Goal 
-  "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
+  "[|is_simulation R C A; ext C = ext A|] ==>  \     
 \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
 \            mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
 
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);
 (* cons case *) 

 (*               Lemma 2 : corresp_ex_sim is execution             *)
 (* ----------------------------------------------------------- *)
 
 
 Goal 
- "!!f.[| is_simulation R C A |] ==>\
+ "[| is_simulation R C A |] ==>\
 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R  \
 \ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')"; 
 
 by (Asm_full_simp_tac 1);
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);

      for the induction cases concerning the two lemmas correpsim_is_execution and 
      traces_coincide_sim, the second for the start state case. 
      S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
 
 Goal 
-"!!C. [| is_simulation R C A; s:starts_of C |] \
+"[| is_simulation R C A; s:starts_of C |] \
 \ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
 \     (s,S'):R & S':starts_of A";
   by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
          corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
   by (REPEAT (etac conjE 1));

 bind_thm("sim_starts1",(rewrite_rule [Let_def] simulation_starts) RS conjunct1);
 bind_thm("sim_starts2",(rewrite_rule [Let_def] simulation_starts) RS conjunct2);
 
 
 Goalw [traces_def]
-  "!!f. [| ext C = ext A; is_simulation R C A |] \
+  "[| ext C = ext A; is_simulation R C A |] \
 \          ==> traces C <= traces A"; 
 
   by (simp_tac(simpset() addsimps [has_trace_def2])1);
   by (safe_tac set_cs);