*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Tue, 13 Apr 2010 22:59:37 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk, Peter Gammie <peteg42 at gmail.com>*In-reply-to*: <4BC2BBD9.7020907@informatik.tu-muenchen.de>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi> <85BA6970-0E84-407C-8840-BD6D17BE324E@gmail.com> <4BB0BF4D.9040307@abo.fi> <310B13AA-C344-4A27-A9F4-30AE2D1182D0@gmail.com> <4BBAEDE0.6040007@abo.fi> <4BC2BBD9.7020907@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.9) Gecko/20100317 Thunderbird/3.0.4

Hi Florian, On 4/12/2010 9:21 AM, Florian Haftmann wrote:

Hi Viorel,There is still something which does not work as expected. The syntax defined in the locale cannot be used in the interpretation. Moreover, when I use facts from the locale in the interpretation they are parametrized by the instance for the function pair. On the other hand when using classes things work more as I would expect them to work.syntax is a delicate issue. Can you provide me with the whole example containing the interpretation? Then perhaps I can explain why things behave as they do.

is used for termination.

fixpoint semantics.

recursive procedure using the rule for mutually recursive procedures. However, I cannot use the notation (|- _ {| _ |} _ ) in the locale instance. Best regards, Viorel ================================================================= header {* Hoare Rule for Mutually Recursive Procedures *} theory RecursiveProcedures imports Inductive Datatype begin definition "Hoare (p::'a::complete_lattice) S q = (p \<le> S q)"; locale RecursiveProcedures = fixes pair::"'a => 'b=> ('c::wellorder)" begin definition "sup_less P (u::'c) i = SUPR {v . (pair v i) < u} (% v . P v i)"; definition

("|- (_){| _ |}(_) " [0,0,900] 900) where "|- P {| F |} Q =

theorem correctness: "mono F ==> |- P {| F |} Q ==> Hoare (P i) ((lfp F) i) (Q i)"; sorry; end; datatype Single = single; interpretation RecursiveProcedures "% (n::nat) (a :: Single) . n"; done; definition

theorem [simp]: "lfp (% S a . F (S a)) = (% a . lfp F)"; sorry theorem [simp]: "mono F ==> mono (% S a . F (S a))"; by (simp add: mono_def le_fun_def); theorem correctnesssingle: "mono F \<Longrightarrow> HoareSingleProc P F Q ==> Hoare P (lfp F) Q"; (*apply (case_tac "|- (% a . P) {| (% S a . F (S a)) |} (% a . Q)");*) apply (case_tac "HoareProc (% a . P) (% S a . F (S a)) (% a . Q)"); apply (case_tac "mono (% S a . F (S a))");

apply auto; apply (erule notE); apply (simp_all add: HoareProc_def HoareSingleProc_def); apply auto; apply (rule_tac x = "% n a . X n" in exI); apply (simp add: sup_less_def le_fun_def SUPR_def Sup_fun_def); apply (case_tac "range X = {y\<Colon>'b. EX f\<Colon>nat. y = X f}"); by auto; end;

**Follow-Ups**:**Re: [isabelle] Specification depends on extra type variables***From:*Florian Haftmann

**References**:**Re: [isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

**Re: [isabelle] Specification depends on extra type variables***From:*Florian Haftmann

- Previous by Date: [isabelle] question about locales and locale parameters
- Next by Date: Re: [isabelle] can't hack induction
- Previous by Thread: Re: [isabelle] Specification depends on extra type variables
- Next by Thread: Re: [isabelle] Specification depends on extra type variables
- Cl-isabelle-users April 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