[isabelle] BUG: poly-ml dumps core (polyml 4.1.4, Isabelle2005, AWE 0.4)



I can get polyml to dump core using the attached files.
polyml crashes on the "apply (erule_tac [!] SLE66.transs.elims,
simp_all)" in SLE66.thy (right at the bottom).

The actual error message is (from *isabelle*):
catchSEGV; &context = 0x8088304, in_run_time_system=1, context.trapno=14
/home/thomas/local/opt/Isabelle2005/lib/scripts/run-polyml: line 126:  9984 Segmentation fault      (core dumped) "$POLY" $ML_OPTIONS "$(fixpath "$DB")"

I'm using Isabelle2005, polyml 4.1.4 (downloaded from the Isabelle home
page) and AWE 0.4 (downloaded from
http://www.informatik.uni-bremen.de/~cxl/awe/)

Seems like it's some interaction with AWE, because it works fine if I
remove the "use_thy ...AWE.thy" from SLE66.thy.
However, I currently use AWE in another theory just fine, so in general
the system is working, it just blows up on this specific command.

I didn't know where best to post this bug; if this is the wrong place
please let me know.

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

*)

(* header {* Minor extensions of HOL *} *)

theory Basis
imports Main
begin
(*<*)
ML {* Pretty.setmargin 169; quick_and_dirty:=false *}

(*
hide const "inputs"
hide const "outputs"

*)

declare O_assoc [simp]

declare fun_upd_idem_iff [simp] 
lemma o_fun_upd [simp]: "g \<circ> f(x:=y) = (g \<circ> f)(x:=g y)" 
by (rule ext, simp)

(* ####TO HOL/Fun.thy *)
constdefs 
  fun_upd_s :: "('a => 'b) => 'a set => 'b => ('a => 'b)"
                                              ("_/'(_{:=}_/')" [900,0,0] 900)
 "fun_upd_s f A b == %x. if x:A then b else f x" 

  chg_fun :: "('b => 'b) => 'a => ('a => 'b) => ('a => 'b)"
 "chg_fun f x g == g (x:=f (g x))"

lemma fun_upd_s_apply [simp]: "(f(A{:=}b)) x = (if x : A then b else f x)"
by (simp add: fun_upd_s_def)

(* TO HOL/Map.thy?* )
constdefs
  rev_image :: "('a ~=> 'b) => 'b => 'a set"
 "rev_image f b == {a. f a = Some b}"

constdefs
  dist_map :: "('a ~=> 'b * 'c) => ('a ~=> 'b ) * ('a ~=> 'c)"
 "dist_map m == (option_map fst o m, option_map snd o m)"

  graph :: "('a ~=> 'b) => ('a * 'b) set"
 "graph m == {(a, b) |a b. m a = Some b}"
*)
(* These are from HOL/Map.thy, but commented out there *)
(* Uncomment these lines if you use something newer than Isabelle2005 *)
(*
consts
map_subst::"('a ~=> 'b) => 'b => 'b =>
            ('a ~=> 'b)"                         ("_/'(_~>_/')"    [900,0,0]900)
map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
            ('a ~=> 'b)"                         ("_/'(_{|->}_/')" [900,0,0]900)

syntax (xsymbols)
map_subst :: "('a ~=> 'b) => 'b => 'b =>
                ('a ~=> 'b)"                     ("_/'(_\<leadsto>_/')"    [900,0,0]900)
map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
                                                 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
defs
map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"

lemma map_upd_s_apply [simp]:
  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
by (simp add: map_upd_s_def)

lemma map_subst_apply [simp]:
  "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
by (simp add: map_subst_def)
*)

subsection {* folding a relation over a list *}

consts
  fold_rel :: "('a \<times> 'c \<times> 'a) set \<Rightarrow> ('a \<times> 'c list \<times> 'a) set"
(*"fold_rel R cs \<equiv> foldl (\<lambda>r c. r O {(x,y). (c,x,y)\<in>R}) Id cs"*)

inductive "fold_rel R" intros
  Nil:  "(a, [],a) \<in> fold_rel R"
  Cons: "\<lbrakk>(a,x,b) \<in> R; (b,xs,c) \<in> fold_rel R\<rbrakk> \<Longrightarrow> (a,x#xs,c) \<in> fold_rel R"
inductive_cases fold_rel_elim_case [elim!]:
   "(a, [] , b) \<in> fold_rel R"
   "(a, x#xs, b) \<in> fold_rel R"

lemma fold_rel_Nil [intro!]: "a = b \<Longrightarrow> (a, [], b) \<in> fold_rel R" 
by (simp add: fold_rel.Nil)
declare fold_rel.Cons [intro!]


subsection "List maps"

constdefs
  K_Nil :: "'a => 'b list" ("\<currency>")
 "K_Nil \<equiv> \<lambda>x. []"

(*<*)
lemma K_Nil_def2 [simp]: "K_Nil x = []"
by (simp add: K_Nil_def)

lemma K_Nil_eqI: "\<forall>x. m x = [] \<Longrightarrow> m = \<currency>"
by (rule ext, auto)

lemma K_Nil_upd [simp]: "(\<lambda> x. if x=a then b else []) = (\<currency>(a:=b))"
by(simp add:K_Nil_def fun_upd_def)

lemma lmap_upd_cong [simp]: "(m(x := y) = m(x := y')) = (y = y')"
by (safe, drule fun_cong, auto split add: split_if_asm)

(*>*)
constdefs
  lmap_dom :: "('a => 'b list) \<Rightarrow> 'a set"
 "lmap_dom m \<equiv> {x. m x \<noteq> []}"
(*<*)
lemma lmap_dom_def2 [simp]: "x \<in> lmap_dom m = (m x \<noteq> [])" 
by (auto simp add: lmap_dom_def)

lemma lmap_dom_empty_eq [simp]: "lmap_dom m = {} = (m = \<currency>)"
by (auto simp add: lmap_dom_def intro: K_Nil_eqI)

lemma lmap_dom_K_Nil [simp]: "lmap_dom \<currency> = {}"
by simp
(*>*)
constdefs
  lmap_subst :: "'a => 'a => ('a => 'b list) => ('a => 'b list)"
 "lmap_subst x x' m == m(x:=[],x':= m x)"
constdefs
 "restrict_lmap" :: "['a => 'b list, 'a set] => ('a => 'b list)"
                                                      ("_[\<lfloor>]_" [90, 91] 90)
  "m[\<lfloor>]A == %x. if x : A then m x else []"

(*<*)
lemma restrict_lmap_K_Nil [simp]: "\<currency>[\<lfloor>]A = \<currency>"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_empty [simp]: "a[\<lfloor>]{} = \<currency>"
by (rule ext, auto simp: restrict_lmap_def)

lemma restrict_lmap_restrict_lmap [simp]: "a[\<lfloor>]A[\<lfloor>]B = a[\<lfloor>](A\<inter>B)"
by (rule ext, auto simp: restrict_lmap_def)

lemma restrict_lmap_upd_in [simp]: "x \<in> A \<Longrightarrow> m(x:=y)[\<lfloor>]A = (m[\<lfloor>]A)(x:=y)"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_upd_notin [simp]: "x \<notin> A \<Longrightarrow> m(x:=y)[\<lfloor>]A = m[\<lfloor>]A"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_contains [simp]: 
  "x \<in> set ((m[\<lfloor>]A) p) = (x \<in> set (m p) \<and> p \<in> A)"
by (auto simp add: restrict_lmap_def)

lemma lmap_dom_restrict_lmap [simp]: "lmap_dom (a[\<lfloor>]A) = lmap_dom a \<inter> A" 
by (auto simp add: restrict_lmap_def split add: split_if_asm)

