# Re: [isabelle] Specification depends on extra type variables

```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.
```
I have a a theory which is developed in few files. However I have created a smaller example which contains many of the Isabelle features I am using. I have listed the file at the end of the email.
```
```
There I have a definition for correctness of a collection of mutually recursive procedures. This definition has associated the notation |- P {| F |} Q where P, Q are families of predicates (one for each procedure) and F defines the mutually recursive procedures. This rule is defined in the context of a locale which fixes 'b the indexes of procedures, and 'a an arbitrary type. pair applied to an index and an element from 'a ranges over a well founded set, and this set
```is used for termination.

```
I have a correctness theorem which states that the rule is correct with respect to the least
```fixpoint semantics.

```
Next I instantiate the locale for a single procedure, and I prove the rule for a single
```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
```
HoareProc:: "('b => ('d::complete_lattice)) => (('b => ('e => 'd)) => ('b => ('e => 'd))) => ('b => 'e) => bool"
```   ("|- (_){| _ |}(_) " [0,0,900] 900) where
"|- P {| F |} Q =
```
(EX X . P \<le> SUPR UNIV X & (ALL S v i. (ALL j . Hoare (sup_less X (pair v i) j) (S j) (Q j)) --> Hoare (X v i) (F S i) (Q i)))";
```
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
```
"HoareSingleProc P F Q = (EX X . P <= SUPR UNIV X & (ALL S (n::nat) . Hoare (SUPR {k . k < n} X) S Q --> Hoare (X n) (F S) Q))";
```
theorem [simp]:
"lfp (% S a . F (S a)) = (% a . lfp F)";
sorry

theorem [simp]:
"mono F ==> mono (% S a . F (S a))";

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 (drule_tac P="% (a::Single) . P" and F="(% S a . F (S a))" and Q = "% (a::Single) . Q" in correctness);
```    apply auto;
apply (erule notE);
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;

```

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