src/HOLCF/IOA/meta_theory/Automata.ML

 (*  Title:      HOLCF/IOA/meta_theory/Automata.ML
     ID:         $Id$
     Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
-
-The I/O automata of Lynch and Tuttle.
 *)
 
 (* this modification of the simpset is local to this file *)
 Delsimps [split_paired_Ex];
 

 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
   by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
 qed "starts_of_par";
 
 Goal
-"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \       
+"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
 \            in (a:act A | a:act B) & \
-\               (if a:act A then       \                
-\                  (fst(s),a,fst(t)):trans_of(A) \                    
-\                else fst(t) = fst(s))            \                      
-\               &                                  \                     
-\               (if a:act B then                    \   
-\                  (snd(s),a,snd(t)):trans_of(B)     \                
+\               (if a:act A then       \
+\                  (fst(s),a,fst(t)):trans_of(A) \
+\                else fst(t) = fst(s))            \
+\               &                                  \
+\               (if a:act B then                    \
+\                  (snd(s),a,snd(t)):trans_of(B)     \
 \                else snd(t) = snd(s))}";
 
 by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
 qed "trans_of_par";
 

 (* ------------------------------------------------------------------------- *)
 
 section "actions and par";
 
 
-Goal 
+Goal
 "actions(asig_comp a b) = actions(a) Un actions(b)";
   by (simp_tac (simpset() addsimps
                ([actions_def,asig_comp_def]@asig_projections)) 1);
   by (fast_tac (set_cs addSIs [equalityI]) 1);
 qed "actions_asig_comp";

 
 Goal "ext (A1||A2) =    \
 \  (ext A1) Un (ext A2)";
 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,
       asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
-by (rtac set_ext 1); 
+by (rtac set_ext 1);
 by (fast_tac set_cs 1);
-qed"externals_of_par"; 
+qed"externals_of_par";
 
 Goal "act (A1||A2) =    \
 \  (act A1) Un (act A2)";
 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
       asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
-by (rtac set_ext 1); 
+by (rtac set_ext 1);
 by (fast_tac set_cs 1);
-qed"actions_of_par"; 
+qed"actions_of_par";
 
 Goal "inp (A1||A2) =\
 \         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
       asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
 qed"inputs_of_par";
-  
+
 Goal "out (A1||A2) =\
 \         (out A1) Un (out A2)";
 by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
       asig_outputs_def,Un_def,set_diff_def]) 1);
 qed"outputs_of_par";

       asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
 qed"internals_of_par";
 
 (* ------------------------------------------------------------------------ *)
 
-section "actions and compatibility"; 
+section "actions and compatibility";
 
 Goal"compatible A B = compatible B A";
 by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
 by Auto_tac;
 qed"compat_commute";

 by (Blast_tac 1);
 qed"inpAAactB_is_inpBoroutB";
 
 (* ------------------------------------------------------------------------- *)
 
-section "input_enabledness and par";  
-
-
-(* ugly case distinctions. Heart of proof: 
+section "input_enabledness and par";
+
+
+(* ugly case distinctions. Heart of proof:
      1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
      2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
-Goalw [input_enabled_def] 
+Goalw [input_enabled_def]
 "[| compatible A B; input_enabled A; input_enabled B|] \
 \     ==> input_enabled (A||B)";
 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);

 
 (* ------------------------------------------------------------------------- *)
 
 section "invariants";
 
-val [p1,p2] = goalw thy [invariant_def]
+val [p1,p2] = goalw (the_context ()) [invariant_def]
   "[| !!s. s:starts_of(A) ==> P(s);     \
 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
 \  ==> invariant A P";
 by (rtac allI 1);
 by (rtac impI 1);

 by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
 by (REPEAT (atac 1));
 qed"invariantI";
 
 
-val [p1,p2] = goal thy
+val [p1,p2] = goal (the_context ())
  "[| !!s. s : starts_of(A) ==> P(s); \
 \    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
 \ |] ==> invariant A P";
   by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
 qed "invariantI1";
 
 Goalw [invariant_def] "[| invariant A P; reachable A s |] ==> P(s)";
-by (Blast_tac 1);   
+by (Blast_tac 1);
 qed "invariantE";
 
 (* ------------------------------------------------------------------------- *)
 
 section "restrict";

 val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
 val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2,
                       trans_B_proj2,trans_AB_proj];
 
 
-Goal 
+Goal
 "((s,a,t) : trans_of(A || B || C || D)) =                                    \
 \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
 \   a:actions(asig_of(D))) &                                                 \
 \  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
 \   else fst t=fst s) &                                                      \

 qed "trans_of_par4";
 
 
 (* ------------------------------------------------------------------------- *)
 
-section "proof obligation generator for IOA requirements";  
+section "proof obligation generator for IOA requirements";
 
 (* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
 Goalw [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 [is_trans_of_def] 
+Goalw [is_trans_of_def]
 "is_trans_of A ==> is_trans_of (restrict A acts)";
 by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
 qed"is_trans_of_restrict";
 
-Goalw [is_trans_of_def,restrict_def,restrict_asig_def] 
+Goalw [is_trans_of_def,restrict_def,restrict_asig_def]
 "is_trans_of A ==> is_trans_of (rename A f)";
 by (asm_full_simp_tac
     (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);
+                         asig_outputs_def,asig_inputs_def,externals_def,
+                         asig_of_def,rename_def,rename_set_def]) 1);
 by (Blast_tac 1);
 qed"is_trans_of_rename";
 
 Goal "[| is_asig_of A; is_asig_of B; compatible A B|]  \
 \         ==> is_asig_of (A||B)";

 by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
 by Auto_tac;
 qed"is_asig_of_par";
 
 Goalw [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
-           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
+           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def]
 "is_asig_of A ==> is_asig_of (restrict A f)";
 by (Asm_full_simp_tac 1);
 by Auto_tac;
 qed"is_asig_of_restrict";
 
 Goal "is_asig_of A ==> is_asig_of (rename A f)";
 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
      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 Auto_tac;
 by   (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac));
 by   (ALLGOALS(Blast_tac));
 qed"is_asig_of_rename";
 
 

           is_trans_of_par,is_trans_of_restrict,is_trans_of_rename];
 
 
 Goalw [compatible_def]
 "[|compatible A B; compatible A C |]==> compatible A (B||C)";
-by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
+by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
    outputs_of_par,actions_of_par]) 1);
 by Auto_tac;
 qed"compatible_par";
 
 (*  better derive by previous one and compat_commute *)
 Goalw [compatible_def]
 "[|compatible A C; compatible B C |]==> compatible (A||B) C";
-by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
+by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
    outputs_of_par,actions_of_par]) 1);
 by Auto_tac;
 qed"compatible_par2";
 
 Goalw [compatible_def]