theory Hyper
imports Main LList2
begin

section{*Preliminaries*}

text{* An abstract notion of a state. *}
typedecl state

text{* Traces are sequences of states. *}
types trace = "state llist"

text{* We reason about this abstract set of states. *}
consts States :: "state set"       ("\<Sigma>")

(* States is non-empty.  How to express? *)

section{*Definitions*}

constdefs
  phi_fin :: "trace set"
  "phi_fin == fpslsts States"
  phi_inf :: "trace set"
  "phi_inf == inflsts States"
  phi :: "trace set"
  "phi == phi_fin Un phi_inf"

  (* set of infinite traces *)
types property = "trace set"
constdefs
  Prop :: "property set"
  "Prop == Pow phi_inf"

types hyperproperty = "property set"
constdefs
  HP :: "hyperproperty set"
  "HP == Pow Prop"

consts
  property_satisfies :: "trace set => property => bool" ("(_ |= _)" [80,80] 80)
  hyperproperty_satisfies :: "trace set => hyperproperty => bool" ("(_ |= _)" [80,80] 80)


defs (overloaded)
property_satisfies_def:      "ts |= p == ts <= p"
hyperproperty_satisfies_def: "ts |= h == ts : h"

constdefs
  property_lift :: "property => hyperproperty" ("[[ _ ]]" 80)
  "property_lift p == Pow p"

  (* Figure out precedence of <=, or alternate way to declare. *)
consts
  trace_set_prefix :: "trace set => trace set => bool" (infix "<|" 80)

defs
  trace_set_prefix_def: "T <| T' == ALL t. t : T --> (EX t'. t' : T' & t <= t')"


constdefs
  Obs :: "trace set set"
  "Obs == {ts. ts <= phi_fin & finite ts}"

constdefs
  sp :: "property => bool"
  "sp P == ALL t. t : phi_inf & t ~: P -->
            (EX m. m : phi_fin & m <= t &
              (ALL t'. t' : phi_inf & m <= t' --> t' ~: P))"
  SP :: "property set"
  "SP == {P. sp P}"

  false_p :: "property"
  "false_p == {}"

constdefs
  shp :: "hyperproperty => bool"
  "shp H == ALL T. T : Prop & T ~: H -->
              (EX M. M : Obs & M <| T &
                (ALL T'. T':Prop & M <| T' --> T'~:H))"
  SHP :: "hyperproperty set"
  "SHP == {hp. shp hp}"

  false_hp :: "hyperproperty"
  "false_hp == [[ false_p ]]"

constdefs
  lp :: "property => bool"
  "lp L == ALL t : phi_fin. (EX t' : phi_inf. t <= t' & t' : L)"
  LP :: "property set"
  "LP == {P. lp P}"
  lhp :: "hyperproperty => bool"
  "lhp H == ALL T : Obs. (EX T' : Prop. T <| T' & T' : H)"
  LHP :: "hyperproperty set"
  "LHP == {hp . lhp hp}"



theorem proposition_1_oif:
  assumes S_Prop: "S : Prop"
  and     S_SP:   "S : SP"
  shows           "[[S]] : SHP"
proof -
  {
    fix T :: property
    assume T_st: "T : Prop" "T ~: [[S]]"
    from `T ~: [[S]]` have "~(T <= S)" by (simp add: property_lift_def)
    then obtain t where t_st: "t : T" "t ~: S" by blast

    have "EX m. m:phi_fin & m <= t & (ALL t'. t':phi_inf & m <= t' --> t'~:S)"
    proof -
      from t_st and T_st have t_phi_inf: "t:phi_inf"
        unfolding Prop_def by blast
      with S_Prop and S_SP and T_st and t_st
      show ?thesis unfolding SP_def Prop_def sp_def by blast
    qed
    then obtain m where m_st: "m:phi_fin" "m <= t" "ALL t'. t':phi_inf & m <= t' --> t'~:S"
      by blast

    let ?M = "{m}"
    from m_st and t_st have M_prf_T: "?M <| T"
      unfolding trace_set_prefix_def by blast
    with m_st and t_st have M_Obs: "?M : Obs"
      unfolding Obs_def by blast

    {
      fix T' :: property
      assume T'_st: "T' : Prop" "?M <| T'"

      then have "EX t':T'. m <= t'"
        by (simp only: trace_set_prefix_def) blast
      then obtain t' where t'_st: "t':T'" "m <= t'" ..
      with m_st and T'_st have t'_out_S: "t' ~: S"
        unfolding Prop_def by blast
      from T'_st and S_Prop and S_SP and t'_st and t'_out_S
      have "T' ~: [[S]]" unfolding property_lift_def by blast
    }
    hence "ALL T'. T' : Prop & ?M <| T' --> T' ~: [[ S ]]" by blast

    with m_st and M_prf_T and M_Obs
    have "EX M. M:Obs & M <| T & (ALL T'. T' : Prop & M <| T' --> T' ~: [[S]])"
      by blast
  }
  thus ?thesis unfolding SHP_def shp_def by blast
qed

    (* Longest is my analogue to Finite_Set.Max *)
definition
  Longest :: "'a llist set => 'a llist"
where
  "Longest = fold1 max"

theorem prefix_set_has_max:
  fixes t::"'a llist"
  assumes X_prefix_t:  "ALL x : X. x <= t"
  and     X_non_empty: "X ~= {}"
  and     X_fin:       "finite X"
  shows "EX m : X. (ALL x : X. x <= m)"
  using  X_fin  X_non_empty X_prefix_t
