Email Gateway (Jul 11 2022 at 08:21): Email Gateway (Jul 11 2022 at 08:21):From: Jan van Brügge <jan@vanbruegge.de>
Hi,
I am proving some theorem in ML, basically 'P rhs'. This proof is working as expected.
However if I use Local_Theory.define on rhs and try to proof the goal with that, I get an extra sort hypothesis error.
I don't understand where that is coming from. The goal has neither free variables in rhs nor forall bound variables. Could someone help me there?
Thanks
Jan
Email Gateway (Jul 11 2022 at 17:30):From: Peter Lammich <lammich@in.tum.de>
Hi
You get this error if you have a type class that has no instantiation yet.
Does your locale use such a type class?
Peter
Email Gateway (Jul 11 2022 at 21:41):From: Jan van Brügge <jan@vanbruegge.de>
Yes, I generate a class just before the goal that is supposed to be instatiated by the user.
(and that triggers the sort hyposesis error). But the goal should not mention that class. How can I prevent it from doing so?
Cheers,
Jan
Email Gateway (Jul 12 2022 at 09:18):From: Jan van Brügge <jan@vanbruegge.de>
To make it concrete, the goal (with the definition looks like this):
Const ("HOL.Trueprop", "bool ⇒ prop") $
(Const ("Prelim.infinite_regular_card_order", "(((nat suc + nat suc) × nat suc) × (nat suc + nat suc) × nat suc) set ⇒ bool") $
Const ("Composition.foo_sum.sum.Sum_Type.bd_foo_sum",
"(((nat suc + nat suc) × nat suc) ×
(nat suc + nat suc) × nat suc) set"))
The RHS of the definition is this:
Const ("BNF_Cardinal_Arithmetic.cprod",
"((nat suc + nat suc) × (nat suc + nat suc)) set
⇒ (nat suc × nat suc) set ⇒ (((nat suc + nat suc) × nat suc) × (nat suc + nat suc) × nat suc) set") $
(Const ("BNF_Cardinal_Arithmetic.csum",
"(nat suc × nat suc) set ⇒ (nat suc × nat suc) set ⇒ ((nat suc + nat suc) × (nat suc + nat suc)) set") $
(Const ("Prelim.card_suc", "(nat × nat) set ⇒ (nat suc × nat suc) set") $ Const ("BNF_Cardinal_Order_Relation.natLeq", "(nat × nat) set")) $
(Const ("Prelim.card_suc", "(nat × nat) set ⇒ (nat suc × nat suc) set") $
Const ("BNF_Cardinal_Order_Relation.natLeq", "(nat × nat) set"))) $
(Const ("Prelim.card_suc", "(nat × nat) set ⇒ (nat suc × nat suc) set") $
Const ("BNF_Cardinal_Order_Relation.natLeq", "(nat × nat) set")))
And somehow trying to prove the goal with the definition causes this
extra sort hyposesis: [["Composition.var_sumID"]], which is a class that
I generate in the same bunch of ML code.
But neither the goal nor the RHS has any variables at all, so I have no
idea why this sort hypothesis is added. Also without the definition it
works just fine, no sort hypothesis is added to the goal.
Thanks,
Jan
Last updated: Apr 26 2024 at 16:20 UTC