*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Trouble selecting maximum element of locally linear relation*From*: Stefan Friedrich <stefan.friedrich at methodpark.de>*Date*: Wed, 19 Mar 2008 15:22:19 +0100*Cc*: Denis Bueno <dbueno at gmail.com>*In-reply-to*: <6dbd4d000803180931k8f9dd61k4af0010e7b5e1603@mail.gmail.com>*Organization*: method park Software AG*References*: <6dbd4d000803180931k8f9dd61k4af0010e7b5e1603@mail.gmail.com>*Reply-to*: Stefan.Friedrich at methodpark.de*User-agent*: Thunderbird 2.0.0.12 (X11/20080227)

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" 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

**References**:**[isabelle] Trouble selecting maximum element of locally linear relation***From:*Denis Bueno

- Previous by Date: [isabelle] IJCAR's ESHOL Workshop - CFP
- Next by Date: [isabelle] term abbreviations?
- Previous by Thread: [isabelle] Trouble selecting maximum element of locally linear relation
- Next by Thread: Re: [isabelle] Trouble selecting maximum element of locally linear relation
- Cl-isabelle-users March 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list