Theory Generics

(*  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 = System:

(*>*)

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> "¬(u \<leadsto> v)"

axioms policy_refl: "u \<leadsto> u"

locale policy_trans =
  assumes policy_trans: "[|u \<leadsto> v; v \<leadsto> w|] ==> u \<leadsto> w"
(*<*)

lemma (in policy_trans) rev_policy_trans: "[|u \<notleadsto> w; v \<leadsto> w|] ==> 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 ≡ {u}"

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

declare singleton_def [simp]

lemma singleton_iff [iff]: "v ∈ 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 ∪ 
                    {w. P w a ∧ (∃v. w \<leadsto> v ∧ v ∈ gen_chain P as u)}"

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

(*>*)
lemma gen_chain_trans: 
  "[|w \<leadsto> v; v ∈ gen_chain P as u; P w a|] ==> w ∈ gen_chain P (a#as) u"
(*<*)
by (induct "as", auto)
lemma rev_gen_chain_trans: 
  "w ∉ gen_chain P (a#as) u ==> ¬(∃u∈gen_chain P as u. w \<leadsto> u ∧ P w a)"
by (blast intro: gen_chain_trans)

lemma gen_chain_direct: "[|w \<leadsto> u; P w a|] ==> w ∈ gen_chain P (a#as) u"
by (blast intro: gen_chain_refl gen_chain_trans)
lemma rev_gen_chain_direct: "w ∉ gen_chain P (a#as) u ==> ¬ (w \<leadsto> u ∧ P w a)"
by (blast intro: gen_chain_direct)

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

lemma singleton_subset_gen_chain: "singleton as u ⊆ gen_chain P as u"
by (blast intro!: gen_chain_refl)

lemma gen_chain_append2 [rule_format]: 
  "∀bs. v ∈ gen_chain P bs u --> v ∈ gen_chain P (as @ bs) u"
by (induct "as", auto)

lemma (in policy_trans) gen_chain_implies_policy_lemma [rule_format]:
  "∀w. w ∈ gen_chain P as u --> 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 ∈ gen_chain P as u ==> w \<leadsto> u"
(*<*)
by (erule gen_chain_implies_policy_lemma)

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

lemma in_gen_chain_Cons_eq_lemma: 
  "P w a ==> w ∈ gen_chain P (a#as) u <-> (∃v. w \<leadsto> v ∧ v ∈ gen_chain P as u)"
by (auto intro!: policy_refl)
(*>*)
lemma (in policy_trans) in_gen_chain_Cons_eq: 
  "P w a ==> w ∈ 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: 
  "∀w a. P w a --> Q w a ==> gen_chain P as u ⊆ gen_chain Q as u"
by (induct "as", auto)

(*>*)

constdefs 
  chain :: "sourcef"
 "chain ≡ gen_chain (λw a. True)"

lemma (in policy_trans) chain_subset_tsources: "chain as u ⊆ 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 ≡ gen_chain (λw a. w = dom a)"

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

lemma singleton_subset_sources: "singleton as u ⊆ 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 ∪ 
      (if (∃v. dom a \<leadsto> v ∧ v ∈ sources as u) then {dom a} else {})"
by (auto simp: sources_def)

lemma sources_subset_Cons: "sources as u ⊆ sources (a#as) u"
by (auto simp add: sources_Cons)

lemma sources_refl: "u ∈ sources as u" 
by (simp add: sources_def gen_chain_refl)

lemma sources_trans: 
  "dom a \<leadsto> v ==> v ∈ sources as u ==> dom a ∈ sources (a#as) u"
by (auto simp only: sources_def intro: gen_chain_trans)
lemma rev_sources_trans: 
 "dom a ∉ sources (a#as) u ==> ¬(∃u∈sources as u. dom a \<leadsto> u)"
by (auto simp only: sources_def dest: rev_gen_chain_trans)

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

lemma dom_in_sources_Cons_eq_lemma: 
  "dom a ∈ sources (a#as) u <-> (∃v. dom a \<leadsto> v ∧ v ∈ 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 ∈ 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"  ("(_\ ∼_∼\ _)"(*<*) [46,46,46] 45(*>*))

axioms
  uwr_s0: "s0 ∼u∼ s0"
(*<*)

locale uwr_refl = 
  assumes uwr_refl: "s ∼u∼ s"
locale uwr_trans =
  assumes uwr_trans: "[|r ∼u∼ s; s ∼u∼ t|] ==> r ∼u∼ t"
(*>*)

constdefs gen_uwr :: "state => domain set => state => bool" 
 (*<*)("(_\ ≈_≈\ _)" [46,46,46] 45) (*>*)
 "s ≈us≈ t ≡ ∀u∈us. s ∼u∼ t"
(*<*)
lemma gen_uwrI: "(!!u. u∈us ==> s ∼u∼ t) ==> s ≈us≈ t"
by (simp add: gen_uwr_def)

lemma gen_uwrD: "[|s ≈us≈ t; u∈us|] ==> s ∼u∼ t"
by (simp add: gen_uwr_def)

lemma gen_uwr_empty [simp]: "s ≈{}≈ t"
by (auto simp add: gen_uwr_def)

lemma gen_uwr_insert [simp]: "s ≈insert u us≈ t <-> s ∼u∼ t ∧ s ≈us≈ t"
by (auto simp add: gen_uwr_def)
(*
lemma gen_uwr_singleton [simp]: "s ≈{u}≈ t <-> s ∼u∼ t"
by (simp)
*)
lemma gen_uwr_Union [simp]: "s ≈us ∪ vs≈ t <-> s ≈us≈ t ∧ s ≈vs≈ t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_s0: "s0 ≈us≈ s0"
by (rule gen_uwrI, rule uwr_s0)

lemma (in uwr_refl) gen_uwr_refl: "s ≈us≈ s"
by (rule gen_uwrI, rule uwr_refl)

lemma (in uwr_trans) gen_uwr_trans: "r ≈us≈ s ==> s ≈us≈ t ==> r ≈us≈ t"
by (blast intro: gen_uwrI uwr_trans dest: gen_uwrD)

lemma gen_uwr_mono: "s ≈vs≈ t ==> us ⊆ vs ==> s ≈us≈ t"
by (blast intro: gen_uwrI dest: gen_uwrD)

lemma gen_uwr_uwr: 
  "[|s ≈us≈ t; (!!u. [|s ∼u∼ t; u ∈ us|] ==> s' ∼u∼ t')|] ==> s' ≈us≈ 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 ≡ s ≈{v. v \<leadsto> u}≈ t"

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

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

lemma nest_uwrD: "[|s \<simeq>u\<simeq> t; v \<leadsto> u|] ==> s ∼v∼ 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 ==> s ∼u∼ t"
by (blast intro: policy_refl nest_uwrD)
(*>*)

lemma (in policy_trans) nesting: "[|s \<simeq>v\<simeq> t; u \<leadsto> v|] ==> s \<simeq>u\<simeq> t" 
(*<*)
by (blast intro: nest_uwrI dest: nest_uwrD policy_trans)

lemma gen_chain_uwr_ConsD: 
 "s ≈gen_chain P (a # as) u≈ t ==> 
  (w \<leadsto> v --> v ∈ gen_chain P as u --> P w a --> s ∼w∼ t) ∧ 
   s ≈gen_chain P as u≈ t"
by (auto simp add: dest: gen_uwrD)

lemma chain_uwr_ConsD: 
 "s ≈chain (a # as) u≈ t ==> (v ∈ chain as u --> s \<simeq>v\<simeq> t) ∧ s ≈chain as u≈ t"
by (unfold chain_def, 
       blast intro!: nest_uwrI dest: gen_chain_uwr_ConsD)

lemma sources_uwr_ConsD: 
  "s ≈sources (a#as) u≈ t ==> 
  (dom a \<leadsto> v --> v ∈ sources as u --> s ∼dom a∼ t) ∧ 
   s ≈sources as u≈ 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 ==> s ≈gen_chain P as u≈ t"
by (blast intro: gen_uwrI nest_uwrD gen_chain_implies_policy)
(*>*)

constdefs 
  output_consistent :: "bool"
 "output_consistent ≡ ∀u s t. s ∼u∼ t --> output u s = output u t"
(*<*)
lemma output_consistentD:
  "[|output_consistent; s ∼u∼ t|] ==> 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"
("(_\ ≅_,_,_≅\ _)"(*<*) [46,46,46,46,46] 45(*>*))
  "s ≅as,u,bs≅ t ≡ output u (run as s) = output u (run bs t)"
(*<*)
lemma obs_equivI: "[|output_consistent; run as s ∼u∼ run bs t|] ==> s ≅as,u,bs≅ 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 ≡ ∀a u s t. dom a \<leadsto> u --> s ∼dom a∼ t --> 
                               s ∼u∼ t --> step a s ∼u∼ step a t"
constdefs 
  step_respect :: "bool" --{* a consequence of @{text "local_respect"} *}
 "step_respect ≡ ∀a u s t. dom a \<notleadsto> u --> s ∼u∼ t --> step a s ∼u∼ step a t"
(*<*)
lemma weakly_step_consistentD:  
 "[|weakly_step_consistent; s ∼u∼ t; dom a \<leadsto> u; s ∼dom a∼ t|] ==> step a s ∼u∼ step a t"
by (simp add: weakly_step_consistent_def)

lemma step_respectD: 
  "[|step_respect; s ∼u∼ t; dom a \<notleadsto> u|] ==> step a s ∼u∼ 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 ≡ ∀a u s t. (∀w. P w a --> w\<leadsto>u --> s ∼w∼ t) --> 
                               s ∼u∼ t --> step a s ∼u∼ step a t"

lemma gen_weak_step_consistent_respect_action:
"[|weakly_step_consistent; step_respect|] ==> 
  gen_weak_step_consistent_respect (λ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:
"[|s ≈gen_chain P (a#as) u≈ t; gen_weak_step_consistent_respect P|] ==> 
  step a s ≈gen_chain P as u≈ 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 *}
"[|s ≈sources (a#as) u≈ t; weakly_step_consistent; step_respect|] ==> 
  step a s ≈sources as u≈ 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 ≡ ∀s'. (s, s') ∈ Run as --> 
                    (∃t'. (t, t') ∈ Run bs ∧ output u s' = output u t')"