proof(induct X rule: Finite_Set.finite_ne_induct)
  fix x::"'a llist" show "\<exists>m\<in>{x}. \<forall>x\<in>{x}. x \<le> m" by blast
next fix x::"'a llist" and F::"'a llist set"
  assume 
    R: "\<forall>x\<in>F. x \<le> t \<Longrightarrow> \<exists>m\<in>F. \<forall>x\<in>F. x \<le> m" and
    t_upper_bound: "\<forall>x\<in>insert x F. x \<le> t"
  then obtain m where
    m_in_F: "m\<in>F" and
    m_le_t: "m \<le> t" and
    x_le_t: "x \<le> t" and
    m_max_F: "\<forall>x\<in>F. x \<le> m" using R
    by (auto dest: R)
  from m_le_t x_le_t have 
    "m \<le> x \<or> x \<le> m" by (rule pref_locally_linear)
  thus "\<exists>m\<in>insert x F. \<forall>x\<in>insert x F. x \<le> m"
  proof
    assume "m \<le> x" with m_max_F
    have  "\<forall> xa \<in> insert x F. xa \<le> x"
      by auto
    thus ?thesis by blast
  next assume "x \<le> m" with m_max_F
    have "\<forall> xa \<in> insert x F. xa \<le> m" by auto
    thus ?thesis using m_in_F by blast 
  qed
qed

    
(* proof- *)
(*   { fix a assume a_st: "a:X" *)
(*     fix b assume b_st: "b:X" *)
(*     with a_st and X_prefix_t have a_lt_t: "a <= t" by blast *)
(*     from a_st and b_st and X_prefix_t have b_lt_t: "b <= t" by blast *)
(*     with a_lt_t have "a <= b | b <= a" by (rule pref_locally_linear) } *)
(*   hence X_linord: "[| a2 : X; b2 : X |] ==> a2 <= b2 | b2 <= a2" by blast *)
(*   show ?thesis *)
(*   proof (rule ccontr) *)
(*     assume "~(EX y:X. (ALL x:X. x <= y))" *)
(*     hence "ALL y:X. (EX x:X. y <= x)" by blast *)
(*     with X_fin have False by blast *)
(*     { fix x assume x_st: "x:X" *)
(*       with nc obtain xsup where "x <= xsup" by blast *)
(*     } *)
  


theorem proposition_1_if:
  assumes S_Prop:     "S : Prop"
  and     lift_S_shp: "[[S]] : SHP"
  shows               "S : SP"
proof -
  {                             (* show that t has finite bad thing m. *)
    fix t
    assume t_st: "t ~: S" "{t} : Prop"
    then have t_out_lift_S: "{t} ~: [[S]]" by (simp add: property_lift_def)
    
    with t_st and S_Prop and lift_S_shp
    have "EX M. M:Obs & M <| {t} & (ALL T'. T' : Prop & M <| T' --> T' ~: [[S]])"
      unfolding SHP_def shp_def by blast
    then obtain M where M_st: "M : Obs" "M <| {t}" "ALL T'. T' : Prop & M <| T' --> T' ~: [[S]]"
       by blast

    obtain m_star where m_star_st: "m_star : phi_fin" "m_star : M" "m_star <= t" "ALL m : M. m <= m_star"
      sorry

    {                           (* show that any t' ~: S *)
      fix t'
      assume t'_st: "{t'} : Prop" "m_star <= t'"
      let ?T' = "{t'}"
      from M_st and m_star_st and t'_st have "M <| ?T'"
        proof -
          {
            fix m
            assume "m : M"
            with m_star_st have "m <= m_star" by blast
            with t'_st have "m <= t'" using llist_le_trans by blast
          }
          thus "M <| ?T'" unfolding trace_set_prefix_def by blast
        qed

      with M_st and t'_st have "?T' ~: [[S]]" by blast
      hence "t' ~: S" unfolding property_lift_def by blast
    }

    with m_star_st have "(EX m. m : phi_fin & m <= t & (ALL t'. t' : phi_inf & m <= t' --> t' ~: S))"
      unfolding Prop_def
      by blast
  }
    thus ?thesis
      unfolding SP_def sp_def Prop_def by blast
qed

theorem proposition_2_oif:
  assumes L_Prop: "L : Prop"
  and     L_LP:   "L : LP"
  shows           "[[L]] : LHP"
proof -
{
  fix M assume M_st: "M : Obs"
  {
    fix m assume m_st: "m : M"
    have "EX t. m <= t & t : L" 
    proof -
      from m_st and M_st have "m : phi_fin"
        unfolding Obs_def by blast
      with L_Prop and L_LP and m_st show ?thesis
        unfolding LP_def
        unfolding lp_def
        unfolding Prop_def by blast
    qed
  }
  hence M_more: "ALL m : M. (EX t. m <= t & t : L)" by blast
  obtain T where
    T_st: "T = {t_m. m : M & t_m >= m & t_m : L}" (* same as paper? *)
    by blast
  hence "T <= L" by blast
  hence T_in_lift: "T : [[L]]" unfolding property_lift_def by blast
  with T_st and M_more have M_pfx_T: "M <| T"
    unfolding trace_set_prefix_def sorry
  have "T : Prop" sorry
  with T_st and T_in_lift and L_Prop
    have "EX T. T : Prop & M <| T & T : [[L]]" by blast
}
thus "[[L]] : LHP" unfolding LHP_def unfolding lhp_def by blast