*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Basic help with class and instantiation*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Thu, 16 Aug 2012 10:23:45 +0200*Organization*: Ada @ Home*References*: <op.wiz568nrule2fv@douda-yannick>*User-agent*: Opera Mail/12.01 (Linux)

declare [[show_types]] declare [[show_consts]] declare [[show_sorts]] … before the Instantiation

proof (state): step 1 goal (1 subgoal): 1. cls1_f (cls1_g (0∷nat)) = cls1_g (0∷nat) constants: TYPE(int) :: int itself cls1_class :: int itself ⇒ prop prop :: prop ⇒ prop 0∷nat :: nat cls1_g :: nat ⇒ int cls1_f :: int ⇒ int op = :: int ⇒ int ⇒ bool Trueprop :: bool ⇒ prop op ⟹ :: prop ⇒ prop ⇒ prop Types seems correctly applied/inferred. I attempted to replace then show "(cls1_f (cls1_g 0)) = (cls1_g 0)" with then show "(cls1_f (cls1_g (0::nat))) = (cls1_g (0::nat))" … but this solved nothing.

Hi all,I must miss something obvious, I can't get a simple sample classinstatiation working, and that's many hours I try to guess, but failed,thus this message.Here is the sample: class cls1 = fixes cls1_x :: "'a" and cls1_f :: "'a ⇒ 'a" and cls1_g :: "nat ⇒ 'a" assumes cls1_fg_prop: "(cls1_f (cls1_g 0)) = (cls1_g 0)" fun f :: "int ⇒ int" where "f i = i" fun g :: "nat ⇒ int" where "g n = (int n)" instantiation int :: cls1 begin definition df: "cls1_f n = f n" definition dg: "cls1_g n = g n" instance proof have "cls1_f 0 = f 0" unfolding df by simp -- #1 have "cls1_g 0 = g 0" unfolding dg by simp -- #2 have "f (g 0) = g 0" by simp -- #3 then show "cls1_f (cls1_g 0) = cls1_g 0" -- #4 unfolding df and dg by simp qed endCls1 is just for testing, it does not pretend to be useful in any way. Fand g, are supposed to play the role of cls1_f and cls1_g, respectively.In the instantiation, putting the cursor on Show, which is underlined inred, Isabelle insist on complaining:Local statement will fail to refine any pending goal Failed attempt to solve goal by exported rule: cls1_f (cls1_g 0) = cls1_g 0 However, putting the cursor right after Instance Proof, Isabelle says: proof (state): step 1 goal (1 subgoal): 1. cls1_f (cls1_g 0) = cls1_g 0 … which is exactly what's in the expression to be shown.Line #1 and #2 are for testing, after this failure, and both are OK.Hovering the cursor above cls1_f and cls1_g in line #1 and #2, says theyare cls1_class.cls1_f and cls1_class.cls1_g, which makes Isabelle'scomplains even less clear to me.Line #3 is OK too. So what's wrong? Must be obvious, but honestly, I completely miss it.P.S. By the way, what's the name of the default proof method Isabelleuses in Instance Proof? Does not seems to be unfold_classes (as there isan unfold_locales method) or any similar names I've tested.

-- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Follow-Ups**:**Re: [isabelle] Basic help with class and instantiation***From:*Florian Haftmann

**References**:**[isabelle] Basic help with class and instantiation***From:*Yannick Duchêne (Hibou57)

- Previous by Date: [isabelle] Last CfP: Special Issue "Theorem-Prover based Systems for Education"
- Next by Date: Re: [isabelle] Basic help with class and instantiation
- Previous by Thread: Re: [isabelle] Basic help with class and instantiation
- Next by Thread: Re: [isabelle] Basic help with class and instantiation
- Cl-isabelle-users August 2012 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