lemma restrict_lmap_dom_eq [simp]: "(m[\<lfloor>]A = m) = (lmap_dom m \<subseteq> A)"
apply safe
apply (drule_tac x = x in fun_cong)
apply (rule_tac [2] ext)
apply (rule_tac [2] sym)
apply (auto simp add: restrict_lmap_def lmap_dom_def split add: split_if_asm)
done

(*>*)constdefs
  fappend :: "('a => 'b list) => ('a => 'b list) => ('a => 'b list)" 
                                                      (infixr ". at ." 65) 
 "a . at . b == %n. a n @ b n"

(*<*)
lemma fappend_def2 [simp]: "(a . at . b) n = a n @ b n"
apply (unfold fappend_def)
apply (rule refl)
done

lemma fappend_K_Nil [simp]: "a . at . \<currency> = a"
by (auto simp add: fappend_def)

lemma K_Nil_fappend [simp]: "\<currency> . at . a = a"
by (auto simp add: fappend_def)

lemma fappend_inj1 [simp]: "a . at . b = a' . at . b = (a = a')"
apply auto
apply (unfold fappend_def)
apply (rule ext)
apply (drule_tac x=x in fun_cong)
apply simp
done

lemma fappend_inj2 [simp]: "a . at . b = a . at . b' = (b = b')"
apply auto
apply (unfold fappend_def)
apply (rule ext)
apply (drule_tac x=x in fun_cong)
apply simp
done

lemma fappend_assoc [simp]: "(a . at . b) . at . c = a . at . b . at . c"
apply (unfold fappend_def)
apply auto
done

lemma fappend_commut_disjunct_lmap_dom: 
  "lmap_dom a \<inter> lmap_dom b = {} \<Longrightarrow> a . at . b = b . at . a"
apply (rule ext, auto simp: fappend_def)
apply (drule equalityD1)
apply (simp add: subset_def)
apply (erule_tac x = x in allE)
apply auto
done

lemma "fappend_upd_conv" [simp]: "a . at . b(n:=[v]) = (a . at . b)(n:=a n @ [v])"
apply (rule ext)
apply (simp add: K_Nil_def)
done

lemma "upd_fappend_conv" [simp]: "a(n:=[v]) . at . b  = (a . at . b)(n:=v#b n)"
apply (rule ext)
apply (simp add: K_Nil_def)
done

lemma fappend_eq_Nil [simp]: "(a . at . b = \<currency>) = (a = \<currency> \<and> b = \<currency>)"
apply (auto simp add: fappend_def)
apply (rule_tac [!] ext)
apply auto
apply (drule_tac [!] x = x in fun_cong)
apply auto
done

lemma fappend_not_K_Nil [dest!]: "a(x := y a # f a) = \<currency> \<Longrightarrow> False"
by (drule fun_cong [of _ _ x], auto)

lemma K_Nil_not_fappend_not [dest!]: "\<currency> = a(x := y a # f a)  \<Longrightarrow> False"
by (drule fun_cong [of _ _ x], auto)

lemma fappend_restrict_lmap [simp]: "(a . at . b)[\<lfloor>]A = a[\<lfloor>]A . at . b[\<lfloor>]A"
by (rule ext, auto simp add: restrict_lmap_def)

lemma fappend_compl_restrict_lmap [simp]: "a[\<lfloor>]A . at . a[\<lfloor>](-A) = a"
by (rule ext, auto simp add: restrict_lmap_def)

lemma fappend_incr_length [simp]: "length (bs x) \<le> length ((bs . at . b) x)"
by (auto simp add: fappend_def)

