# Re: [isabelle] Trouble selecting maximum element of locally linear relation

Hi Denis,

concerning your second question, the proof in the enclosed theory file
should do the trick.

Cheers,

Stefan

Denis Bueno schrieb:
> Hi all,
>
> In a proof I am working on, I need to formalise the statement "let x
> be the largest member of X".  There is the Max operator in Finite_Set
> which provides this, but it requires the elements in the set X to be
> ordered by a linear order.  My elements are *linearly ordered* but
> they are not ordered by a linear order.  That is, my order is locally
> linear in the context I care about, but it is not linear in general.
> Is there a way to express this fact to Isabelle so I can use the Max
> function?
>
> Second, since I couldn't figure out how to express this to Isabelle
> (if it is indeed possible), I tried to prove that there is always a
> max for my set.  Mathematically, this is achieved via a simple
> induction on the cardinality of the set X, and indeed in the
> Finite_Set library there is the induction rule
> "Finite_Set.finite_ne_induct" for an induction whose base case is a
> non-empty set, which is exactly what I want.  However, Isabelle
> rejects my attempt to perform this induction ("empty result
> sequence").
>
> Concretely, I am using a sequence-prefix ordering from the library
> LList2 [0]: x <= y if the sequence x is a prefix of y.  In my proof,
> every element of the set X is a prefix of a fixed sequence, t.  Thus,
> the elements in X are linearly ordered, since any two elements x and y
> are prefixes of t, and thus x <= y or y <= x.
>
> If you can help me, please try out the proof script, which I've
> attached: the relevant induction is for the theorem on line 152.
> Thank you.
>
> [0] http://afp.sourceforge.net/browser_info/current/HOL/Lazy-Lists-II/LList2.html
>

--
Stefan Friedrich, Consultant
method park Software AG, Kaiserstuhlstr. 3, 79312 Emmendingen, Germany
phone: +49 7641 93339-70 mailto:stefan.friedrich at methodpark.de
fax:   +49 7641 93339-69 <http://www.methodpark.de> www.methodpark.de

Vorstand: Prof. Dr. Bernd Hindel (Vorsitzender), Dr. Erich Meier,
Jochen Seemann
Aufsichtsratsvorsitzender: Klaus-Magnus Junginger
Sitz der Gesellschaft ist Erlangen
Registergericht Fürth, HRB 8609
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"

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)

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

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