Re: [isabelle] Specification depends on extra type variables



Hi Viorel,

> theory RecursiveProcedures
> imports Inductive Datatype

remark: it is not recommend to import theories beneath Main for
applications.  Just stick with Main.

> begin

> locale RecursiveProcedures =
>   fixes pair::"'a => 'b=> ('c::wellorder)"
>   begin
> 
>   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)))";
> 
> end;
> 
> datatype Single = single;
> 
> interpretation RecursiveProcedures "% (n::nat) (a :: Single) . n";
> done;

Contrary to classes, definitions relative to locales are not considered
specially for interpretation.  Only an *input* abbreviation is
generated.  To restore the syntax, isse something like

abbreviation HoareProc2 ("|- (_){| _ |}(_) " [0,0,900] 900) where
"HoareProc2 ≡ RecursiveProcedures.HoareProc (% (n::nat) (a :: Single) . n)"

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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