*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Higher-order matching against schematic variables*From*: Michael Chan <mchan at inf.ed.ac.uk>*Date*: Thu, 18 Nov 2010 18:05:50 +0000*Cc*: isabelle-users at cl.cam.ac.uk, Alexander Krauss <krauss at in.tum.de>*In-reply-to*: <FD96B647-7006-48C2-82D0-D2FDB693A2FD@cam.ac.uk>*References*: <4CE52C0F.5060108@inf.ed.ac.uk> <FD96B647-7006-48C2-82D0-D2FDB693A2FD@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.11) Gecko/20101006 Thunderbird/3.1.5

On 18/11/10 16:07, Lawrence Paulson wrote:

I can't see the answer to this, but something complicated is going on when you match (?f::((?'a=>?'b)=>?'c)) ?stuff against x y where x :: nat => nat.

lemma lem: "g a = 0" sorry vs lemma lem: "(x::nat=>nat) y = 0" sorry Now, if we instead use a simpler pattern: val trm1 = term_of @{cpat "(?f::?'a=>?'b) ?stuff = ?v"}; matching it against "g a = 0" gives 4 matchers: 1. [?f::nat => nat := %a::nat. a, ?v::nat := 0::nat, ?stuff::nat := g a] 2. [?f::nat => nat := g, ?v::nat := 0::nat, ?stuff::nat := a] 3. [?f::?'a => nat := %b::?'a. g a, ?v::nat := 0::nat, ?stuff::?'a := ?stuff::?'a] 4. [?f::?'a => ?'b := g, ?v::?'b := 0::nat, ?stuff::?'a := a] But matching it against "(x::nat=>nat) y = 0", gives only 1 matcher: 1. [?f::?'a => ?'b := ?x::nat => nat, ?v::?'b := 0::nat, ?stuff::?'a := ?y::nat] which is of the same shape of the first lemma's 4th matcher.

Thanks Michael

Larry Paulson On 18 Nov 2010, at 13:37, Michael Chan wrote:Hi all, I have a question with higher-order matching against schematic variables. I can't figure out why the pattern trm1 can't be matched against lem if lem was "A x y --> x y = 0". However, if the RHS contains constants instead, e.g., "A x y --> g a = 0", a matcher is found. Since x and y have the same types of g and a respectively, how come there isn't a matcher in the former case? A difference is that x and y are schematic variables, but why can't schematic variables be matched against? Here's the code: locale A = fixes f :: "nat => nat" and a :: nat assumes ax: "f a = 0" consts g :: "nat => nat" a :: nat lemma lem: "A x y --> x y = 0" sorry ML {* val trm1 = term_of @{cpat "?P --> (?f::((?'a=>?'b)=>?'c)) ?stuff = ?v"}; val trm2 = Thm.prop_of @{thm lem}; val mtch_seq = let val init = Envir.empty 0 val ctxt = @{context} val (Const ("Trueprop",_) $ trm2) = Thm.prop_of (ProofContext.get_thm ctxt "lem") in Unify.matchers @{theory} [(trm1,trm2)] end; val seq as SOME (mtch,_) = nthseq 0 mtch_seq; pretty_env @{context} (Envir.term_env mtch); *} Thanks Michael -- Postal Address: School of Informatics, University of Edinburgh, Room 2.05, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, UK. Telephone Number: +44-131-651-3077, Fax Number: +44-131-650-6899, Email: M.Chan at ed.ac.uk Web Page: http://homepages.inf.ed.ac.uk/mchan/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

-- Postal Address: School of Informatics, University of Edinburgh, Room 2.05, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, UK. Telephone Number: +44-131-651-3077, Fax Number: +44-131-650-6899, Email: M.Chan at ed.ac.uk Web Page: http://homepages.inf.ed.ac.uk/mchan/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

**Follow-Ups**:**Re: [isabelle] Higher-order matching against schematic variables***From:*Michael Chan

**References**:**[isabelle] Higher-order matching against schematic variables***From:*Michael Chan

- Previous by Date: [isabelle] prooving protocols
- Next by Date: Re: [isabelle] Porting a tool: OuterSyntax.read disappeared
- Previous by Thread: [isabelle] Higher-order matching against schematic variables
- Next by Thread: Re: [isabelle] Higher-order matching against schematic variables
- Cl-isabelle-users November 2010 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