Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Another naive question: I'd like to define several mutually recursive
functions, eg (roughly) as is_val and is_exp in the example below.
Looking in the tutorial I only see single examples - how would this be
most nicely done? (Presumably I could make a new disjoint sum type
and work over that, but that seems ugly - though some plumbing of size
functions is going to be needed somewhere.)
ta,
Peter
theory Out = Main:
types ident = "string"
datatype
exp =
Exp_ident "ident"
| Exp_unit
| Exp_pair "exp*exp"
| Exp_fun "ident*exp"
| Exp_app "exp*exp"
| Exp_foo "exp"
and C =
Ctx_pairL "exp"
| Ctx_pairR "exp"
| Ctx_appL "exp"
| Ctx_appR "exp"
and Jop =
JO_red "exp*exp"
and judgement =
judgement_Jop "Jop"
consts is_val :: "exp => bool"
is_C :: "C => bool"
is_Jop :: "Jop => bool"
is_exp :: "exp => bool"
recdef is_val "measure (% x . size x)"
"is_val (Exp_ident ( x ) ) = (True)"
"is_val (Exp_unit) = (True)"
"is_val (Exp_pair ( exp , exp' ) ) = (((is_val exp) & (is_val exp')))"
"is_val (Exp_fun ( x , exp ) ) = (((is_exp exp)))"
"is_val (Exp_app ( exp , exp' ) ) = False"
"is_val (Exp_foo ( val ) ) = False"
recdef is_C "measure (% x . size x)"
"is_C (Ctx_pairL ( exp ) ) = (((is_exp exp)))"
"is_C (Ctx_pairR ( val ) ) = (((is_val val)))"
"is_C (Ctx_appL ( exp ) ) = (((is_exp exp)))"
"is_C (Ctx_appR ( val ) ) = (((is_val val)))"
recdef is_Jop "measure (% x . size x)"
"is_Jop (JO_red ( e , e' ) ) = (((is_exp e) & (is_exp e')))"
recdef is_exp "measure (% x . size x)"
"is_exp (Exp_ident ( x ) ) = (True)"
"is_exp (Exp_unit) = (True)"
"is_exp (Exp_pair ( exp , exp' ) ) = (((is_exp exp) & (is_exp exp')))"
"is_exp (Exp_fun ( x , exp ) ) = (((is_exp exp)))"
"is_exp (Exp_app ( exp , exp' ) ) = (((is_exp exp) & (is_exp exp')))"
"is_exp (Exp_foo ( val ) ) = (((is_val val)))"
Email Gateway (Aug 17 2022 at 14:14):From: Brian Huffman <brianh@csee.ogi.edu>
You could actually define these functions together using primrec: Since
recursive calls are only made on subterms, you don't really need the full
power of recdef.
However, using primrec is complicated by the fact that you have used product
types as arguments to your constructors. This is actually an instance of
indirect recursion, which means you would be required to additionally define
several extra constants which take the product types as arguments. If you
change your datatype definitions so that the constructors have two separate
arguments instead of a pair, then primrec should work just fine.
Email Gateway (Aug 17 2022 at 14:14):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Brian Huffman writes:
You could actually define these functions together using primrec: Since
recursive calls are only made on subterms, you don't really need the full
power of recdef.
that's true in this case, indeed.
However, using primrec is complicated by the fact that you have used product
types as arguments to your constructors. This is actually an instance of
indirect recursion, which means you would be required to additionally define
several extra constants which take the product types as arguments. If you
change your datatype definitions so that the constructors have two separate
arguments instead of a pair, then primrec should work just fine.
But that seems not to be. As far as I can tell it's impossible to
define multiple mutually-recursive functions over the same types, eg the
is_val :: "exp => bool"
is_exp :: "exp => bool"
in the example below, using either primrec or recdef. Is that really the case?
Clearly I could encode, with something like
is_val_is_exp :: "exp => (bool * bool) "
and Tom Ridge points out that I can then prove lemmas characterising
the projections of that that look like my original definition.
But I don't want to do that encoding unless I have to...
thanks,
Peter
(* here is_val and is_exp define two sub-grammars of the free exp *)
theory Out = Main:
types ident = "string"
datatype
exp =
Exp_ident "ident"
| Exp_unit
| Exp_pair "exp" "exp"
| Exp_fun "ident" "exp"
| Exp_app "exp" "exp"
| Exp_foo "exp"
consts
is_val :: "exp => bool"
is_exp :: "exp => bool"
primrec
"is_val ((Exp_ident x)) = (True)"
"is_val (Exp_unit) = (True)"
"is_val ((Exp_pair exp exp')) = (((is_val exp) & (is_val exp')))"
"is_val ((Exp_fun x exp)) = (((is_exp exp)))"
"is_val ((Exp_app exp exp')) = False"
"is_val ((Exp_foo val)) = False"
"is_exp ((Exp_ident x)) = (True)"
"is_exp (Exp_unit) = (True)"
"is_exp ((Exp_pair exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_fun x exp)) = (((is_exp exp)))"
"is_exp ((Exp_app exp exp')) = (((is_exp exp) & (is_exp exp')))"
"is_exp ((Exp_foo val)) = (((is_val val)))"
Email Gateway (Aug 17 2022 at 14:14):From: nipkow@in.tum.de
I think the only mutual recursion we currently support is for mutually
recursive datatypes. Mutual recursion in general is in the pipeline...
Below you find a higher-order encoding of mutual recursion. It avoids having
to mess around with pairs but requires its own tricks. I had never tried this
before and it was a valuable exercise.
Tobias
types ident = "string"
datatype
exp =
Exp_ident "ident"
| Exp_unit
| Exp_pair "exp" "exp"
| Exp_fun "ident" "exp"
| Exp_app "exp" "exp"
| Exp_foo "exp"
consts
is_val2 :: "(exp => bool) => exp => bool"
is_exp :: "exp => bool"
primrec
"is_val2 ise (Exp_ident x) = True"
"is_val2 ise (Exp_unit) = True"
"is_val2 ise (Exp_pair exp exp') = (is_val2 ise exp & is_val2 ise exp')"
"is_val2 ise (Exp_fun x exp) = ise exp"
"is_val2 ise (Exp_app exp exp') = False"
"is_val2 ise (Exp_foo val) = False"
recdef is_exp "measure size"
"is_exp (Exp_ident x) = True"
"is_exp (Exp_unit) = True"
"is_exp (Exp_pair exp exp') = (is_exp exp & is_exp exp')"
"is_exp (Exp_fun x exp) = is_exp exp"
"is_exp (Exp_app exp exp') = (is_exp exp & is_exp exp')"
"is_exp (Exp_foo val) = is_val2 is_exp val"
(* The real thing: *)
constdefs is_val :: "exp => bool"
"is_val == is_val2 is_exp"
(* Deriving the real eqns: *)
lemma [simp]:
"is_val (Exp_ident x) = True"
"is_val (Exp_unit) = True"
"is_val (Exp_pair exp exp') = (is_val exp & is_val exp')"
"is_val (Exp_fun x exp) = is_exp exp"
"is_val (Exp_app exp exp') = False"
"is_val (Exp_foo val) = False"
by(simp_all add:is_val_def)
(* A complication: the final is_exp rule is more complicated than one
may naively expect. *)
thm is_exp.simps(6)
lemma is_val2_cong:
"(!!e'. size e' < size e ==> f e' = g e') ==> is_val2 f e = is_val2 g e"
by (induct e) simp_all
lemma is_exp_foo[simp]: "is_exp (Exp_foo e) = is_val e"
by(simp add:is_val_def measure_def inv_image_def is_val2_cong)
declare is_exp.simps(6)[simp del]
Email Gateway (Aug 17 2022 at 14:15):From: nipkow@in.tum.de
I think the only mutual recursion we currently support is for mutually
recursive datatypes. Mutual recursion in general is in the pipeline...
Below you find a higher-order encoding of mutual recursion. It avoids having
to mess around with pairs but requires its own tricks. I had never tried this
before and it was a valuable exercise.
Tobias
types ident = "string"
datatype
exp =
Exp_ident "ident"
| Exp_unit
| Exp_pair "exp" "exp"
| Exp_fun "ident" "exp"
| Exp_app "exp" "exp"
| Exp_foo "exp"
consts
is_val2 :: "(exp => bool) => exp => bool"
is_exp :: "exp => bool"
primrec
"is_val2 ise (Exp_ident x) = True"
"is_val2 ise (Exp_unit) = True"
"is_val2 ise (Exp_pair exp exp') = (is_val2 ise exp & is_val2 ise exp')"
"is_val2 ise (Exp_fun x exp) = ise exp"
"is_val2 ise (Exp_app exp exp') = False"
"is_val2 ise (Exp_foo val) = False"
recdef is_exp "measure size"
"is_exp (Exp_ident x) = True"
"is_exp (Exp_unit) = True"
"is_exp (Exp_pair exp exp') = (is_exp exp & is_exp exp')"
"is_exp (Exp_fun x exp) = is_exp exp"
"is_exp (Exp_app exp exp') = (is_exp exp & is_exp exp')"
"is_exp (Exp_foo val) = is_val2 is_exp val"
(* The real thing: *)
constdefs is_val :: "exp => bool"
"is_val == is_val2 is_exp"
(* Deriving the real eqns: *)
lemma [simp]:
"is_val (Exp_ident x) = True"
"is_val (Exp_unit) = True"
"is_val (Exp_pair exp exp') = (is_val exp & is_val exp')"
"is_val (Exp_fun x exp) = is_exp exp"
"is_val (Exp_app exp exp') = False"
"is_val (Exp_foo val) = False"
by(simp_all add:is_val_def)
(* A complication: the final is_exp rule is more complicated than one
may naively expect. *)
thm is_exp.simps(6)
lemma is_val2_cong:
"(!!e'. size e' < size e ==> f e' = g e') ==> is_val2 f e = is_val2 g e"
by (induct e) simp_all
lemma is_exp_foo[simp]: "is_exp (Exp_foo e) = is_val e"
by(simp add:is_val_def measure_def inv_image_def is_val2_cong)
declare is_exp.simps(6)[simp del]
Last updated: Nov 21 2024 at 12:39 UTC