(*  Title:      NI/Generics.thy
    Id:         $Id: Generics.thy,v 1.6 2004/01/29 17:36:46 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Generic notions *}

(*<*)
theory Generics imports System begin

(*>*)

subsection "policies"

(*<*)
hide const dom 
(*>*)
consts dom        :: "action => domain"           --{* security domain *}
       policy     :: "domain => domain => bool"  ("(_\ \<leadsto>\ _)"(*<*) [46,46] 45(*>*))
syntax policy_neg :: "domain => domain => bool"  ("(_\ \<notleadsto>\ _)"(*<*) [46,46] 45(*>*))
translations "u \<notleadsto> v" \<rightleftharpoons> "\<not>(u \<leadsto> v)"

axioms policy_refl: "u \<leadsto> u"

locale policy_trans =
  assumes policy_trans: "\<lbrakk>u \<leadsto> v; v \<leadsto> w\<rbrakk> \<Longrightarrow> u \<leadsto> w"
(*<*)

lemma (in policy_trans) rev_policy_trans: "\<lbrakk>u \<notleadsto> w; v \<leadsto> w\<rbrakk> \<Longrightarrow> u \<notleadsto> v"
by (blast intro: policy_trans)

(*>*)
subsection "allowed source domains"

types sourcef = "action list => domain => domain set"

subsubsection "trivial source functions"

constdefs
  singleton :: "sourcef"
 "singleton as u \<equiv> {u}"

  tsources :: "sourcef"
 "tsources as u \<equiv> {w. w \<leadsto> u}"
(*<*)

declare singleton_def [simp]

lemma singleton_iff [iff]: "v \<in> singleton as u = (v = u)"
by (simp)

(*>*)
subsubsection "chains of domains"

consts gen_chain :: "(domain => action => bool) => sourcef"
primrec 
  Nil:  "gen_chain P []     u = {u}"
  Cons: "gen_chain P (a#as) u = gen_chain P as u \<union> 
                    {w. P w a \<and> (\<exists>v. w \<leadsto> v \<and> v \<in> gen_chain P as u)}"

lemma gen_chain_refl: "u \<in> gen_chain P as u" 
(*<*)
by (induct "as", auto)

(*>*)
lemma gen_chain_trans: 
  "\<lbrakk>w \<leadsto> v; v \<in> gen_chain P as u; P w a\<rbrakk> \<Longrightarrow> w \<in> gen_chain P (a#as) u"
(*<*)
by (induct "as", auto)
lemma rev_gen_chain_trans: 
  "w \<notin> gen_chain P (a#as) u \<Longrightarrow> \<not>(\<exists>u\<in>gen_chain P as u. w \<leadsto> u \<and> P w a)"
by (blast intro: gen_chain_trans)

lemma gen_chain_direct: "\<lbrakk>w \<leadsto> u; P w a\<rbrakk> \<Longrightarrow> w \<in> gen_chain P (a#as) u"
by (blast intro: gen_chain_refl gen_chain_trans)
lemma rev_gen_chain_direct: "w \<notin> gen_chain P (a#as) u \<Longrightarrow> \<not> (w \<leadsto> u \<and> P w a)"
by (blast intro: gen_chain_direct)

(*>*)
lemma gen_chain_subset_Cons: "gen_chain P as u \<subseteq> gen_chain P (a#as) u"
(*<*)
by (induct "as", auto)

lemma singleton_subset_gen_chain: "singleton as u \<subseteq> gen_chain P as u"
by (blast intro!: gen_chain_refl)

lemma gen_chain_append2 [rule_format]: 
  "\<forall>bs. v \<in> gen_chain P bs u \<longrightarrow> v \<in> gen_chain P (as @ bs) u"
by (induct "as", auto)

lemma (in policy_trans) gen_chain_implies_policy_lemma [rule_format]:
  "\<forall>w. w \<in> gen_chain P as u \<longrightarrow> w \<leadsto> u"