(*<*)
lemma obs_POI: "[|output_consistent; 
∀s'. (s, s') ∈ Run as --> (∃t'. (t, t') ∈ Run bs ∧ s' ∼u∼ t')|] ==> 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 ≡ ∀a u s s' t. dom a \<leadsto> u --> 
  (s, s') ∈ Step a --> s ∼u∼ t --> (∃t'. (t, t') ∈ Step a ∧ s' ∼u∼ t')"

  Step_respect :: "bool" --{* a consequence of @{text "Local_respect"} *}
 "Step_respect ≡ ∀a u s s' t. dom a \<notleadsto> u --> 
  (s, s') ∈ Step a --> s ∼u∼ t --> (∃t'. (t, t') ∈ Step a ∧ s' ∼u∼ t')"
(*<*)

lemma Step_consistentD:  
 "[|(s, s') ∈ Step a; Step_consistent; s ∼u∼ t; dom a \<leadsto> u|] ==>
  ∃t'. (t, t') ∈ Step a ∧ s' ∼u∼ t'" 
by (simp add: Step_consistent_def)

lemma Step_respectD: 
  "[|Step_respect; (s, s') ∈ Step a; s ∼u∼ t; dom a \<notleadsto> u|] ==> 
    ∃t'. (t, t') ∈ Step a ∧ s' ∼u∼ t'" 
by (simp add: Step_respect_def)
(*>*)

lemma simple_unwinding_Step:
      "[|(s, s') ∈ Step a; s ∼u∼ t; Step_consistent; Step_respect |] ==> 
  ∃t'. (t, t') ∈ Step a ∧ s' ∼u∼ 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 ≡ ∀a us s s' t. (∃u∈us. dom a \<leadsto> u) --> s ∼dom a∼ t --> 
      (s, s') ∈ Step a --> s ≈us≈ t --> 
(∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t')"

  uni_Step_respect :: "bool"
 "uni_Step_respect ≡ ∀a us s t s'.  ¬(∃u∈us. dom a \<leadsto> u) --> (∃u. u∈us) -->
        (s, s') ∈ Step a --> s ≈us≈ t --> 
  (∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t')"
(*<*)
lemma uni_Step_consistentD:  
 "[|(s, s') ∈ Step a; uni_Step_consistent; s ≈us≈ t; ∃u∈us. dom a \<leadsto> u; 
   s ∼dom a∼ t|] ==> ∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t'"
by (unfold uni_Step_consistent_def, blast)

lemma uni_Step_respectD [rule_format]: 
  "[|uni_Step_respect; s ≈us≈ t; ¬(∃u∈us. dom a \<leadsto> u); 
    (s, s') ∈ Step a; u∈us|] ==> ∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t'" 
by (unfold uni_Step_respect_def, blast)
(*>*)

constdefs
  gen_uni_Step_consistent_respect :: "(domain => action => bool) => bool"
 "gen_uni_Step_consistent_respect P ≡ ∀a s us t s'. 
   (∀w. P w a --> (∃u∈us. w \<leadsto> u) --> s ∼w∼ t) --> (∃u. u∈us) --> 
         (s, s') ∈ Step a --> s ≈us≈ t --> 
   (∃t'. (t, t') ∈ Step a ∧ s' ≈us≈ t')"

lemma gen_chain_unwinding_Step:
      "[|(s, s') ∈ Step a; s ≈gen_chain P (a#as) u≈ t; 
        gen_uni_Step_consistent_respect P|] ==> 
  ∃t'. (t, t') ∈ Step a ∧ s' ≈gen_chain P as u≈ 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:
"[|uni_Step_consistent; uni_Step_respect|] ==> 
  gen_uni_Step_consistent_respect (λw a. w = dom a)"
apply (clarsimp simp add: gen_uni_Step_consistent_respect_def)
apply (case_tac "∃v∈us. dom a \<leadsto> v")
apply  (blast dest: uni_Step_consistentD)
apply (blast dest: uni_Step_respectD)
done
(*>*)

lemma sources_unwinding_Step:
      "[|(s, s') ∈ Step a; s ≈sources (a#as) u≈ t;
        uni_Step_consistent; uni_Step_respect|] ==> 
  ∃t'. (t, t') ∈ Step a ∧ s' ≈sources as u≈ 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: "[|(x, y) ∈ Step a; (x, z) ∈ Step a|] ==> y = z"

lemma (in Step_functional) uni_Step_consistent: 
  "Step_respect ==> Step_consistent ==> 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 ∈ us")
apply (thin_tac "s ∼x∼ t")
apply (thin_tac "s' ∼x∼ 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
(*>*)