(*  Title:      ISM/ISM.thy
    Id:         $Id: ISM.thy,v 1.34 2003/09/12 16:13:02 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2002 Siemens AG; any non-commercial use is granted

*)

header {* Interacting State Machines *}

theory ISM
imports Basis
begin

types ('p, 'm) msgss = "'p \<Rightarrow> 'm list"  --{* family of message lists,\\
i.e. i/o port contents or patterns @{typ 'm} indexed by port names @{typ 'p} *}
(*<*)
translations "(p, m) msgss" \<leftharpoondown> (type) "p \<Rightarrow> m list"
(*>*)
types ('c, 'p, 'm, 's, 'd) trans = "(('p,'m) msgss \<times> 's) \<times> ('c \<times> 'd) \<times> (('p,'m) msgss \<times> 's)"
--{* input pattern, local pre-state, command, output pattern, post-state *}

consts 
  "input" :: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> ('p, 'm) msgss"
 "output" :: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> ('p, 'm) msgss"
 "cmd"    :: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> 'c"
 "dom_of" :: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> 'd"
 "lstate" :: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> 's"
 "lstate'":: "('c, 'p, 'm, 's, 'd) trans \<Rightarrow> 's"
defs
   input_def : " input  \<equiv> fst \<circ> fst"
  output_def : "output  \<equiv> fst \<circ> snd \<circ> snd"
  cmd_def    : "cmd     \<equiv> fst \<circ> fst \<circ> snd"
  dom_of_def : "dom_of  \<equiv> snd \<circ> fst \<circ> snd"
  lstate_def : "lstate  \<equiv> snd \<circ> fst"
  lstate'_def: "lstate' \<equiv> snd \<circ> snd \<circ> snd"
(*<*)
declare input_def [simp] lstate_def  [simp] cmd_def    [simp] 
       output_def [simp] lstate'_def [simp] dom_of_def [simp]
(*>*)

record ('c, 'p, 'm, 's, 'd) "ism" = 
  "inputs" :: "'p set"                           --{* input  port names   *}
 "outputs" :: "'p set"                           --{* output port names   *}
 "init"    :: "'s"                               --{* initial local state *}
 "trans"   :: "(('c, 'p, 'm, 's, 'd) trans) set" --{* transitions         *}

(*<*)
lemma surjective_ism: 
 "a = \<lparr>inputs = inputs a, outputs = outputs a, init = init a, trans = trans a\<rparr>"
by simp

(*>*)
constdefs
  map_ism ::"('s \<Rightarrow> 't) \<Rightarrow> ('c, 'p, 'm, 's, 'd) ism \<Rightarrow> ('c, 'p, 'm, 't, 'd) ism"
 "map_ism f a \<equiv> \<lparr>inputs = inputs a, outputs = outputs a, init = f (init a), 
                 trans  = (upd_fst (upd_snd f) \<circ>
                           upd_snd (upd_snd (upd_snd f))) ` trans a\<rparr>"
(*<*)
lemma map_ism_conv [simp]: 
"\<And>tr. map_ism f \<lparr>inputs = inp, outputs = out, init = (  ini), trans = tr\<rparr> = 
                 \<lparr>inputs = inp, outputs = out, init = (f ini), trans = 
                      (\<lambda>((p,s),(c,d),(p',s')). ((p,f s),(c,d),(p',f s'))) ` tr\<rparr>"
by (auto simp add: map_ism_def upd_snd_def upd_fst_def 
         del: image_eqI intro!: image_eqI)

(*>*)

subsection "Renaming"

constdefs 
  ren_trans :: "'p \<Rightarrow> 'p \<Rightarrow> ('c, 'p, 'm, 's, 'd) trans \<Rightarrow> ('c, 'p, 'm, 's, 'd) trans"
 "ren_trans pn pn' \<equiv> \<lambda>((p,s),(c,d),(p',s')). ((lmap_subst pn pn' p ,s ),(c,d),
                                           (lmap_subst pn pn' p',s'))"

  subst_elem :: "'a \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
 "subst_elem x y A \<equiv> if x \<in> A then A - {x} \<union> {y} else A"

  ren_conn :: "'p \<Rightarrow> 'p \<Rightarrow> ('c, 'p, 'm, 's, 'd) ism \<Rightarrow> ('c, 'p, 'm, 's, 'd) ism"
 "ren_conn pn pn' a \<equiv> \<lparr>inputs  = subst_elem pn pn' ( inputs a),
                       outputs = subst_elem pn pn' (outputs a),
                       init = init a, trans = ren_trans pn pn' ` trans a\<rparr>"


subsection "Well-formedness"

consts 
  ipns :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> 'p set" --{* potential  input port names *}
  opns :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> 'p set" --{* potential output port names *}
defs
  ipns_def : "ipns a \<equiv> \<Union>lmap_dom`( input`trans a)"
  opns_def : "opns a \<equiv> \<Union>lmap_dom`(output`trans a)"
constdefs 
  wf_ism :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> bool"
 "wf_ism a \<equiv> ipns a \<subseteq> inputs a \<and> opns a \<subseteq> outputs a"
--{* input and output may overlap ($\leadsto$ direct feedback) *}
(*<*)
 lemma wf_ismI: 
  "\<lbrakk>\<And>p s c d p' s' pn. \<lbrakk>((p, s), (c, d), (p', s')) \<in> t; p   pn \<noteq> []\<rbrakk> \<Longrightarrow> pn \<in> Is;
    \<And>p s c d p' s' pn. \<lbrakk>((p, s), (c, d), (p', s')) \<in> t; p'  pn \<noteq> []\<rbrakk> \<Longrightarrow> pn \<in> Os\<rbrakk> \<Longrightarrow> 
  wf_ism \<lparr>inputs = Is, outputs = Os, init = i, trans = t\<rparr>"
by (auto simp add: wf_ism_def ipns_def opns_def)

lemma wf_ism_trans_in_inputs: 
  "\<lbrakk>wf_ism a; ((p, s), c_d_p'_s') \<in> trans a\<rbrakk> \<Longrightarrow> lmap_dom p \<subseteq> inputs a"
apply (clarsimp simp add: wf_ism_def ipns_def UN_subset_iff)
apply (erule rev_ballE, fast)
apply (auto simp add: lmap_dom_def)
done
lemma wf_ism_trans_in_outputs: 
  "\<lbrakk>wf_ism a; (p_s, c_d, (p',s')) \<in> trans a\<rbrakk> \<Longrightarrow> lmap_dom p' \<subseteq> outputs a"
apply (clarsimp simp add: wf_ism_def opns_def UN_subset_iff)
apply (erule rev_ballE, fast)
apply (auto simp add: lmap_dom_def)
done

(*>*)
text {*\pagebreak*}
subsection "Runs"

consts 
  runs :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> ('s list) set"
inductive "runs a" intros  --{* ignoring commands and global state! *}
--{* for technical reasons, traces are built from right to left *}
 "init": "[init a] \<in> runs a"
 "step": "\<lbrakk>s#ss \<in> runs a; 
           ((p,s),(c,d),(p',s')) \<in> trans a
          \<rbrakk> \<Longrightarrow> s'#s#ss \<in> runs a"
-- {* Communication with the environment is unrestricted ($\leadsto$ arbitrary input). *}
(*<*)
inductive_cases runs_elim_cases: "ss \<in> runs a"
ML_setup
{* bind_thm ("runs_step2", rearrange_prems [1,0] (thm "runs.step")) *}
(*>*)

types ('c, 'p, 'm, 's, 'd) truns = "((('c, 'p, 'm, 's, 'd) trans) list) set"
consts 
  truns :: "('c, 'p, 'm, 's, 'd) ism  \<Rightarrow> ('c, 'p, 'm, 's, 'd) truns"
inductive "truns a" intros
--{* for technical reasons, traces are built from right to left *}
 "init": "((p,init a),c,c2) \<in> trans a \<Longrightarrow> [((p,init a),c,c2)] \<in> truns a"
 "step": "\<lbrakk>(c0,c',(p1,s1))#ts \<in> truns a; 
           ((p1,s1),c,c2) \<in> trans a\<rbrakk> \<Longrightarrow> 
           ((p1,s1),c,c2)#(c0,c',(p1,s1))#ts \<in> truns a"

lemma truns2trans [rule_format]: "ts \<in> truns a \<Longrightarrow> \<forall>t \<in> set ts. t \<in> trans a"
(*<*)
by (erule truns.induct, auto)
(*>*)

constdefs 
   truns2runs :: "(('c, 'p, 'm, 's, 'd) trans) list \<Rightarrow> 's list"
  "truns2runs ts \<equiv> lstate'(hd ts)#map lstate ts"

lemma truns2runs [rule_format]: "ts \<in> truns a \<Longrightarrow> truns2runs ts \<in> runs a"
(*<*)
by (erule truns.induct, 
    auto simp add: truns2runs_def intro: runs.intros)
(*>*)

lemma lstate_in_truns2runs: "t \<in> set ts \<Longrightarrow> lstate t \<in> set (truns2runs ts)"
(*<*)
by (simp add: truns2runs_def)
(*>*)

subsection "Reachability and invariants"

constdefs
  reach :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> 's set"
 "reach a \<equiv> \<Union>set`runs a"

  inv :: "('c, 'p, 'm, 's, 'd) ism \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool"
 "inv a P \<equiv> \<forall>s \<in> reach a. P s"

lemma invI: 
"\<lbrakk>P (init a); 
  \<And>x p s c d p' s'. \<lbrakk>s \<in> reach a; P s; ((p,s),(c,d),(p',s')) \<in> trans a\<rbrakk> \<Longrightarrow> P s'
 \<rbrakk> \<Longrightarrow> inv a P";
(*<*)
apply (unfold inv_def reach_def)
apply safe
apply (subgoal_tac "Ball (set x) P")
apply  blast
apply (erule runs.induct) 
apply  simp
apply auto
apply (subgoal_tac "sa \<in> set (sa # ss) \<and> P sa")
apply blast
apply simp
done
(*>*)

lemma invE: "\<lbrakk>inv a P; s \<in> reach a\<rbrakk> \<Longrightarrow> P s"
(*<*)
by (auto simp: inv_def reach_def split_paired_all)
(*>*)

lemma runs_reach: "\<lbrakk>r \<in> runs a; s \<in> set r\<rbrakk> \<Longrightarrow> s \<in> reach a"
(*<*)
by (auto simp add: reach_def)

lemma truns_lstate_reach: 
 "\<lbrakk>ts \<in> truns a; ((p, s), c_p'_s') \<in> set ts\<rbrakk> \<Longrightarrow> s \<in> reach a"
apply (erule truns2runs [THEN runs_reach])
apply (drule lstate_in_truns2runs)
apply simp
done
(*>*)


subsection "Parallel composition"

types ('i, 'a) family = "('i \<Rightarrow> 'a) \<times> 'i set"

consts
  all_inputs  :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> 'p set"
  all_outputs :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> 'p set"
  closed      :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> bool"
text {*\pagebreak*}
defs
  all_inputs_def : "all_inputs  \<equiv> \<lambda>(A,I). \<Union>( inputs \<circ> A)`I"
  all_outputs_def: "all_outputs \<equiv> \<lambda>(A,I). \<Union>(outputs \<circ> A)`I"
  closed_def     : "closed A \<equiv> all_inputs A = all_outputs A"

(*<*)
lemma inputs_in_all_inputs: 
 "i \<in> snd AI \<Longrightarrow> inputs (fst AI i) \<subseteq> all_inputs AI"
by (auto simp add: all_inputs_def)

lemma outputs_in_all_outputs: 
 "i \<in> snd AI \<Longrightarrow> outputs (fst AI i) \<subseteq> all_outputs AI"
by (auto simp add: all_outputs_def ran_def)
(*>*)
constdefs  --{* (static) well-formedness: inputs of peers should not overlap *}
  wf_comp :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> bool"
 "wf_comp \<equiv> \<lambda>(A,I). \<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> inputs (A i) \<inter> inputs (A j) = {}"
  --{* outputs of peers may overlap ($\leadsto$ nondeterministic interleaving) *}
  wf_isms :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> bool"
 "wf_isms \<equiv> \<lambda>(A,I). \<forall>i\<in>I. wf_ism (A i)"
(*<*)
lemma wf_ismsI: "\<And>AI. \<lbrakk>\<And>i. i\<in>snd AI \<Longrightarrow> wf_ism (fst AI i)\<rbrakk> \<Longrightarrow> wf_isms AI"
by (auto simp add: wf_isms_def)

lemma wf_ismsD: "\<lbrakk>wf_isms AI; i\<in>snd AI\<rbrakk> \<Longrightarrow> wf_ism (fst AI i)"
by (auto simp add: wf_isms_def)
(*>*)

types ('p, 'm, 's) conf = "('p, 'm) msgss \<times> 's" 
--{* input buffer state and local state *}
(*<*)
translations "(p, m, s) conf" \<leftharpoondown> (type) "(p, m) msgss \<times> s"
(*>*)

consts  comp_trans :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> 
                   (('c, 'p, 'm, ('p, 'm, 'i \<Rightarrow> 's) conf, 'd) trans) set"
inductive "comp_trans AI" intros --{* including feedback *}
 step: "\<lbrakk>i \<in> snd AI; ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst AI i)\<rbrakk> \<Longrightarrow>
         ((p1[\<lfloor>](-all_outputs AI), (p1[\<lfloor>](all_outputs AI) .@. b, s(i:=s1))), (c, d),
          (p2[\<lfloor>](-all_inputs  AI), (b .@. p2[\<lfloor>](all_inputs  AI), s(i:=s2)))) 
                                                              \<in> comp_trans AI"
(*<*)
inductive_cases comp_trans_elim_cases: "t \<in> comp_trans A"
(*>*)
constdefs
  ISM_comp :: "('i, ('c, 'p, 'm, 's, 'd) ism) family \<Rightarrow> 
               ('c, 'p, 'm, ('p, 'm, 'i \<Rightarrow> 's) conf, 'd) ism"
 "ISM_comp AI \<equiv> \<lparr>inputs  = all_inputs AI - all_outputs AI,
              \<spacespace>outputs = all_outputs AI - all_inputs AI,
              \<spacespace>init    = (\<currency>, init \<circ> fst AI),
              \<spacespace>trans   = comp_trans AI\<rparr>"
(*
lemma runs_comp_buffers_in_all_inputs_outputs [rule_format]:  --{* unused *}
"\<lbrakk>r \<in> runs (ISM_comp AI); wf_isms AI\<rbrakk> \<Longrightarrow> 
 \<forall>bs s' cs. r = (bs,s')#cs \<longrightarrow> lmap_dom bs \<subseteq> all_inputs AI \<inter> all_outputs AI"
*)(*<*)
(*apply (erule runs.induct)
apply  (simp_all add: ISM_comp_def del: K_Nil_def2)
apply (clarsimp elim!: comp_trans_elim_cases)
apply (drule wf_ismsD, simp)
apply (drule wf_ism_trans_in_outputs, simp)
apply (auto simp add: restrict_lmap_def split add: split_if_asm)
apply (simp only: lmap_dom_def2 [symmetric])
apply (fast dest: outputs_in_all_outputs)
done
*)(*>*)

lemma runs_closed_comp_past_induct [rule_format]:
"\<lbrakk>r \<in> runs (ISM_comp AI); closed AI; wf_isms AI;
  P \<currency> (init \<circ> fst AI) [];
  \<And>a p1 p2 cs i b c d s s1 s2.
       \<lbrakk>lmap_dom p1 \<subseteq> all_outputs AI; 
        (p1 .@. b, s(i:=s1)) # cs \<in> runs (ISM_comp AI); 
        P (p1 .@. b) (s(i:=s1)) cs; 
        i \<in> snd AI; ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst AI i)
       \<rbrakk> \<Longrightarrow> P (b .@. p2) (s(i:=s2)) ((p1 .@. b, s(i:=s1)) # cs)
 \<rbrakk> \<Longrightarrow> \<forall>bs s cs. r = (bs,s)#cs \<longrightarrow> P bs s cs"
(*<*)
apply (erule runs.induct)
apply (simp_all add: ISM_comp_def closed_def)
apply  (simp add: K_Nil_def)
apply (clarsimp elim!: comp_trans_elim_cases)
apply (drule wf_ismsD, simp)
apply (frule (1) wf_ism_trans_in_inputs)
apply (drule (1) wf_ism_trans_in_outputs)
apply (subgoal_tac "p1[\<lfloor>]all_outputs AI = p1", simp del: restrict_lmap_dom_eq)
apply  (subgoal_tac "p2[\<lfloor>]all_outputs AI = p2",(*all_inputs!*)simp (no_asm_simp))
apply   (simp)
apply  (simp)
apply  (erule subset_trans)
apply  (erule outputs_in_all_outputs)
apply (simp)
apply (erule subset_trans)
apply (erule inputs_in_all_inputs [THEN subset_trans])
apply blast
done
(*>*)

lemma runs_closed_comp_all_imp_all_induct:
"\<lbrakk>cs \<in> runs (ISM_comp AI); closed AI; wf_isms AI;
  P (\<currency>, init \<circ> fst AI) \<longrightarrow> Q (\<currency>, init \<circ> fst AI);
  \<And>a p1 p2 cs i b c d s s1 s2.
     \<lbrakk>lmap_dom p1 \<subseteq> all_outputs AI; 
      (p1 .@. b, s(i:=s1)) # cs \<in> runs (ISM_comp AI); 
      i \<in> snd AI; ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst AI i);
      Ball (set cs) Q; Q (p1 .@. b, s(i:=s1)); 
      Ball (set cs) P; P (p1 .@. b, s(i:=s1)); P (b .@. p2, s(i:=s2))
     \<rbrakk> \<Longrightarrow> Q (b .@. p2, s(i:=s2))
 \<rbrakk> \<Longrightarrow> (\<forall>c\<in>set cs. P c) \<longrightarrow> (\<forall>c\<in>set cs. Q c)"
(*<*)
apply (erule runs.induct)
apply  (simp_all add: ISM_comp_def closed_def)
apply (clarsimp elim!: comp_trans_elim_cases)
apply (drule wf_ismsD, simp)
apply (frule (1) wf_ism_trans_in_inputs)
apply (drule (1) wf_ism_trans_in_outputs)
apply (subgoal_tac "p1[\<lfloor>]all_outputs AI = p1", simp del: restrict_lmap_dom_eq)
apply  (subgoal_tac "p2[\<lfloor>]all_outputs AI = p2",(*all_inputs!*) simp del: restrict_lmap_dom_eq)
apply   (simp)
apply  (simp)
apply  (erule subset_trans)
apply  (erule outputs_in_all_outputs)
apply (simp)
apply (erule subset_trans)
apply (erule inputs_in_all_inputs [THEN subset_trans]) 
apply blast
done

(*>*)
text {*\pagebreak*}
subsection "Composite runs"

types ('i, 'c, 'g) g_trans =  "'i \<Rightarrow> ('g \<times> 'c \<times> 'g) set"
--{* index, input and output patterns, global pre-state, command, post-state *}

consts comp_runs:: "('g \<Rightarrow> ('i, ('c, 'p, 'm, 's, 'd) ism) family) \<Rightarrow> 
     'g \<Rightarrow> ('i, 'c, 'g) g_trans \<Rightarrow> ((('p, 'm, 'g \<times> ('i \<Rightarrow> 's)) conf) list) set"
inductive "comp_runs AIs g0 g_trans" intros
--{* including feedback *}
--{* for technical reasons, traces are built from right to left *}
 "init": "[(\<currency>, (g0,init \<circ> fst (AIs g0)))] \<in> comp_runs AIs g0 g_trans"
 "step": "\<lbrakk>(p1 .@. b, (g1, s(i:=s1)))#cs \<in> comp_runs AIs g0 g_trans;
           i \<in> snd (AIs g1); a = fst (AIs g1) i;
           ((p1, s1), (c, d), (p2, s2)) \<in> trans a;
           lmap_dom p1 \<subseteq> inputs a \<inter> all_outputs (AIs g1); 
           lmap_dom p2 \<subseteq> outputs a \<inter> all_inputs (AIs g1); 
           (g1, c, g2) \<in> g_trans i
           \<rbrakk> \<Longrightarrow> 
            (b .@. p2, (g2, s(i:=s2)))#
            (p1.@. b , (g1, s(i:=s1)))#cs \<in> comp_runs AIs g0 g_trans"
-- {* Changes to global state take effect after output has been performed.  *}
-- {* Here the environment is assumed to be part of the ISM system;\\\hspace*{2.5ex}
      communication with the environment may be modeled with suitable ISMs. *}
(*<*)
inductive_cases comp_runs_elim_cases: "cs \<in> comp_runs AIs g0 g_trans"
(*>*)

lemma comp_runs_global_induct: "cs \<in> comp_runs AIs ginit g_trans \<Longrightarrow> 
 P (AIs ginit) \<Longrightarrow> 
 (\<And>g1 c g2 i. \<lbrakk>(g1, c, g2) \<in> g_trans i; i \<in> snd (AIs g1); P (AIs g1)\<rbrakk> \<Longrightarrow>
                                                           P (AIs g2)      ) \<Longrightarrow>
 \<forall>(b,g,s) \<in> set cs. P (AIs g)"
(*<*)
by (erule comp_runs.induct, auto)
(*>*)

(*
lemma past_in_comp_runs [rule_format]: 
 "cs' \<in> comp_runs AIs g0 g_trans \<Longrightarrow> 
 \<forall>c. c \<in> set cs' \<longrightarrow> (\<exists>cs. cs' >= c#cs \<and> c#cs \<in> comp_runs AIs g0 g_trans)"
( *<* )
apply (erule comp_runs.induct)
apply  safe
apply  (force intro: comp_runs.init)
apply (drule set_ConsD, safe)
apply  (blast intro: comp_runs.step)
apply (fast intro: postfix_ConsI)
done
( *>
*)

lemma comp_runs_past_induct [rule_format]:
"\<lbrakk>r \<in> comp_runs AIs g0 g_trans; 
  P \<currency> g0 (init \<circ> fst (AIs g0)) [];
  \<And>a p1 p2 cs i b c d s g1 s1 g2 s2.
       \<lbrakk>(p1 .@. b, (g1, s(i:=s1))) # cs \<in> comp_runs AIs g0 g_trans; 
        P (p1 .@. b) g1 (s(i:=s1)) cs; 
        i \<in> snd (AIs g1);
        ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst (AIs g1) i);
        (g1, c, g2) \<in> g_trans i
       \<rbrakk> \<Longrightarrow> P (b .@. p2) g2 (s(i:=s2)) ((p1 .@. b, (g1, s(i:=s1))) # cs)
 \<rbrakk> \<Longrightarrow> \<forall>bs g s cs. r = (bs,(g,s))#cs \<longrightarrow> P bs g s cs"
(*<*)
apply (erule comp_runs.induct)
apply  (simp_all del: K_Nil_def2)
done
(*>*)

lemma comp_runs_all_imp_all_induct:
"\<lbrakk>cs \<in> comp_runs AIs g0 g_trans; 
  P (\<currency>, g0, init \<circ> fst (AIs g0)) \<longrightarrow> Q (\<currency>, g0, init \<circ> fst (AIs g0));
  \<And>a p1 p2 cs i b c d s g1 s1 g2 s2.
     \<lbrakk>(p1 .@. b, g1, s(i:=s1)) # cs \<in> comp_runs AIs g0 g_trans; 
      i \<in> snd (AIs g1); ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst (AIs g1) i);
      (g1, c, g2) \<in> g_trans i; 
      Ball (set cs) Q; Q (p1 .@. b, g1, s(i:=s1)); 
      Ball (set cs) P; P (p1 .@. b, g1, s(i:=s1)); 
      P (b .@. p2, g2, s(i:=s2))
     \<rbrakk> \<Longrightarrow> Q (b .@. p2, g2, s(i:=s2))
 \<rbrakk> \<Longrightarrow> (\<forall>c\<in>set cs. P c) \<longrightarrow> (\<forall>c\<in>set cs. Q c)"
(*<*)
apply (erule comp_runs.induct)
apply  (simp_all)
done
(*>*)

(*<*)
lemma comp_runs_g_trans_idD:
"(p, g, s) # cs \<in> comp_runs AIs g0 (\<lambda>i. {u. \<exists>g c. u = (g, c, g)}) \<Longrightarrow> g = g0"
by (drule_tac P = "\<lambda>bs g s cs. g = g0" in comp_runs_past_induct, auto)
(*>*)
theorem closed_comp_runs_comp: 
"\<lbrakk>wf_isms (AIs g); closed (AIs g)\<rbrakk> \<Longrightarrow> runs (ISM_comp (AIs g)) = 
  map (\<lambda>(b,g,s). (b,s)) ` comp_runs AIs g (\<lambda>i. {(g,c,g')| g c g'. g = g'})"
(*<*)
apply (auto simp: ISM_comp_def)
apply  (erule runs.induct)
apply   simp_all
apply   (rule image_eqI)
apply    (rule_tac [2] comp_runs.init)
apply   simp
apply  (tactic {* split_all_tac 1*}, rename_tac b s b' s' cs)
apply  (erule comp_trans_elim_cases)
apply  (clarsimp)
apply  (drule wf_ismsD, simp)
apply  (frule (1) wf_ism_trans_in_inputs)
apply  (drule (1) wf_ism_trans_in_outputs)
apply  (frule comp_runs_g_trans_idD, clarify)
apply  (rule image_eqI)
prefer 2
apply   (erule (1) comp_runs.step, rule refl)
prefer 5 apply (force)
apply     (subgoal_tac "p1[\<lfloor>]all_outputs (AIs g) = p1")
apply      (subgoal_tac "p2[\<lfloor>]all_inputs (AIs g) = p2")
apply       (simp (no_asm_simp))
apply      (simp)
apply      (erule subset_trans)
apply      (simp add: closed_def)
apply      (erule outputs_in_all_outputs)
apply     (simp add: closed_def)
apply     (drule sym)
apply     (simp, erule subset_trans)
apply     (erule inputs_in_all_inputs)
apply    force
apply   force
apply  fast
apply (erule_tac V = "closed (AIs g)" in thin_rl)
apply (erule comp_runs.induct, simp_all)
apply  (rule ssubst [OF arg_cong], rule_tac [2] runs.init) back
apply  (simp add: K_Nil_def o_def)
apply (rule runs.step, assumption)
apply (frule comp_runs_g_trans_idD)
apply clarsimp
apply (subgoal_tac "p1[\<lfloor>]all_outputs (AIs g) = p1")
apply  (rotate_tac -1, erule subst)
apply  (subgoal_tac "p2[\<lfloor>]all_inputs (AIs g) = p2")
apply   (rotate_tac -1, erule subst)
apply   (drule (2) comp_trans.step)
apply  auto
done
(*>*)

end