apply (induct "as")
apply  (simp_all add: policy_refl)
apply (fast dest: policy_trans)
done
(*>*)
lemma (in policy_trans) gen_chain_implies_policy:  --{* Rushby's Lemma 6 *}
  "w \<in> gen_chain P as u \<Longrightarrow> w \<leadsto> u"
(*<*)
by (erule gen_chain_implies_policy_lemma)

lemma (in policy_trans) gen_chain_subset_tsources:
 "gen_chain P as u \<subseteq> tsources as u"
by (auto simp add: tsources_def elim: gen_chain_implies_policy)

lemma in_gen_chain_Cons_eq_lemma: 
  "P w a \<Longrightarrow> w \<in> gen_chain P (a#as) u <-> (\<exists>v. w \<leadsto> v \<and> v \<in> gen_chain P as u)"
by (auto intro!: policy_refl)
(*>*)
lemma (in policy_trans) in_gen_chain_Cons_eq: 
  "P w a \<Longrightarrow> w \<in> gen_chain P (a#as) u <-> w \<leadsto> u"
(*<*)
apply (rule)
apply  (erule gen_chain_implies_policy)
apply (simp only: in_gen_chain_Cons_eq_lemma)
apply (blast intro: gen_chain_refl)
done

lemma gen_chain_mono: 
  "\<forall>w a. P w a \<longrightarrow> Q w a \<Longrightarrow> gen_chain P as u \<subseteq> gen_chain Q as u"
by (induct "as", auto)

(*>*)

constdefs 
  chain :: "sourcef"
 "chain \<equiv> gen_chain (\<lambda>w a. True)"

lemma (in policy_trans) chain_subset_tsources: "chain as u \<subseteq> tsources as u"
(*<*)
by (simp add: chain_def gen_chain_subset_tsources)

lemma chain_Nil [simp]: "chain [] u = {u}"
by (simp add: chain_def)
(*>*)

constdefs
  sources :: "sourcef"
 "sources \<equiv> gen_chain (\<lambda>w a. w = dom a)"

lemma sources_subset_chain: "sources as u \<subseteq> chain as u"
(*<*)
by (unfold sources_def chain_def, rule gen_chain_mono, blast)

lemma singleton_subset_sources: "singleton as u \<subseteq> sources as u"
by (simp only: sources_def singleton_subset_gen_chain)

lemma sources_Nil [simp]: "sources [] u = {u}"
by (simp add: sources_def)

lemma sources_Cons: "sources (a#as) u = sources as u \<union> 
      (if (\<exists>v. dom a \<leadsto> v \<and> v \<in> sources as u) then {dom a} else {})"
by (auto simp: sources_def)

lemma sources_subset_Cons: "sources as u \<subseteq> sources (a#as) u"
by (auto simp add: sources_Cons)

lemma sources_refl: "u \<in> sources as u" 
by (simp add: sources_def gen_chain_refl)

lemma sources_trans: 
  "dom a \<leadsto> v \<Longrightarrow> v \<in> sources as u \<Longrightarrow> dom a \<in> sources (a#as) u"
by (auto simp only: sources_def intro: gen_chain_trans)
lemma rev_sources_trans: 
 "dom a \<notin> sources (a#as) u \<Longrightarrow> \<not>(\<exists>u\<in>sources as u. dom a \<leadsto> u)"
by (auto simp only: sources_def dest: rev_gen_chain_trans)

lemma rev_sources_direct: "dom a \<notin> sources (a#as) u \<Longrightarrow> (dom a \<notleadsto> u)"
by (auto simp only: sources_def dest: rev_gen_chain_direct)

lemma dom_in_sources_Cons_eq_lemma: 
  "dom a \<in> sources (a#as) u <-> (\<exists>v. dom a \<leadsto> v \<and> v \<in> sources as u)"
by (simp only: sources_def in_gen_chain_Cons_eq_lemma)

lemma (in policy_trans) dom_in_sources_Cons_eq: 
  "dom a \<in> sources (a#as) u <-> dom a \<leadsto> u"
by (simp only: sources_def in_gen_chain_Cons_eq)

(*>*)
--{* \pagebreak *}
subsection "unwinding relations"

consts uwr :: "state => domain => state => bool"  ("(_\ \<sim>_\<sim>\ _)"(*<*) [46,46,46] 45(*>*))

axioms
  uwr_s0: "s0 \<sim>u\<sim> s0"
(*<*)

locale uwr_refl = 
  assumes uwr_refl: "s \<sim>u\<sim> s"
locale uwr_trans =
  assumes uwr_trans: "\<lbrakk>r \<sim>u\<sim> s; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> r \<sim>u\<sim> t"
(*>*)

constdefs gen_uwr :: "state => domain set => state => bool" 
 (*<*)("(_\ \<approx>_\<approx>\ _)" [46,46,46] 45) (*>*)
 "s \<approx>us\<approx> t \<equiv> \<forall>u\<in>us. s \<sim>u\<sim> t"
(*<*)
lemma gen_uwrI: "(!!u. u\<in>us \<Longrightarrow> s \<sim>u\<sim> t) \<Longrightarrow> s \<approx>us\<approx> t"
by (simp add: gen_uwr_def)

lemma gen_uwrD: "\<lbrakk>s \<approx>us\<approx> t; u\<in>us\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> t"
by (simp add: gen_uwr_def)

lemma gen_uwr_empty [simp]: "s \<approx>{}\<approx> t"
by (auto simp add: gen_uwr_def)

lemma gen_uwr_insert [simp]: "s \<approx>insert u us\<approx> t <-> s \<sim>u\<sim> t \<and> s \<approx>us\<approx> t"
by (auto simp add: gen_uwr_def)
(*
lemma gen_uwr_singleton [simp]: "s \<approx>{u}\<approx> t <-> s \<sim>u\<sim> t"
by (simp)
*)
lemma gen_uwr_Union [simp]: "s \<approx>us \<union> vs\<approx> t <-> s \<approx>us\<approx> t \<and> s \<approx>vs\<approx> t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_s0: "s0 \<approx>us\<approx> s0"
by (rule gen_uwrI, rule uwr_s0)

lemma (in uwr_refl) gen_uwr_refl: "s \<approx>us\<approx> s"
by (rule gen_uwrI, rule uwr_refl)

lemma (in uwr_trans) gen_uwr_trans: "r \<approx>us\<approx> s \<Longrightarrow> s \<approx>us\<approx> t \<Longrightarrow> r \<approx>us\<approx> t"
by (blast intro: gen_uwrI uwr_trans dest: gen_uwrD)

lemma gen_uwr_mono: "s \<approx>vs\<approx> t \<Longrightarrow> us \<subseteq> vs \<Longrightarrow> s \<approx>us\<approx> t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_uwr: 
  "\<lbrakk>s \<approx>us\<approx> t; (!!u. \<lbrakk>s \<sim>u\<sim> t; u \<in> us\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t')\<rbrakk> \<Longrightarrow> s' \<approx>us\<approx> t'"
by (blast intro: gen_uwrI dest: gen_uwrD)
(*>*)

constdefs nest_uwr :: "state => domain => state => bool" 
  (*<*)("(_\ \<simeq>_\<simeq>\ _)" [46,46,46] 45) (*>*)
  "s \<simeq>u\<simeq> t \<equiv> s \<approx>{v. v \<leadsto> u}\<approx> t"

lemma tsources_uwr_is_nest(*<*) [simp](*>*): "s \<approx>tsources as u\<approx> t <-> s \<simeq>u\<simeq> t"
(*<*)
by (simp add: tsources_def nest_uwr_def)

lemma nest_uwrI: "(!!v. v\<leadsto>u \<Longrightarrow> s \<sim>v\<sim> t) \<Longrightarrow> s \<simeq>u\<simeq> t" 
by (auto simp add: nest_uwr_def intro: gen_uwrI)

lemma nest_uwrD: "\<lbrakk>s \<simeq>u\<simeq> t; v \<leadsto> u\<rbrakk> \<Longrightarrow> s \<sim>v\<sim> t" 
by (auto simp add: nest_uwr_def dest: gen_uwrD)

lemma nest_uwr_s0: "s0 \<simeq>u\<simeq> s0" 
by (blast intro: nest_uwrI uwr_s0)

lemma nest_uwr_implies_uwr: "s \<simeq>u\<simeq> t \<Longrightarrow> s \<sim>u\<sim> t"
by (blast intro: policy_refl nest_uwrD)
(*>*)

lemma (in policy_trans) nesting: "\<lbrakk>s \<simeq>v\<simeq> t; u \<leadsto> v\<rbrakk> \<Longrightarrow> s \<simeq>u\<simeq> t" 
(*<*)
by (blast intro: nest_uwrI dest: nest_uwrD policy_trans)

lemma gen_chain_uwr_ConsD: 
 "s \<approx>gen_chain P (a # as) u\<approx> t \<Longrightarrow> 
  (w \<leadsto> v \<longrightarrow> v \<in> gen_chain P as u \<longrightarrow> P w a \<longrightarrow> s \<sim>w\<sim> t) \<and> 
   s \<approx>gen_chain P as u\<approx> t"
by (auto simp add: dest: gen_uwrD)

lemma chain_uwr_ConsD: 
 "s \<approx>chain (a # as) u\<approx> t \<Longrightarrow> (v \<in> chain as u \<longrightarrow> s \<simeq>v\<simeq> t) \<and> s \<approx>chain as u\<approx> t"
by (unfold chain_def, 
       blast intro!: nest_uwrI dest: gen_chain_uwr_ConsD)

lemma sources_uwr_ConsD: 
  "s \<approx>sources (a#as) u\<approx> t \<Longrightarrow> 
  (dom a \<leadsto> v \<longrightarrow> v \<in> sources as u \<longrightarrow> s \<sim>dom a\<sim> t) \<and> 
   s \<approx>sources as u\<approx> t"
by (unfold sources_def, blast dest: gen_chain_uwr_ConsD)

declare gen_chain.Cons [simp del]

lemma (in policy_trans) nest_uwr_implies_gen_chain_uwr: 
 "s \<simeq>u\<simeq> t \<Longrightarrow> s \<approx>gen_chain P as u\<approx> t"
by (blast intro: gen_uwrI nest_uwrD gen_chain_implies_policy)
(*>*)

constdefs 
  output_consistent :: "bool"
 "output_consistent \<equiv> \<forall>u s t. s \<sim>u\<sim> t \<longrightarrow> output u s = output u t"
(*<*)
lemma output_consistentD:
  "\<lbrakk>output_consistent; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> output u s = output u t"
by (simp add: output_consistent_def)

(*>*)
(*--{* \pagebreak *}*)
subsection "the deterministic case"

constdefs 
  obs_equiv :: "state => action list => domain => action list => state => bool"
("(_\ \<simeq>_,_,_\<simeq>\ _)"(*<*) [46,46,46,46,46] 45(*>*))
  "s \<simeq>as,u,bs\<simeq> t \<equiv> output u (run as s) = output u (run bs t)"
(*<*)
lemma obs_equivI: "\<lbrakk>output_consistent; run as s \<sim>u\<sim> run bs t\<rbrakk> \<Longrightarrow> s \<simeq>as,u,bs\<simeq> t"
by (unfold obs_equiv_def, erule (1) output_consistentD)
(*>*)

constdefs 
  weakly_step_consistent :: "bool" --{* sufficient also for transitive policies,
new premise @{term "dom a \<leadsto> u"} *}
 "weakly_step_consistent \<equiv> \<forall>a u s t. dom a \<leadsto> u \<longrightarrow> s \<sim>dom a\<sim> t \<longrightarrow> 
                               s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"
constdefs 
  step_respect :: "bool" --{* a consequence of @{text "local_respect"} *}
 "step_respect \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"
(*<*)
lemma weakly_step_consistentD:  
 "\<lbrakk>weakly_step_consistent; s \<sim>u\<sim> t; dom a \<leadsto> u; s \<sim>dom a\<sim> t\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> step a t"
by (simp add: weakly_step_consistent_def)

lemma step_respectD: 
  "\<lbrakk>step_respect; s \<sim>u\<sim> t; dom a \<notleadsto> u\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> step a t"
by (simp add: step_respect_def)
(*>*)

constdefs
  gen_weak_step_consistent_respect :: "(domain => action => bool) => bool"
 "gen_weak_step_consistent_respect P \<equiv> \<forall>a u s t. (\<forall>w. P w a \<longrightarrow> w\<leadsto>u \<longrightarrow> s \<sim>w\<sim> t) \<longrightarrow> 
                               s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"

lemma gen_weak_step_consistent_respect_action:
"\<lbrakk>weakly_step_consistent; step_respect\<rbrakk> \<Longrightarrow> 
  gen_weak_step_consistent_respect (\<lambda>w a. w = dom a)"
(*<*)
apply (clarsimp simp add: gen_weak_step_consistent_respect_def)
apply (case_tac "dom a \<leadsto> u")
apply  (blast dest: weakly_step_consistentD)
apply (blast dest: step_respectD)
done
(*>*)

lemma gen_chain_unwinding_step:
"\<lbrakk>s \<approx>gen_chain P (a#as) u\<approx> t; gen_weak_step_consistent_respect P\<rbrakk> \<Longrightarrow> 
  step a s \<approx>gen_chain P as u\<approx> step a t"
(*<*)
apply (rule gen_uwr_uwr)
apply  (erule gen_chain_uwr_ConsD [THEN conjunct2])
apply (simp add: gen_weak_step_consistent_respect_def)
apply (blast dest: gen_chain_uwr_ConsD [THEN conjunct1])
done
(*>*)

lemma sources_unwinding_step: --{* Rushby's Lemma 3 *}
"\<lbrakk>s \<approx>sources (a#as) u\<approx> t; weakly_step_consistent; step_respect\<rbrakk> \<Longrightarrow> 
  step a s \<approx>sources as u\<approx> step a t"
(*<*) 
apply (unfold sources_def)
apply (erule gen_chain_unwinding_step)
apply (erule (1) gen_weak_step_consistent_respect_action)
done
(*>*)
--{* \pagebreak *}

subsection "the nondeterministic case"

--{* TODO: reachability *}

constdefs 
  obs_PO :: "state => action list => domain => action list => state => bool"  
("(_\ \<lesssim>_,_,_\<lesssim>\ _)"(*<*) [46,46,46,46,46] 45(*>*))
  "s \<lesssim>as,u,bs\<lesssim> t \<equiv> \<forall>s'. (s, s') \<in> Run as \<longrightarrow> 
                    (\<exists>t'. (t, t') \<in> Run bs \<and> output u s' = output u t')"
(*<*)
lemma obs_POI: "\<lbrakk>output_consistent; 
\<forall>s'. (s, s') \<in> Run as \<longrightarrow> (\<exists>t'. (t, t') \<in> Run bs \<and> s' \<sim>u\<sim> t')\<rbrakk> \<Longrightarrow> s \<lesssim>as,u,bs\<lesssim> t"
by (unfold obs_PO_def, fast dest: output_consistentD)

