Email Gateway (Aug 18 2022 at 14:49): Email Gateway (Aug 18 2022 at 14:49):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,
Thank you for your answer. Almost for sure I would have an inconsistency
similar
to what you showed if I would use the axiomatic approach. I have used
the locale
to introduce the extra types. Moreover, my definition depends also on a
constant
(pair) and I fixed that in the locale too.
This solution is satisfactory, but reading your example, I realized that
what I would
need is an existential quantification on the extra type:
axioms f_def2: "f (a::'a) = (EX 'b::type . (EX (g::'b => 'a). inj g))"
Like this there is no danger of inconsistencies. Is there something in
Isabelle which
would allow something similar to this?
Viorel
Email Gateway (Aug 18 2022 at 14:49):From: Peter Gammie <peteg42@gmail.com>
Viorel,
I am bit confused by:
(pair a b) = (b a)
-- b does not have a function type.
If you want 'a and 'b to be fixed-but-arbitrary, define another locale, e.g.:
locale AB =
fixes a :: "'a :: order"
fixes b :: "'b :: order"
and use sublocale to interpret the locales containing the lemmas of interest. There was a recent thread with subject "Locale Import" initiated by Andreas Lochbihler that clearly presents the approach. Intuitively you need to define every context (set of assumptions) you want the lemmas to work in as a locale.
Note that you have to ensure that the order on 'a * 'b is the lexicographic one by examining the class instances -- you only get to define one instance per type.
Hope this helps.
cheers
peter
Email Gateway (Aug 18 2022 at 14:59):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I am trying to define a constant which depends on an extra type
variable. A simplified version of the definition looks like:
definition
"f a = (?g . !u . g u = a)";
I have found an answer to a similar question in the Isabelle archive
which suggests having a dummy parameter for f which gives the
missing type:
definition
f :: "'a => ('b itself) => bool" where
"f a x = (?g . !u . g (u::'b) = a)";
However like this I have to use x as parameter for f everywhere.
Moreover, I am defining Hoare triples for some kind of programs,
and I want to use the syntax "|- _ {| _ |} _", but with this approach
I need a place for the extra dummy parameter also.
The fact is that the type 'b must be a type variable. I cannot
instantiate it
at this point.
Another approach which seem to work is by defining an uninterpreted
constant, and give its concrete definition using an axiom:
consts
f :: "'a => bool";
axioms f_def:
"f a = (? g . !u . g u = a)";
Is the axiomatic solution unsound?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 14:59):From: Brian Huffman <brianh@cs.pdx.edu>
On Fri, Mar 26, 2010 at 5:49 AM, Viorel Preoteasa
<viorel.preoteasa@abo.fi> wrote:
Hello,
I am trying to define a constant which depends on an extra type
variable.
...
Another approach which seem to work is by defining an uninterpreted
constant, and give its concrete definition using an axiom:consts
f :: "'a => bool";axioms f_def:
"f a = (? g . !u . g u = a)";Is the axiomatic solution unsound?
In this particular case, axiom f_def is sound. But this style of axiom
will be unsound in all but the most trivial of instances.
For clarity, here's a type-annotated version of your axiom:
axioms f_def: "f (a::'a) = (EX (g::'b => 'a) . ALL (u::'a). g u = a)"
When you write an axiom with a free type variable (or a free term
variable, for that matter) it like declaring an infinite collection of
axioms all at once, one for each possible instantiation of the free
variables.
Your axiom f_def happens to be sound, but only because the RHS is
always true no matter what 'b is. (Constant functions exist for every
type 'b.) So you might as well have written
axioms f_def: "f (a::'a) = True"
But I'd guess that your real example is not so trivial. Here's a
variation where the value of the RHS actually does depend on which
type 'b is instantiated to, since injective functions exist between
some pairs of types, but not all.
axioms f_def2: "f (a::'a) = (EX (g::'b => 'a). inj g)"
Let's look at two different type instances of axiom f_def2:
"f (a::bool) = (EX (g::bool => bool). inj g)"
"f (a::bool) = (EX (g::nat => bool). inj g)"
The first one is equivalent to "f (a::bool) = True", and the second is
equivalent to "f (a:bool) = False". This is clearly unsound. The
general lesson here is that declaring axioms is dangerous, and you
should avoid doing so whenever possible.
If you really want to avoid explicitly passing around an extra dummy
parameter, here's what I would recommend: Declare a locale that fixes
the dummy type parameter of type "'b itself", and define your
constants (which may refer to the locally-fixed type 'b) inside the
locale.
Email Gateway (Aug 18 2022 at 15:00):From: Peter Gammie <peteg42@gmail.com>
Viorel,
Can I suggest you look into locales?
locale L =
fixes unused_x :: "'b"
begin
definition
"f a = (?g. !u. g (u::'b) = a)"
end
(untested, but I can expand on this if you think it might be a profitable approach.)
You can later instantiate 'b with a sublocale or interpretation command.
cheers
peter
Email Gateway (Aug 18 2022 at 15:00):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Peter,
Thank you for our answer. I could get the definitions using locales.
However my
case is more involved compared to the dummy example I presented in my
earlier message. The locale depends actually on three type parameters:
locale HoareRule =
fixes pair:: "'a => 'b => ('c::order)"
begin
definition
"SUP_L_P X u i = SUPR {v . pair v i < u} (%v . X v i)";
definition
Hoare_dgr :: "('b => ('u::complete_lattice)) => ('b × 'b => 'u => 'u)
=> ('b => 'u) => bool" ( "|- (_){| _ |}(_) " [900,0,900] 900) where
"|- P {| D |} Q = (? X . (! w i j . X w i <= D(i, j) (SUP_L_P X
(pair w i) j)) /\ P = SUP X /\ Q = (SUP X))"
I have succeeded to develop this general theory, but I have problem
instantiating it
for concrete types. I need it instantiated for 'c = 'a * 'b where 'a and
'b are orders
and the order on 'c is the lexicographic order. (pair a b) = (b a). I
have built the
lexicographic order on pairs, but I don't know how to instantiate this
locale.
All examples I found with locales had only one type parameter.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 15:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
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.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:05):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hi Florian,
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;
Email Gateway (Aug 18 2022 at 15:05):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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)"
begindefinition
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
signature.asc
Email Gateway (Aug 18 2022 at 15:07):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Peter,
Thank you again for your answer. I have finally figured out how to interpret
the locale. What I needed was every easy:
locale HoareRule =
fixes pair::"'a => 'b => ('c::well_founded_transitive)"
begin
...
end
interpretation HoareRule "% (a::'a::well_founded_transitive)
(b::('b::well_founded_transitive)) . (b, a)";
done;
The tutorial on locales is a bit misleading. There an arbitrary order is
interpreted as order
on integers, and the name int is used for this interpretation. I thought
of this name as being
the instantiation of the locale for the int type, when actually this was
just a name for the interpretation.
The fact that the type name is used when interpreting a class has
contributed to this confusion.
Because of this misinterpretation I could not figure out how to give
interpretation to something
which depends on more than one type.
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.
Best regards,
Viorel
Peter Gammie wrote:
Last updated: Nov 21 2024 at 12:39 UTC