Re: [isabelle] Knaster-Tarski Lemma




Am 30/11/2013 14:26, schrieb Alfio Martini:
> Dear Users,
> 
>  I solved the problem using the notation facility. But I am not sure what
> this was necessary since
> this syntax seems to be available in the theory Complete_Lattice. It does
> not seem to be exported
> though.

It is hidden (no_notation) in Main.
You can get it back by importing Library/Lattice_Syntax.

Tobias

> notation
>   less_eq (infix "⊑" 50) and
>   Inf  ("⨅_" [900] 900)
> 
> lemma  Knaster_Tarski:
> fixes f::"'a::complete_lattice  ⇒ 'a"
> assumes mono:"⋀ x y. x ⊑ y ⟹ f x ⊑ f y"
> shows "f( ⨅ {x. f(x) ≤ x}) = ⨅ {x. f(x) ≤ x}" (is "f ?k = ?k")
>   proof -
>      have "f ?k ≤ ?k"  (is " _ ≤ Inf ?P")
>      proof (rule Inf_greatest)
>        fix x0 assume "x0 ∈ ?P"
>        then have "?k ⊑ x0" by (rule Inf_lower)
>        from this and  mono have "f(?k) ⊑ f(x0)" by simp
>        from `x0 ∈ ?P` have "f(x0) ⊑ x0" by simp
>        from `f(?k) ⊑ f(x0)` and this show "f(?k) ⊑ x0" by simp
>      qed
>      also have "?k ⊑ f(?k)"
>        proof (rule Inf_lower)
>          from mono and `f(?k) ≤ ?k` have "f(f ?k) ⊑ f(?k)" by simp
>          then show "f ?k ∈ ?P" by simp
>        qed
>      finally show "f ?k = ?k" by this
>   qed
> 
> Best!
> 
> 
> On Fri, Nov 29, 2013 at 9:21 PM, Alfio Martini <alfio.martini at acm.org>wrote:
> 
>> Dear Isabelle Users,
>>
>> I typed a slightly different version of Makarius´s proof of Knaster-Tarski
>> lemma
>> according to his Orsay´s slides. Everything works fine but I
>> have to use "Inf" instead of "\<Sqinter>" or "INF". Otherwise I get the
>> error message "inner lexical error. Failed to parse proposition".
>> Probably something related to a wrong use of this type class.
>>
>> lemma  Knaster_Tarski:
>> fixes f::"'a::complete_lattice⇒ 'a"
>> assumes mono:"⋀ x y. x ≤ y ⟹ f x ≤ f y"
>> shows "f( Inf {x. f(x) ≤ x}) = Inf {x. f(x) ≤ x}" (is "f ?k = ?k")
>>   proof -
>>      have "f ?k ≤ ?k"  (is " _ ≤ Inf ?P")
>>      proof (rule Inf_greatest)
>>        fix x0 assume "x0 ∈ ?P"
>>        then have "?k ≤ x0" by (rule Inf_lower)
>>        from this and  mono have "f(?k) ≤ f(x0)" by simp
>>        from `x0 ∈ ?P` have "f(x0) ≤ x0" by simp
>>        from `f(?k) ≤ f(x0)` and this show "f(?k) ≤ x0" by simp
>>      qed
>>      also have "?k ≤ f(?k)"
>>        proof (rule Inf_lower)
>>          from mono and `f(?k) ≤ ?k` have "f(f ?k) ≤ f(?k)" by simp
>>          then show "f ?k ∈ ?P" by simp
>>        qed
>>      finally show "f ?k = ?k" by this
>>   qed
>>
>>
>> Thanks for any help on this (thy file attached)
>>
>> --
>> Alfio Ricardo Martini
>> PhD in Computer Science (TU Berlin)
>> www.inf.pucrs.br/alfio
>> Lattes:  http://lattes.cnpq.br/4016080665372277
>> Associate Professor at Faculty of Informatics (PUCRS)
>> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
>> 90619-900 -Porto Alegre - RS - Brasil
>>
> 
> 
> 




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