(*>*)
subsubsection "simple version"

constdefs 
  Step_consistent :: "bool"
 "Step_consistent \<equiv> \<forall>a u s s' t. dom a \<leadsto> u \<longrightarrow> 
  (s, s') \<in> Step a \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t')"

  Step_respect :: "bool" --{* a consequence of @{text "Local_respect"} *}
 "Step_respect \<equiv> \<forall>a u s s' t. dom a \<notleadsto> u \<longrightarrow> 
  (s, s') \<in> Step a \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t')"
(*<*)

lemma Step_consistentD:  
 "\<lbrakk>(s, s') \<in> Step a; Step_consistent; s \<sim>u\<sim> t; dom a \<leadsto> u\<rbrakk> \<Longrightarrow>
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'" 
by (simp add: Step_consistent_def)

lemma Step_respectD: 
  "\<lbrakk>Step_respect; (s, s') \<in> Step a; s \<sim>u\<sim> t; dom a \<notleadsto> u\<rbrakk> \<Longrightarrow> 
    \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'" 
by (simp add: Step_respect_def)
(*>*)

lemma simple_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<sim>u\<sim> t; Step_consistent; Step_respect \<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<sim>u\<sim> t'"
(*<*)
apply (case_tac "dom a \<leadsto> u")
apply  (drule (3) Step_consistentD, fast)
apply (blast dest: Step_respectD) 
done
(*>*)

