Basic properties of strongly well-formed symbolic environments

This file proves basic lemmas about the strong well-formedness predicate on environments.

theorem Cedar.Thm.swf_εnv_implies_wf {εnv : SymCC.SymEnv} : εnv.StronglyWellFormed → εnv.WellFormed

theorem Cedar.Thm.swf_εnv_all_implies_swf_all {εnv : SymCC.SymEnv} {xs : List Spec.Expr} : εnv.StronglyWellFormedForAll xs → ∀ (x : Spec.Expr), x ∈ xs → εnv.StronglyWellFormedFor x

theorem Cedar.Thm.swf_εnv_all_implies_wf_all {εnv : SymCC.SymEnv} {xs : List Spec.Expr} : εnv.StronglyWellFormedForAll xs → ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x

theorem Cedar.Thm.swf_εnv_for_implies_wf_for {εnv : SymCC.SymEnv} {x : Spec.Expr} : εnv.StronglyWellFormedFor x → εnv.WellFormedFor x

theorem Cedar.Thm.swf_env_implies_wf {env : Spec.Env} : env.StronglyWellFormed → env.WellFormed

theorem Cedar.Thm.swf_env_all_implies_swf_all {env : Spec.Env} {xs : List Spec.Expr} : env.StronglyWellFormedForAll xs → ∀ (x : Spec.Expr), x ∈ xs → env.StronglyWellFormedFor x

theorem Cedar.Thm.swf_env_all_implies_wf_all {env : Spec.Env} {xs : List Spec.Expr} : env.StronglyWellFormedForAll xs → ∀ (x : Spec.Expr), x ∈ xs → env.WellFormedFor x

theorem Cedar.Thm.swf_env_for_implies_wf_for {env : Spec.Env} {x : Spec.Expr} : env.StronglyWellFormedFor x → env.WellFormedFor x

theorem Cedar.Thm.swf_εnv_for_policy_iff_swf_for_polices {εnv : SymCC.SymEnv} {p : Spec.Policy} : εnv.StronglyWellFormedForPolicy p ↔ εnv.StronglyWellFormedForPolicies [p]

theorem Cedar.Thm.swf_env_for_policy_iff_swf_for_polices {env : Spec.Env} {p : Spec.Policy} : env.StronglyWellFormedForPolicy p ↔ env.StronglyWellFormedForPolicies [p]

theorem Cedar.Thm.swf_εnv_for_policies_iff_swf_for_append {εnv : SymCC.SymEnv} {ps₁ ps₂ : Spec.Policies} : εnv.StronglyWellFormedForPolicies ps₁ ∧ εnv.StronglyWellFormedForPolicies ps₂ ↔ εnv.StronglyWellFormedForPolicies (ps₁ ++ ps₂)

theorem Cedar.Thm.swf_env_for_policies_iff_swf_for_append {env : Spec.Env} {ps₁ ps₂ : Spec.Policies} : env.StronglyWellFormedForPolicies ps₁ ∧ env.StronglyWellFormedForPolicies ps₂ ↔ env.StronglyWellFormedForPolicies (ps₁ ++ ps₂)

theorem Cedar.Thm.swf_εnv_for_policies_implies_wf_for_policies {εnv : SymCC.SymEnv} {ps : Spec.Policies} : εnv.StronglyWellFormedForPolicies ps → εnv.WellFormedForPolicies ps

theorem Cedar.Thm.swf_env_for_policies_implies_wf_for_policies {env : Spec.Env} {ps : Spec.Policies} : env.StronglyWellFormedForPolicies ps → env.WellFormedForPolicies ps