Email Gateway (Aug 22 2022 at 14:59): Email Gateway (Aug 22 2022 at 14:59):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I attempted to do as shown below (also see attached).
I tried to follow the "Tutorial on Functions" to prove something
about the mutually recursive definition, but I am thwarted by:
proof (prove)
goal (1 subgoal):
1. (⋀b. P a b ⟹ Q a b) &&& (R a ⟹ S a)
Ill-typed instantiation:
a :: 'b
Can some kind soul explain what is happening here? Thanks.
BTW, I deleted a few irrelevant clauses from the "term" datatype for the purposes
of this example and the processing time for the "fun" definition dropped
from about 9 minutes for the original to less than 20 seconds on the excerpt
shown here.
- Gene Stark
theory Barf
imports Main
begin
datatype (discs_sels) 't "term" =
Prim 't
| Unit
| Tensor "'t term * 't term"
| Comp "'t term * 't term"
| Lunit "'t term"
| Runit "'t term"
| Assoc "'t term * 't term * 't term"
fun normalize :: "'t term ⇒ 't term"
where "normalize t = t"
fun redTensor
and red
where "redTensor (Unit, Unit) = Lunit Unit"
| "redTensor (Prim f, Unit) = Runit (Prim f)"
| "redTensor (Tensor (a, b), Unit) = Comp (redTensor (a, b), Runit (Tensor (a, b)))"
| "redTensor (Unit, a) = Lunit a"
| "redTensor (Prim f, a) = Tensor (Prim f, a)"
| "redTensor (Tensor (a, b), c) =
Comp (redTensor (a, normalize (Tensor (b, c))), Tensor (a, redTensor (b, c)))"
| "redTensor (a, b) = Tensor (a, b)"
| "red Unit = Unit"
| "red (Prim f) = Prim f"
| "red (Tensor (a, Unit)) = Comp (red a, Runit a)"
| "red (Tensor (Unit, a)) = Comp (red a, Lunit a)"
| "red (Tensor (Prim f, a)) = Tensor (Prim f, red a)"
| "red (Tensor (Tensor (a, b), c)) =
Comp (redTensor (red a, redTensor (red b, red c)), Assoc (a, b, c))"
| "red a = a"
lemma
shows "⋀b. P a b ⟹ Q a b"
and "R a ⟹ S a"
proof (induct a and a rule: redTensor_red.induct)
show ?thesis
sorry
qed
end
Barf.thy
Email Gateway (Aug 22 2022 at 14:59):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Gene,
there is a problem with the types of your expressions.
From the function definition you have
redTensor :: 'a term * ‘a term => 'a term
red :: 'a term => 'a term
Consequently the induction rule for redTensor/red expects two arguments a and b
so that the type of a and b are an instance of 'a term * ‘a term and ‘a term.
In particular this means that
(induct a and a rule: redTensor_red.induct)
must fail, because term term “a" cannot be an instance of 'a term * ‘a term and ‘a term
for the same instance of “‘a”.
Moreover, in your example you do not restrict “a” to be of type “‘a term” at all:
your “a” is of arbitrary type “‘a”.
The following invocation applies the induction rule,
lemma fixes a :: "'a term × 'a term" and b :: "'a term"
shows "⋀c. P a c ⟹ Q a c"
and "R b ⟹ S b"
proof (induct a and b rule: redTensor_red.induct)
Hope this helps,
René
Last updated: Apr 25 2024 at 16:19 UTC