(*>*)
end
(*  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) . at . b, s(i:=s1))), (c, d),
          (p2[\<lfloor>](-all_inputs  AI), (b . at . 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 . at . b, s(i:=s1)) # cs \<in> runs (ISM_comp AI); 
        P (p1 . at . b) (s(i:=s1)) cs; 
        i \<in> snd AI; ((p1, s1), (c, d), (p2, s2)) \<in> trans (fst AI i)
       \<rbrakk> \<Longrightarrow> P (b . at . p2) (s(i:=s2)) ((p1 . at . 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 . at . 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 . at . b, s(i:=s1)); 
      Ball (set cs) P; P (p1 . at . b, s(i:=s1)); P (b . at . p2, s(i:=s2))
     \<rbrakk> \<Longrightarrow> Q (b . at . 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 . at . 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 . at . p2, (g2, s(i:=s2)))#
            (p1. at . 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 . at . b, (g1, s(i:=s1))) # cs \<in> comp_runs AIs g0 g_trans; 
        P (p1 . at . 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 . at . p2) g2 (s(i:=s2)) ((p1 . at . 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 . at . 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 . at . b, g1, s(i:=s1)); 
      Ball (set cs) P; P (p1 . at . b, g1, s(i:=s1)); 
      P (b . at . p2, g2, s(i:=s2))
     \<rbrakk> \<Longrightarrow> Q (b . at . 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
(*<*)
theory ISM_package
imports ISM

begin
ML {*
(*  Title:      ISM_package.ML
    ID:         $Id: ISM_package.ML,v 1.13 2003/09/12 16:13:02 dvo Exp $
    Author:     Sebastian Nanz, TU Muenchen and David von Oheimb, Siemens AG

Definition of Interacting State Machines (ISMs).
*)

datatype ('a,'b) sum = Inl of 'a | Inr of 'b;

fun option_map f  NONE    = NONE
|   option_map f (SOME x) = SOME (f x)

type ind_def = {defs: thm list, mono: thm, elims: thm list, intrs: thm list,
            induct: thm, unfold: thm, mk_cases: string -> thm, raw_induct: thm};


signature ISM_PACKAGE =
sig
  type 'a rule
  val add_ism: string -> (string * string) list -> 
               string -> string -> string -> string -> 
               (string * string option) option -> 
               string option -> 
               (string * (string * string)) option -> 
               (string * (string * string)) option ->
               string rule list -> theory -> 
               theory * ind_def list * thm list
  val add_ism_i: string -> (string * typ) list -> 
               typ -> term -> term -> typ -> 
               (typ * term option) option ->
               typ option -> 
               (typ * (term * string)) option -> 
               (typ * (term * term  )) option ->
               term rule list -> theory -> 
               theory * ind_def list * thm list
end;


structure ISM_package (*: ISM_PACKAGE*) =
struct

(*** utilities ***)

(** messages and errors **)

val quiet_mode = ref false;
fun message s = if !quiet_mode then () else writeln s;

exception ism_exception;
fun ism_error msg = (raise ism_exception) handle ism_exception => error msg;

fun no_state_error name = "ISM " ^ quote name ^ 
                         " has neither a control nor a data state declaration.";
fun no_ctrl_st_error name = "ISM has a control state transition in rule " ^ 
                            quote name ^ " but no control state declaration.";
fun no_ctrl_trans_error name = 
        "ISM has control state but not control state transitions in rule " ^ 
        quote name ^ ".";
fun no_data_st_error name = "ISM has postconditions in transition " ^ 
                            quote name ^ " but no data state declaration.";
fun field_type_error field_name = "Unable to determine field type for field " ^
                                  quote field_name ^ ".";
fun fetch_constr_error l_st_name g_st_name = "Unable to determine a datatype " ^
                   quote g_st_name ^ "\n that has a single argument of type " ^
                   quote l_st_name ^ ".";

(** constructor of global type **)

fun fetch_constr'' l_st_Typ constr_opt [] = constr_opt
  | fetch_constr'' l_st_Typ constr_opt (constr::rest) =
    let
      val (constr_Term, constr_Typ) = constr;
      val l_st_DTyp = DatatypeAux.dtyp_of_typ [] l_st_Typ;
      val constr_opt' = if constr_Typ = [l_st_DTyp] then SOME constr_Term 
                                                    else constr_opt;
    in
      fetch_constr'' l_st_Typ constr_opt' rest
    end;

fun fetch_constr' l_st_Typ constr_opt [] = constr_opt
  | fetch_constr' l_st_Typ constr_opt (descr::rest) =
    let
      val (_, (_, _, constr)) = descr;
      val constr_opt' = fetch_constr'' l_st_Typ constr_opt constr;
    in
      fetch_constr' l_st_Typ constr_opt' rest
    end;

fun fetch_constr l_st_Typ g_st_Typ thy =
  let
    val sign = Theory.sign_of thy;
    val fetch_constr_err = fetch_constr_error (Sign.string_of_typ sign l_st_Typ)
      (Sign.string_of_typ sign g_st_Typ);

    (* determine type name of global state datatype *)
    val g_st_name = case g_st_Typ of Type (g_st_name, _)
                         => Sign.intern_type sign g_st_name
                     | _ => let val _ = ism_error fetch_constr_err in "" end;
    
    (* symbol table lookup *)
    val symtab_opt = Symtab.lookup (DatatypePackage.get_datatypes thy) g_st_name;
    val descr_opt = option_map (#descr) symtab_opt;
    val descr = case descr_opt of SOME descr => descr
      | NONE => let val _ = ism_error fetch_constr_err in [] end;
    val constr_opt = fetch_constr' l_st_Typ NONE descr;
    val constr = case constr_opt of NONE =>
      let val _ = ism_error fetch_constr_err in "" end
      | SOME(constr) => constr;
  in
    constr
  end;

fun mk_global_st_term l_st_Typ g_st_Typ_opt thy t =
  case g_st_Typ_opt of NONE           => t 
                     | SOME(g_st_Typ) => 
    Const (fetch_constr l_st_Typ g_st_Typ thy, l_st_Typ --> g_st_Typ) $ t

(* end; *)

(** helpers **)

fun combine [] [] = []
  | combine (x::xs) [] = []
  | combine [] (y::ys) = []
  | combine (x::xs) (y::ys) = (x, y) :: combine xs ys;

local
  fun esc_underscores [] = []
  |   esc_underscores (x::xs) = if (x = "_") then "'"::x::esc_underscores xs
                                             else      x::esc_underscores xs;
in
  fun escape_underscores name = implode (esc_underscores (explode name))
end;


(*** type handling ***)

(* 'a rule is the type of the ism transitions *)
type 'a rule = ((bstring * Args.src list) * (('a * 'a) option * ('a option *
               ('a list * ((('a * bool) * 'a) list * ((('a * bool) * 'a) list *
               ('a option * (((string * 'a) list, 'a) sum))))))));

val dummyT = Type ("_dummy", []);

fun mk_Typ prep_typ sign type_constr = typ_of (prep_typ sign type_constr);
fun mk_listT T = Type ("List.list", [T]);



(*** term handling ***)

val dummy_Term = Const("_dummy", dummyT);

fun mk_Term prep_term sign t = term_of (prep_term sign t);

fun mk_k_nil_Term sign pt_Typ msg_Typ =
  let
    val msgss_Typ = mk_listT msg_Typ;
    val k_nil_Typ = pt_Typ --> msgss_Typ;
    val k_nil_Term = Const(Sign.intern_const sign "K_Nil", k_nil_Typ);
  in
    (k_nil_Term, k_nil_Typ)
  end;

fun mk_pair_Const sign a_Typ b_Typ =
  let
    val pair_Const_Typ = a_Typ --> b_Typ --> HOLogic.mk_prodT (a_Typ, b_Typ);
    val pair_Const = Const("Pair", pair_Const_Typ);
  in
    (pair_Const, pair_Const_Typ)
  end;

fun mk_pair_Term_Typ sign (a_Term, a_Typ) (b_Term, b_Typ) =
  let
    val (pair_Const, _) = mk_pair_Const sign a_Typ b_Typ;
    val pair_Term = pair_Const $ a_Term $ b_Term;
    val pair_Typ = HOLogic.mk_prodT(a_Typ, b_Typ);
  in
    (pair_Term, pair_Typ)
  end;

fun mk_state_opt prep_type prep_term sign = option_map
   (fn (s_type, (s_term, s_Var)) =>
    let
      val s_Typ  = mk_Typ  prep_type sign s_type;
      val s_Term = mk_Term prep_term sign (s_term, s_Typ);
    in
      (s_Term, s_Typ, s_Var)
    end);



(*** transitions ***)

(** prepare inputs and outputs **)

fun mk_msgss_pat sign pt_Typ msg_Typ = 
  let
    val msg_list_Typ = mk_listT msg_Typ;
    val msgss_Typ = pt_Typ --> msg_list_Typ;
    fun fun_upd_Typ T = msgss_Typ --> T --> msg_list_Typ --> msgss_Typ;
    val fun_upd_Term   = Const (Sign.intern_const sign "fun_upd" , 
                                fun_upd_Typ pt_Typ);
    val fun_upd_s_Term = Const (Sign.intern_const sign "fun_upd_s", 
                                fun_upd_Typ (HOLogic.mk_setT pt_Typ));
   in
      Library.foldl (fn (f, ((pat,multi), msgs)) => 
          (if multi then fun_upd_s_Term else fun_upd_Term) $ f $ pat $ msgs)
    end;


(** update record fields (for postconditions) **)
(* TODO: I think we don't handle record extensions correctly here... *)
fun find_field_Typ sign field_name data_st_Typ =
  let 
    val record_fields = fst(RecordPackage.get_recT_fields sign data_st_Typ);
    val found_types = filter (fn x => Sign.base_name(fst(x)) = field_name) record_fields;
  in
    case found_types of 
      []  => let val _ = ism_error (field_type_error field_name) in dummyT end
      | _ => snd(hd(found_types))
  end;

(* Typ: Context.theory -> Term.typ -> Term.term -> (string * Term.term) list -> Term.term *)
fun mk_field_upd sign data_st_Typ r [] = r
  | mk_field_upd sign data_st_Typ r (post::rest) =
    let
      val (field_name, field_Term) = post;
      val field_Typ = find_field_Typ sign field_name data_st_Typ;
      val field = Const(Sign.intern_const sign (field_name ^ "_update"),
        field_Typ --> data_st_Typ --> data_st_Typ) $ field_Term $ r;
    in
      mk_field_upd sign data_st_Typ field rest
    end;


(** add premises terms to conclusion term **)

fun mk_prems sign concl [] = concl
  | mk_prems sign concl (pre_Term::rest) =
    let
      val impl_Term = Const("==>", propT --> propT --> propT);
      val concl' = impl_Term $ (HOLogic.mk_Trueprop pre_Term) $ concl;
    in
      mk_prems sign concl' rest
    end;

(** transform transition rule (for simultaneous type check) **)

(* Typ: (Context.theory -> (''a * Term.typ) list -> Thm.cterm list) ->
       Context.theory ->
       (Term.typ * 'b) option * Term.typ * Term.typ * 'c *
       ('d * ...) option * ... option * ... ->
       ''a ISM_package.rule -> Term.term option * Term.term ISM_package.rule
*)
fun transform_rule prep_rule sign types (rule:''a rule) =
  let
    val (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, ctrl_st_Typ_Term_opt,
	      data_st_Typ_Term_opt, l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt) = types;
    val ((name, args), (cs_exprs, (dom_opt, (pres, (inps, (outps, (cmd_opt, post_v))))))) =
        rule;
    val msg_list_Typ = mk_listT msg_Typ;
    val ctrl_st_Typ = case ctrl_st_Typ_Term_opt of 
                        NONE => (case cs_exprs of NONE => dummyT 
                                  | SOME _ => ism_error (no_ctrl_st_error name))
                       | SOME (_, typ, _) => (case cs_exprs of NONE => 
                          ism_error (no_ctrl_trans_error name) | SOME _ => typ);

    (* transform rule into Term_Typ list (for prep_rule) *)
    val l = case data_st_Typ_Term_opt of NONE => []
      | SOME(_, data_st_Typ, data_st_var) => [(data_st_var, data_st_Typ)];
    val l = l @ (case cs_exprs of NONE => [] | SOME (cs_expr,cs_expr') =>
                 [(cs_expr, ctrl_st_Typ), (cs_expr', ctrl_st_Typ)]);
    val l = l @ (map (fn p => (p, HOLogic.boolT)) pres);
    val trans_forw_pats = Library.flat o map (fn ((pat, multi), msgs) =>
                       [(pat, if multi then HOLogic.mk_setT pt_Typ else pt_Typ),
                        (msgs, msg_list_Typ)]);
    val l = l @ trans_forw_pats inps; 
    val l = l @ trans_forw_pats outps;
    val l = l @ (case cmd_opt of NONE => []
    | SOME cmd => (case cmd_Typ_default_opt of
                     NONE => ism_error ("ISM has no commands " ^ 
                      "but subsection \"cmd\" is present in rule " ^quote name)
                   | SOME (cmd_Typ, _) => [(cmd, cmd_Typ)]));
    val l = l @ (case dom_opt of NONE => []
    | SOME dom => (case domain_Typ_default_opt of
                     NONE => ism_error ("ISM has no domains " ^ 
                      "but subsection \"dom\" is present in rule " ^quote name)
                   | SOME (dom_Typ, _) => [(dom, dom_Typ)]));

    val l = case data_st_Typ_Term_opt of NONE => (if (post_v <> Inl []) then 
                                   ism_error (no_data_st_error name) else l)
                              | SOME (_, data_st_Typ, _) => l @ (case post_v of 
          Inl ps => (map (fn (f,v) => (v,find_field_Typ sign f data_st_Typ))) ps
        | Inr sval => [(sval, data_st_Typ)]);

    (* transformation *)
    val l = map term_of (prep_rule sign l);

    (* transform Term_Typ list back into rule *)
    val (data_st_var_opt,l) = case data_st_Typ_Term_opt of NONE => (NONE,l)
                              | _ => (SOME (hd l), Library.drop (1, l));
    val (ctrl_st_exprs,l) = (case cs_exprs of NONE => (NONE,l) 
                             | SOME _ => (SOME (hd l, hd (tl l)), Library.drop(2, l)));
    val pres' = Library.take (length pres, l);
    val l = Library.drop (length pres, l);
    fun trans_back_pats l [] = []
    |   trans_back_pats l (((pat,multi),_)::rest) = 
        ((hd l, multi), hd (tl l))::trans_back_pats (tl (tl l)) rest;
    val inps' = trans_back_pats l inps;
    val l = Library.drop (2* length inps, l);
    val outps' = trans_back_pats l outps;
    val l = Library.drop (2* length outps, l);
    val (cmd_opt',l) = if cmd_opt = NONE then (NONE,l) 
                       else (SOME (hd l), Library.drop (1, l));
    val (dom_opt',l) = if dom_opt = NONE then (NONE,l) 
                       else (SOME (hd l), Library.drop (1, l));
    val post_v' = case post_v of 
          Inl posts => Inl (combine ((map (fn (f, v) => f)) posts) l)
        | Inr sval =>  Inr (hd l);
    val rule' = ((name, args), 
                (ctrl_st_exprs, (dom_opt', (pres', (inps', (outps', (cmd_opt', post_v')))))));
  in
    (data_st_var_opt, (rule':term rule))
  end;


(* We need to define some inductive sets (transs, steps and output), so we use 
 * a common helper function which builds most of what we need
 *)
fun mk_intros_helper prep_rule thy types rule =
    let
      val sign = Theory.sign_of thy;

      (* expand types *)
      val (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, ctrl_st_Typ_Term_opt,
        data_st_Typ_Term_opt, l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt) = types;

      val (data_st_var_opt, rule') = 
               transform_rule prep_rule sign types rule;

      (* expand transition *)
      val ((name, args), (ctrl_st_exprs, conds)) = rule';
      val (dom_opt,( pres, (inps, (outps, (cmd_opt, post_v))))) = conds;

      val (k_nil_Term, _) = mk_k_nil_Term sign pt_Typ msg_Typ;
      val msgss_Typ = pt_Typ --> mk_listT msg_Typ;

      (* prepare inputs *)
      val is_Term = mk_msgss_pat sign pt_Typ msg_Typ (k_nil_Term, inps);

      (* prepare outputs *)
      val os_Term = mk_msgss_pat sign pt_Typ msg_Typ (k_nil_Term, outps);

      (* prepare states *)
      fun mk_state proj post_v = mk_global_st_term l_st_Typ g_st_Typ_opt thy 
        (case data_st_Typ_Term_opt of
          NONE => proj (the ctrl_st_exprs)
        | SOME(_, data_st_Typ, _) => 
          let
            val data_st_Term = case post_v of 
                    Inl posts => mk_field_upd sign data_st_Typ 
                                              (the data_st_var_opt) posts
                  | Inr sval => sval;
          in case ctrl_st_Typ_Term_opt of 
               NONE => data_st_Term
             | SOME(_, ctrl_st_Typ, _) => 
                 fst (mk_pair_Const sign ctrl_st_Typ data_st_Typ)
                 $ proj (the ctrl_st_exprs) $ data_st_Term
	  end);
      val s_Term  = mk_state fst (Inl []);
      val s'_Term = mk_state snd post_v;

      (* construct transition *)
      val cmd_Typ = case cmd_Typ_default_opt of SOME (t,_) => t | NONE => 
                                                                  HOLogic.unitT;
      val cmd     = case cmd_opt of SOME t => t | NONE => 
                   (case cmd_Typ_default_opt of 
                 NONE => HOLogic.unit  
               | SOME (_, SOME default_cmd) => default_cmd
               | _ => ism_error ("ISM has commands without default command " ^ 
                    "but subsection \"cmd\" is missing in rule " ^ quote name));

      val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t 
                                                 | NONE       => HOLogic.unitT;
      val dom     = case dom_opt of SOME t => t | NONE => 
                   (case domain_Typ_default_opt of 
                 NONE => HOLogic.unit  
               | SOME (_, SOME default_domain) => default_domain
               | _ => ism_error ("ISM has domains without default domain " ^ 
                    "but subsection \"dom\" is missing in rule " ^ quote name));
    in
      (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, 
      dom_Typ, dom, name, args, pres)
    end;

(** make introduction rules **)
(* the transs relation is defined inductively in this function *)
fun mk_intros_trans prep_rule thy types param_transs_Term rule =
    let
      val sign = Theory.sign_of thy;
      (* expand types *)
      val (_, _, _, st_Typ, _, _, _, _, _) = types;

      val (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, 
        dom_Typ, dom, name, args, pres) = mk_intros_helper prep_rule thy types rule;

      (* create one trans tuple *)
      val (is_s_Term, is_s_Typ) =
           mk_pair_Term_Typ sign (is_Term, msgss_Typ) (s_Term, st_Typ);
      val (os_s'_Term, os_s'_Typ) = 
           mk_pair_Term_Typ sign (os_Term, msgss_Typ) (s'_Term, st_Typ);
      val (cd_Term, cd_Typ) =
           mk_pair_Term_Typ sign (cmd, cmd_Typ) (dom, dom_Typ);
      val (trans_Term, trans_Typ) = mk_pair_Term_Typ sign (is_s_Term, is_s_Typ) 
        (mk_pair_Term_Typ sign (cd_Term, cd_Typ) (os_s'_Term, os_s'_Typ));

      (* construct conclusion *)
      val elem_Term = Const("op :", 
                    trans_Typ --> HOLogic.mk_setT trans_Typ --> HOLogic.boolT);
      val concl_Term = HOLogic.mk_Trueprop 
                       (elem_Term $ trans_Term $ param_transs_Term);

      (* construct rule with premissions *)
      val rule_Term = mk_prems sign concl_Term (rev pres);

      (* introduction rule *)
      val args' = map (Attrib.global_attribute thy) args;
      val intr = ((name, rule_Term), args');
    in
      intr
    end;

(* the steps relation is defined inductively in this function *)
fun mk_intros_step prep_rule thy types param_steps_Term rule =
    let
      val sign = Theory.sign_of thy;
      val (_, _, _, st_Typ, _, _, _, _, _) = types;
      val (msgss_Typ, is_Term, _, s_Term, s'_Term, _, _, 
        _, _, name, args, pres) = mk_intros_helper prep_rule thy types rule;

      val (steps_Term, state_tuple_Typ) =
           mk_pair_Term_Typ sign (s_Term, st_Typ) (s'_Term, st_Typ);

      (* construct conclusion *)
      val elem_Term = Const("op :", 
                    state_tuple_Typ --> HOLogic.mk_setT state_tuple_Typ --> HOLogic.boolT);
      val concl_Term = HOLogic.mk_Trueprop 
                       (elem_Term $ steps_Term $ param_steps_Term);

      val cond_Term = Const("op =", msgss_Typ --> msgss_Typ --> HOLogic.boolT)
                      $ Free ("ins", msgss_Typ) $ is_Term;
      (* construct rule with premissions *)
      val rule_Term = mk_prems sign concl_Term (cond_Term::(rev pres));

      (* introduction rule *)
      val args' = map (Attrib.global_attribute thy) args;
      val intr = ((name, rule_Term), args');
    in
      intr
    end;


(* the outputs relation is defined inductively in this function *)
fun mk_intros_output prep_rule thy types param_outputs_Term rule =
    let
      val sign = Theory.sign_of thy;

      val (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, 
        dom_Typ, dom, name, args, pres) = mk_intros_helper prep_rule thy types rule;

      (* construct conclusion *)
      val elem_Term = Const("op :", 
                    msgss_Typ --> HOLogic.mk_setT msgss_Typ --> HOLogic.boolT);
      val concl_Term = HOLogic.mk_Trueprop 
                       (elem_Term $ os_Term $ param_outputs_Term);

      (* construct rule with premissions *)
      val dom_pre = Const("op =", dom_Typ --> dom_Typ --> HOLogic.boolT) $ Free("d", dom_Typ) $ dom;
      val rule_Term = mk_prems sign concl_Term (dom_pre::(rev pres));

      (* introduction rule *)
      val args' = map (Attrib.global_attribute thy) args;
      val intr = ((name, rule_Term), args');
    in
      intr
    end;


(** add transition set **)
(* If you use something newer than Isabelle2005, use OldInductivePackage instead *)
local
  open InductivePackage
in
fun add_transs prep_rule types param_transs_Term [] (thy, thms) = 
                                                    (thy, thms)
|   add_transs prep_rule types param_transs_Term transs (thy, thms) =
    let
      val sign = Theory.sign_of thy;
      val intros = map (mk_intros_trans prep_rule thy types param_transs_Term) transs;
      val (thy', thm) = thy
        |> add_inductive_i true false "" false false false 
                                            [param_transs_Term] intros [];
      val thms' = thm :: thms;
    in
      (thy', thms')
    end;

fun add_outputs prep_rule types param_outputs_Term [] (thy, thms) = 
                                                      (thy, thms)
|   add_outputs prep_rule types param_outputs_Term transs (thy, thms) =
    let
      val sign = Theory.sign_of thy;
      val intros = map (mk_intros_output prep_rule thy types param_outputs_Term) transs;
      val (thy', thm) = thy
        |> add_inductive_i true false "" false false false 
                                            [param_outputs_Term] intros [];
      val thms' = thm :: thms;
    in
      (thy', thms')
    end;

fun add_steps prep_rule types param_steps_Term [] (thy, thms) = 
                                                  (thy, thms)
|   add_steps prep_rule types param_steps_Term transs (thy, thms) =
    let
      val sign = Theory.sign_of thy;
      val intros = map (mk_intros_step prep_rule thy types param_steps_Term) transs;
      val (thy', thm) = thy
        |> add_inductive_i true false "" false false false 
                                            [param_steps_Term] intros [];
      val thms' = thm :: thms;
    in
      (thy', thms')
    end;

(* Careful: this function is different from the ones above them - it doesn't 
 * define an inductive set, but a function
 *)
fun add_dom_fun prep_rule types dom_free_Var transs thy =
    let
      val (_, pt_Typ, msg_Typ, _, _, _, _, _, domain_Typ_default_opt) = types;
      val msgss_Typ = pt_Typ --> mk_listT msg_Typ;

      val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t 
                                                 | NONE       => HOLogic.unitT;
      val default_dom = Const("arbitrary", dom_Typ);
      (* filter is_Term and dom out of the transition *)
      fun filter_inp_dom t = let val (_, inp, _, _, _, _, _, _, dom, _, _, _) = t in (inp, dom) end;
      val vars = map (filter_inp_dom o mk_intros_helper prep_rule thy types) transs;


      val elem_Term = Const("HOL.If", HOLogic.boolT --> dom_Typ --> dom_Typ --> dom_Typ);
      val eq_Term = Const("op =", msgss_Typ --> msgss_Typ --> HOLogic.boolT);
      fun construct_if ((inp, dom), elsef) = 
        let
          (* the input pattern inp may contain free variables; we quantify them existentially here *)
          val free_vars = Term.add_frees inp [];
          val dom_free_name = #1 (dest_Free dom_free_Var);
          val _ = if (exists ((curry (op =))(dom_free_name)) (map #1 free_vars)) 
            then ism_error("Sorry, but you can't use the variable name "^quote dom_free_name^" in an ISM.")
            else "";
          val dom_eq_Term = eq_Term $ dom_free_Var $ inp;
          fun mk_exists2 ((name, typ), term) = HOLogic.mk_exists(name,typ,term);
          val inp2 = foldl mk_exists2 dom_eq_Term free_vars;
        in
          elem_Term $ inp2 $ dom $ elsef
        end;
      val if_Term = foldr construct_if default_dom vars;
    in
      if_Term
    end;


end;



(*** add_ism ***)

fun gen_add_ism prep_type prep_term prep_rule name params' 
         pt_type pt_set_I pt_set_O msg_type cmd_type_default_opt
         domain_type_default_opt g_st_type_opt ctrl_st data_st transs thy =
let
  val _ = message ("Constructing ism " ^ quote name ^  " ...");
  val sign = Theory.sign_of thy;

  (* open own namespace *)
  val thy = Theory.add_path name thy;
  val sign = Theory.sign_of thy;

  val params = map (fn (n,ty) => (n, mk_Typ prep_type sign ty)) params';

  (* port types and terms *)
  val pt_Typ = mk_Typ prep_type sign pt_type;
  val pt_set_Typ = HOLogic.mk_setT pt_Typ;
  val pt_set_I_Term = mk_Term prep_term sign (pt_set_I, pt_set_Typ);
  val pt_set_O_Term = mk_Term prep_term sign (pt_set_O, pt_set_Typ);

  (* message type *)
  val msg_Typ = mk_Typ prep_type sign msg_type;
  
  (* command type *)
  val cmd_Typ_default_opt = option_map (fn (cmd_type, default) => 
                              let val cmd_Typ = mk_Typ prep_type sign cmd_type 
                              in (cmd_Typ,
                                  option_map (fn t =>
                                  mk_Term prep_term sign (t, cmd_Typ)) default)
                              end) cmd_type_default_opt;
  val cmd_Typ = case cmd_Typ_default_opt of NONE       => HOLogic.unitT 
                                          | SOME (t,_) => t;

  (* domain type *)
  val domain_Typ_default_opt = option_map (fn (domain_type, default) => 
                              let val domain_Typ = mk_Typ prep_type sign domain_type
                              in (domain_Typ,
                                  option_map (fn t =>
                                  mk_Term prep_term sign (t, domain_Typ)) default)
                              end) domain_type_default_opt;
  val domain_Typ = case domain_Typ_default_opt of NONE       => HOLogic.unitT 
                                                | SOME (t,_) => t;

  (* states *)
  (* global state type *)
  val g_st_Typ_opt = option_map (mk_Typ prep_type sign) g_st_type_opt;
  (* local state initial terms; type*)
  val ctrl_st_Typ_Term_opt = mk_state_opt prep_type prep_term sign ctrl_st;
  val data_st_Typ_Term_opt = mk_state_opt prep_type prep_term sign data_st;
  val l_st_Typ =
    case ctrl_st_Typ_Term_opt of NONE =>
          (case data_st_Typ_Term_opt of NONE =>
                let val _ = ism_error (no_state_error name) in dummyT end
            | SOME(_, data_st_Typ, _) => data_st_Typ)
    | SOME(_, ctrl_st_Typ, ctrl_st_var_dummy) =>
      case data_st_Typ_Term_opt of NONE => ctrl_st_Typ
        | SOME(_, data_st_Typ, data_st_var_dummy) => 
                 (ctrl_st_var_dummy = data_st_var_dummy; (* forcing equal type*)
                  HOLogic.mk_prodT(ctrl_st_Typ, data_st_Typ));

  (* actual state type *)
  val st_Typ = case g_st_Typ_opt of NONE           => l_st_Typ 
                                  | SOME(g_st_Typ) => g_st_Typ;

  (* ism type *)
  (* the record definition itself is in ISM.thy *)
  val ism_name = "ism";
  val ism_typ_name = "ISM." ^ ism_name;
  val ism_Typ = Type (ism_typ_name, [cmd_Typ, pt_Typ, msg_Typ, st_Typ, domain_Typ]);
  val param_ism_Typ = Library.foldr (op -->) (map snd params, ism_Typ);

  (* transitions *)
  val trans_Typ = Type (Sign.intern_type sign "trans", 
                        [cmd_Typ, pt_Typ, msg_Typ, st_Typ, domain_Typ]);
  val transs_Typ = HOLogic.mk_setT trans_Typ;
  val param_transs_Typ = Library.foldr (op -->) (map snd params, transs_Typ);
  val transs_name = "transs";

  (* output function *)
  (* Typ: (domain \<Rightarrow> (state \<Rightarrow> msgss (port, msg) set)) *)
  (* FIXME: the output function doesn't make much sense when there is no domain defined.
   * Only create it conditionally.
   *)
  val msgss_Typ = pt_Typ --> mk_listT msg_Typ;
  val msgss_set_Typ =  HOLogic.mk_setT msgss_Typ;
  val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t 
                                             | NONE       => HOLogic.unitT;
  val outputs_Typ = dom_Typ --> st_Typ --> msgss_set_Typ;
  val param_outputs_Typ = Library.foldr (op -->) (map snd params, outputs_Typ);
  val outputs_name = "outputs";

  (* Step function *)
  (* Typ: (ins \<Rightarrow> (state, state) set) *)
  (* We could create this function out of the transition function in Isabelle directly, 
   * however, this is a little bit hard to work with.
   *)
  val state_tuple_set_Typ =  HOLogic.mk_setT (HOLogic.mk_prodT (st_Typ, st_Typ) );
  val param_steps_Typ = msgss_Typ --> state_tuple_set_Typ;
  val steps_name = "Step";

  (* domain function *)
  (* Typ: (io \<Rightarrow> action list) \<Rightarrow> domain *)
  (* FIXME: This mapping is not necessarily unique; we should check for this and only
   * allow well-formed ISMs
   *)
  val dom_fun_Typ = msgss_Typ --> dom_Typ;
  val dom_fun_name = "dom";

  (* Small note: param_ism_Typ and param_transs_Typ handle the case that the 
   * ISM is parameterised (something like 'ism AP (N::nat) =\<dots>'); in the standard 
   * case, they don't change anything.
   *)

  (* add transs and ism constants *)
  val thy = thy
    |> Theory.add_consts_i [(transs_name,  param_transs_Typ,  NoSyn)]
    |> Theory.add_consts_i [(outputs_name, param_outputs_Typ, NoSyn)]
    |> Theory.add_consts_i [(steps_name,   param_steps_Typ,   NoSyn)]
    |> Theory.add_consts_i [(dom_fun_name, dom_fun_Typ,       NoSyn)]
    |> Theory.add_consts_i [(ism_name,     param_ism_Typ,     NoSyn)]
  val sign = Theory.sign_of thy

  val types = (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, 
               ctrl_st_Typ_Term_opt, data_st_Typ_Term_opt, 
               l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt);

  (* add transs (inductive definition) *)
  val transs_Term = Sign.intern_term sign 
                    (term_of (read_cterm sign (transs_name, param_transs_Typ)));
  val param_transs_Term = Library.foldl (op $) (transs_Term, map Free params);
  val (thy, thms) = add_transs prep_rule types param_transs_Term transs (thy, []);
  val sign = Theory.sign_of thy;

  (* add outputs (inductive definition) *)
  val outputs_Term = (Sign.intern_term sign 
                    (term_of (read_cterm sign (outputs_name, param_outputs_Typ)))) 
  val param_outputs_Term = (Library.foldl (op $) (outputs_Term, map Free params))
                    $ Free ("d", dom_Typ) $ Free ("s", st_Typ);
  val (thy, thms) = add_outputs prep_rule types param_outputs_Term transs (thy, thms);
  (* not that we pass transs to add_outputs above, because we generate the outputs
   * relation from the transitions
   *)
  val sign = Theory.sign_of thy;

  (* add steps (inductive definition) *)
  val steps_Term = (Sign.intern_term sign 
                   (term_of (read_cterm sign (steps_name, param_steps_Typ)))) 
(*  val param_steps_Term = (Library.foldl (op $) (steps_Term, map Free params))
                    $ Free ("ins", msgss_Typ);
*)
  val param_steps_Term = steps_Term $ Free ("ins", msgss_Typ);
  val (thy, thms) = add_steps prep_rule types param_steps_Term transs (thy, thms);

  val sign = Theory.sign_of thy;
  val constname = Sign.intern_const sign;
  val dom_free_Var = Free("inp_var", msgss_Typ);
  val dom_if_Term = add_dom_fun prep_rule types dom_free_Var transs thy;
  val dom_if_eq = Const("==", dom_Typ --> dom_Typ --> propT) $ 
    (Const (constname dom_fun_name, dom_fun_Typ) $ dom_free_Var) $ dom_if_Term;
  val thy = thy
    |> IsarThy.add_defs_i (false, [((dom_fun_name^"_def", dom_if_eq ),[] )]);


(* Earlier, a special syntax for ISM transitions was declared here. However, no code 
 * uses it right now and it was broken by the introduction of domains. The code is
 * still there after all the real declaration as a comment (just for reference)
 *)

  (* initialize ism record *)
  val sign = Theory.sign_of thy;
  val typname = Sign.intern_type sign;
  val constname = Sign.intern_const sign;

  (* initialize init field *)
  val init_Term' =
    let
      val init_Term = 
	case ctrl_st_Typ_Term_opt of NONE =>
            (case data_st_Typ_Term_opt of NONE => dummy_Term
              | SOME(data_st_Term, _, _) => data_st_Term)
      | SOME(ctrl_st_Term, ctrl_st_Typ, _) =>
        case data_st_Typ_Term_opt of NONE => ctrl_st_Term
          | SOME(data_st_Term, data_st_Typ, _) =>
            let
	      val (pair_Const, _) = mk_pair_Const sign ctrl_st_Typ data_st_Typ;
            in
              pair_Const $ ctrl_st_Term $ data_st_Term
            end;
    in
      mk_global_st_term l_st_Typ g_st_Typ_opt thy init_Term
    end;


  val ism_Term = Library.foldl (op $) (Const (constname ism_name, param_ism_Typ), 
                               map Free params);
  val ism_make_Term = ((Const((ism_typ_name^".make"), 
    pt_set_Typ --> pt_set_Typ --> st_Typ --> transs_Typ --> ism_Typ)) $ 
    pt_set_I_Term $ pt_set_O_Term $ init_Term' $ param_transs_Term );
  val ism_eq = ((Const("==", ism_Typ --> ism_Typ --> propT)) $ ism_Term $ ism_make_Term );

  val thy = thy
    |> IsarThy.add_defs_i (false, [(("ism_def", ism_eq ),[] )]);

  (* close own namespace *)
  val thy = Theory.parent_path thy;
in
  (thy, thms, thm)
end;


fun assoc_string ([], (key:string)) = NONE
  | assoc_string ((keyi, xi) :: pairs, key) =
      if key = keyi then SOME xi else assoc_string (pairs, key);

fun read_rule sign sTs = 
  ((fst o (read_def_cterms (sign, K NONE, 
        (fn (x, ~1) => (curry assoc_string o typ_tfrees) TypeInfer.logicT x))
    (((Library.flat o (map ((map fst) o typ_tfrees))) o map snd) sTs) true)) sTs);
fun cterm_of' sign = cterm_of sign o fst;
fun rule_of sign = map (cterm_of' sign);

val add_ism   = gen_add_ism read_ctyp read_cterm read_rule;
val add_ism_i = gen_add_ism ctyp_of   cterm_of'  rule_of;



(*** package setup ***)

(** outer syntax **)

local structure P = OuterParse and K = OuterKeyword in

val ism_decl = 
  let val optional_init = Scan.optional (P.$$$ "init" |-- P.term) "arbitrary"
      val param = P.$$$ "(" |-- P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")"
      val pattern = (   (                  P.term >> (fn x => (x,false)))
                     || (P.$$$ "multi" |-- P.term >> (fn x => (x,true ))))
                    -- P.term 
      val in_pat = (P.term >> (fn x => (x,false))) -- P.term 
      val state_update = P.list1 (P.name -- (P.$$$ ":=" |-- P.term)) >> Inl 
                         ||                                 P.term   >> Inr
  in (P.name -- Scan.repeat param) -- (P.$$$ "=" |--
    (P.$$$ "ports" |-- P.typ --
      (P.$$$ "inputs"  |-- P.term --
      (P.$$$ "outputs" |-- P.term --
    (P.$$$ "messages" |-- P.typ --
    (Scan.option (P.$$$ "commands" |-- P.typ -- 
                  Scan.option (P.$$$ "default" |-- P.typ)) --
    (Scan.option (P.$$$ "domains" |-- P.typ -- 
                  Scan.option (P.$$$ "default" |-- P.typ)) --
    (P.$$$ "states" |-- Scan.option P.typ --
      (Scan.option (P.$$$ "control" |-- P.typ -- 
              (optional_init >> (fn x => (x, "dummy_control_var")))) --
      (Scan.option (P.$$$ "data"    |-- P.typ -- 
              (optional_init --
                (Scan.optional (P.$$$ "name" |-- P.term) "s"))) --
    Scan.optional (P.$$$ "transitions" |--
      Scan.repeat1 (P.thm_name ":" -- 
        (Scan.option (P.term -- ((P.$$$ "\<rightarrow>" || P.$$$ "->") |--  
                      P.term)) --
        (Scan.option   (P.$$$ "dom"  |--          P.term)     --
        (Scan.optional (P.$$$ "pre"  |--  P.list1 P.term ) [] --
        (Scan.optional (P.$$$ "in"   |--  P.list1 in_pat ) [] --
        (Scan.optional (P.$$$ "out"  |--  P.list1 pattern) [] --
        (Scan.option   (P.$$$ "cmd"  |--          P.term)     --
        (Scan.optional (P.$$$ "post" |--  state_update) (Inl []))
       )))))))) []
    )))))))))) end;

val ismP =
  OuterSyntax.command "ism" "define Interacting State Machine" K.thy_decl
   (ism_decl >> (fn ((name, params), (pt_type, (pt_set_I, (pt_set_O, (msg_type, 
   (cmd_type_default_opt, (domain_type_default_opt, (g_st_type_opt, (ctrl_st, (data_st, transs)))))))))) =>
      Toplevel.theory
        (#1 o add_ism name params pt_type pt_set_I pt_set_O msg_type 
                   cmd_type_default_opt domain_type_default_opt 
                   g_st_type_opt ctrl_st data_st transs)));

val _ = OuterSyntax.add_keywords 
["ports", "inputs", "outputs", "messages", "commands", "default",
 "domains", "states", "control", "init", "data", "name", "multi",
 "transitions", "\<rightarrow>", "->", "pre", "in", "out", "cmd", "dom", "post",":="];

val _ = OuterSyntax.add_parsers [ismP];

end; (* local *)


end;
*}
end
(*>*) 
theory SLE66 imports ISM_package  --{* we build on the general ISM definitions *}
begin
ML {* Pretty.setmargin 169; quick_and_dirty:=false *}
use_thy "../awe-0.4/Extensions/AWE"
typedecl fn               --{* function name *}
typedecl dn               --{* data object name *}
datatype on = F fn | D dn --{* object name *}
consts
  f_SN   :: "fn"      --{* the name of the function giving the serial number *}
  FTest0 :: "fn set"  --{* the names of test functions of phase 0 *}
  FTest1 :: "fn set"  --{* the names of test functions of phase 1 *}
  FTest  :: "fn set"  --{* the names of all test functions *}
  F_Sec  :: "fn set"  --{* the names of all security-relevant functions *}
  F_PSec :: "fn set"  --{* the subset of @{term F_Sec} relevant for the processor *}
  F_ASec :: "fn set"  --{* the names of @{term F_Sec} relevant for applications *}
  F_NSec :: "fn set"  --{* the names of all non-security-relevant functions *}
  D_Sec  :: "dn set"  --{* the names of all security-relevant data objects *}
  D_PSec :: "dn set"  --{* the subset of @{term D_Sec} relevant for the processor *}
  D_ASec :: "dn set"  --{* the names of @{term D_Sec} relevant for applications *}
  D_NSec :: "dn set"  --{* the names of all non-security-relevant data objects *}
    Sec  :: "on set"  --{* the names of all security-relevant objects *}
defs
  FTest_def:  "FTest  \<equiv> FTest0 \<union> FTest1"
  F_ASec_def: "F_ASec \<equiv> F_Sec - F_PSec"
  D_ASec_def: "D_ASec \<equiv> D_Sec - D_PSec"
  F_NSec_def: "F_NSec \<equiv> -F_Sec"
  D_NSec_def: "D_NSec \<equiv> -D_Sec"
  Sec_def: "Sec \<equiv> {F fn |fn. fn \<in> F_Sec} \<union> {D dn |dn. dn \<in> D_Sec}"
axioms 
  f_SN_not_FTest:   "f_SN \<notin> FTest"

lemmas f_SN_not_FTest [simp]
lemma [simp]: "(- FTest0 \<inter> - FTest) = (- FTest)" by (auto simp: FTest_def)
lemma [simp]: "(- FTest1 \<inter> - FTest) = (- FTest)" by (auto simp: FTest_def)

datatype ph = P0 | P1 | P2 | Error

typedecl val --{* data and function values *}
consts SN :: val --{* serial number *}

record chip_data = 
  valF :: "fn \<rightharpoonup> val"
  valD :: "dn \<rightharpoonup> val"

translations "chip_data" \<leftharpoondown> (type) "\<lparr>valF :: fn \<rightharpoonup> val, valD :: dn \<rightharpoonup> val\<rparr>"

constdefs 
  val :: "chip_data \<Rightarrow> on \<rightharpoonup> val"
 "val s on \<equiv> case on of F fn \<Rightarrow> valF s fn  | D dn \<Rightarrow> valD s dn"

types SLE66_state = "ph \<times> chip_data"

translations "SLE66_state" \<leftharpoondown> (type) "ph \<times> chip_data"

constdefs
  fct :: "chip_data \<Rightarrow> fn set"
 "fct s \<equiv> dom (valF s)"

lemma dom_valF_fct [simp]: "f \<in> dom (valF s) = (f \<in> fct s)"
by (auto simp: fct_def)

lemma fct_upd_valF [simp]: "fct (s\<lparr>valF := f\<rparr>) = dom f" 
by(auto simp: fct_def)

consts
 "output"   :: "fn \<Rightarrow> chip_data \<Rightarrow> val"
 "change"   :: "fn \<Rightarrow> chip_data \<Rightarrow> chip_data"  
 "positive" :: "val \<Rightarrow> bool" 

datatype interface = In | Out

typedecl sb      (* --{* subjects *}*)
consts Pmf :: sb (* --{* processor manufacturer *}*)

datatype message = 
  Exec sb fn | Load sb fn val | Spy on  --{* input *}
| Val val | Ok | No                     --{* output *}

consts subject :: "message \<Rightarrow> sb"
primrec
  "subject (Exec sb fn  ) = sb"
  "subject (Load sb fn v) = sb"

subsection "ISM definition"

ism SLE66 =
  ports interface
    inputs \<spacespace>"{In}"
    outputs "{Out}"
  messages message
  states
    control ph init "P0" 
    data   chip_data name "s"

  transitions

  R00: P0 \<rightarrow> P1
    pre "f \<in> fct s\<inter>FTest0", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest0)"
  R01: P0 \<rightarrow> P2
    pre "f \<in> fct s\<inter>FTest1", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest)"
  R02: P0 \<rightarrow> Error
    pre "f \<in> fct s\<inter>FTest0", "\<not>positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[No]"
  R03: P0 \<rightarrow> P0
    pre "f \<in> fct s - FTest"
    in  In  "[Exec Pmf f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R04: P0 \<rightarrow> P0
    pre "sb \<noteq> Pmf \<or> f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R11: P1 \<rightarrow> P2
    pre "f \<in> fct s\<inter>FTest1", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest1)"
  R12: P1 \<rightarrow> Error 
    pre "f \<in> fct s\<inter>FTest1", "\<not>positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[No]"
  R13: P1 \<rightarrow> P1
    pre "f \<in> fct s - FTest1"
    in  In  "[Exec Pmf f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R14: P1 \<rightarrow> P1
    pre "sb \<noteq> Pmf \<or> f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R21: P2 \<rightarrow> P2
    pre "f \<in> fct s"
    in  In  "[Exec sb f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R22: P2 \<rightarrow> P2
    pre "f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R31: Error \<rightarrow> Error
    pre "f_SN \<in> fct s"
    in  In  "[Exec sb f_SN]"
    out Out "[Val SN]"
  R32: Error \<rightarrow> Error
    pre "f \<notin> fct s\<inter>{f_SN}"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R41: P1 \<rightarrow> P1
    pre "f \<in> F_NSec \<union> (F_ASec - fct s)"
    in  In  "[Load Pmf f v]"
    out Out "[Ok]"
    post valF := "valF s(f\<mapsto>v)"
  R42: ph \<rightarrow> ph
    pre "f \<notin> F_NSec \<union> (F_ASec - fct s) \<or> sb \<noteq> Pmf \<or> ph \<noteq> P1"
    in  In  "[Load sb f v]"
    out Out "[No]"
  R51: ph \<rightarrow> ph
    pre "on \<notin> Sec", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "case val s on of None \<Rightarrow> [] | Some v \<Rightarrow> [Val v]"
  R52: ph \<rightarrow> Error
    pre "on \<in> Sec", "v \<in> {[],[Val (the (val s on))]}", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "v"
    post "any"
  R52':ph \<rightarrow> ph
    pre "on \<in> Sec", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "[]"
  R53: Error \<rightarrow> Error
    in  In  "[Spy on]"
    out Out "[]"
    post "any"

lemma trans_ism [simp]: "ism.trans ism = transs"
by (simp add: ism_def ism.defs)

constdefs
  unwind :: "SLE66_state \<Rightarrow> on set \<Rightarrow> SLE66_state \<Rightarrow> bool"
 ("_/ ~_~/ _" [61, 61, 61] 60)
 "s ~A~ t \<equiv> fst s = fst t \<and> fct (snd s) = fct (snd t) \<and>
            (\<forall>on\<in>A. val (snd s) on = val (snd t) on)"

lemma unwind_def2: "(ph, s) ~A~ (ph',t) = (ph = ph' \<and> fct s = fct t \<and>
                      (\<forall>fn. F fn \<in> A \<longrightarrow> valF s fn = valF t fn) \<and>
                      (\<forall>dn. D dn \<in> A \<longrightarrow> valD s dn = valD t dn))"
by (auto simp add: unwind_def val_def split add: on.split)

lemma unwind_ph_fct_D: "(ph, s) ~A~ (ph',t) \<Longrightarrow> ph = ph' \<and> fct s = fct t"
by (simp add: unwind_def2)

theorem noleak_Sec_determ: "\<And>s t. \<lbrakk>s ~-Sec~ t; 
  s \<in> reach ism; ((p,s),c,(p' ,s')) \<in> transs;
  t \<in> reach ism; ((p,t),c,(p'',t')) \<in> transs; 
  fst s' \<noteq> Error; fst t' \<noteq> Error\<rbrakk> \<Longrightarrow> p' = p'' \<and> s' ~-Sec~ t'"
apply (clarsimp, frule unwind_ph_fct_D, clarify)
apply (erule SLE66.transs.elims)
apply (safe del: conjI IntI disjE UnE insertE)
apply (erule_tac [!] SLE66.transs.elims, simp_all)
oops

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.