subsubsection "uniform version"

constdefs 
  uni_Step_consistent :: "bool" --{* uniform *}
 "uni_Step_consistent \<equiv> \<forall>a us s s' t. (\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> s \<sim>dom a\<sim> t \<longrightarrow> 
      (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
(\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"

  uni_Step_respect :: "bool"
 "uni_Step_respect \<equiv> \<forall>a us s t s'.  \<not>(\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow>
        (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
  (\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"
(*<*)
lemma uni_Step_consistentD:  
 "\<lbrakk>(s, s') \<in> Step a; uni_Step_consistent; s \<approx>us\<approx> t; \<exists>u\<in>us. dom a \<leadsto> u; 
   s \<sim>dom a\<sim> t\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t'"
by (unfold uni_Step_consistent_def, blast)

lemma uni_Step_respectD [rule_format]: 
  "\<lbrakk>uni_Step_respect; s \<approx>us\<approx> t; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); 
    (s, s') \<in> Step a; u\<in>us\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t'" 
by (unfold uni_Step_respect_def, blast)
(*>*)

constdefs
  gen_uni_Step_consistent_respect :: "(domain => action => bool) => bool"
 "gen_uni_Step_consistent_respect P \<equiv> \<forall>a s us t s'. 
   (\<forall>w. P w a \<longrightarrow> (\<exists>u\<in>us. w \<leadsto> u) \<longrightarrow> s \<sim>w\<sim> t) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow> 
         (s, s') \<in> Step a \<longrightarrow> s \<approx>us\<approx> t \<longrightarrow> 
   (\<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>us\<approx> t')"

lemma gen_chain_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<approx>gen_chain P (a#as) u\<approx> t; 
        gen_uni_Step_consistent_respect P\<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>gen_chain P as u\<approx> t'"
(*<*)
apply (frule gen_chain_uwr_ConsD [THEN conjunct2])
apply (simp add: gen_uni_Step_consistent_respect_def)
apply (blast dest: gen_chain_uwr_ConsD [THEN conjunct1] 
       intro: gen_chain_refl)
done

lemma gen_uni_Step_consistent_respect_action:
"\<lbrakk>uni_Step_consistent; uni_Step_respect\<rbrakk> \<Longrightarrow> 
  gen_uni_Step_consistent_respect (\<lambda>w a. w = dom a)"
apply (clarsimp simp add: gen_uni_Step_consistent_respect_def)
apply (case_tac "\<exists>v\<in>us. dom a \<leadsto> v")
apply  (blast dest: uni_Step_consistentD)
apply (blast dest: uni_Step_respectD)
done
(*>*)

lemma sources_unwinding_Step:
      "\<lbrakk>(s, s') \<in> Step a; s \<approx>sources (a#as) u\<approx> t;
        uni_Step_consistent; uni_Step_respect\<rbrakk> \<Longrightarrow> 
  \<exists>t'. (t, t') \<in> Step a \<and> s' \<approx>sources as u\<approx> t'"
(*<*)
apply (unfold sources_def)
apply (erule (1) gen_chain_unwinding_Step)
apply (erule (1) gen_uni_Step_consistent_respect_action)
done
(*>*)

locale Step_functional =
  assumes Step_functional: "\<lbrakk>(x, y) \<in> Step a; (x, z) \<in> Step a\<rbrakk> \<Longrightarrow> y = z"

lemma (in Step_functional) uni_Step_consistent: 
  "Step_respect \<Longrightarrow> Step_consistent \<Longrightarrow> uni_Step_consistent"
(*<*)
apply (simp add: uni_Step_consistent_def, safe)
(*
apply  (clarsimp simp add: Step_consistent_def)
apply  (drule spec, drule_tac x = "{u}" in spec, force)
*)
apply (frule (1) gen_uwrD)
apply (frule (3) Step_consistentD)
apply (clarify, rule exI, rule conjI, assumption)
apply (thin_tac "x \<in> us")
apply (thin_tac "s \<sim>x\<sim> t")
apply (thin_tac "s' \<sim>x\<sim> t'")
apply (thin_tac "dom a \<leadsto> x")
apply (erule gen_uwr_uwr)
apply (case_tac "dom a \<leadsto> u")
apply  (fast dest: Step_consistentD Step_functional)
apply (fast dest: Step_respectD Step_functional)
done
(*>*)

lemma (in Step_functional) uni_Step_respect: "uni_Step_respect = Step_respect"
(*<*)
apply (unfold uni_Step_respect_def, safe)
apply  (clarsimp simp add: Step_respect_def)
apply  (drule spec, drule_tac x = "{u}" in spec, force)
apply (frule (1) gen_uwrD)
apply (frule (2) Step_respectD, blast, clarify)
apply (rule exI, rule conjI, assumption)
apply (erule gen_uwr_uwr)
apply (drule (2) Step_respectD, blast, fast dest: Step_functional)
done

end
(*>*)