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))";
    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 (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 (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;








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