Re: [isabelle] incompatible operand type



Hello Martin,

On 10-28, M A wrote:
> when design a new unknown function max, it return incompatible operand type error, I tried add bracket, still got error, where is wrong?
> lemma max_app [simp]: "((max xs) @ (max ys)) @ (max zs) = (max xs) @ ((max ys) @ (max zs))"
>  
> Type unification failed: Clash of types "_ ⇒ _" and "_ list"
> Type error in application: incompatible operand type
> Operator:  op @ :: ??'a list ⇒ ??'a list ⇒ ??'a list
> Operand:   max xs :: ??'b ⇒ ??'b

If you Ctrl-hover[*] over "max" you see it is *already* defined as
constant "Orderings.ord_class.max".
[*] Click button on right side "Documentation", 
see section "Prover output" in "jedit: Isabelle/jEdit" entry 
under "Reference Manuals" or search for jedit.pdf.

If you Ctrl-hover+click over "max" you see its definition as
definition (in ord) max :: "'a ⇒ 'a ⇒ 'a" where
  "max a b = (if a ≤ b then b else a)"

The operator "@" expects both arguments to be of type 'a list, 
whereas "max xs" is seen as function of "'a => 'a".
Hence the type unification error. 

Change "max" to a term not yet defined, 
e.g. "mymax" and the type unification error will disappear.
The proof script below will fail, but you could prove "by auto".

> lemma max_app [simp]: "(max xs @ max ys) @ max zs = max xs @ (max ys @ max zs)"
> apply(induct_tac xs)
> apply(auto)
> done

-- 
Holger

===========================================================================
CALL FOR PAPERS International Workshop on MILS: Architecture and Assurance 
for Secure Systems Amsterdam, 20.01.2015 (Paper submission: 20 Nov 2014)
http://mils-workshop.euromils.eu/ (short papers also welcome)
===========================================================================




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