Hello, I’m doing a project on proof theory, and I’m trying to define the proof rules with Hol_reln. I am defining multiple proof systems which build upon each other, i.e. intuitionistic logic then classical logic. It seems natural to have something like:
var (Sys1_rules, …,…) = Hol_reln `…`; var (Sys2_rules,…,…) = Hol_reln `!x. Sys1 x ==> Sys2 x /\ …` But when I go to prove something which needs to use Sys2 rules then Sys1 rules, I don’t know how to get it to work, since the Sys1 rules don’t know mention Sys2 (nor should they). For example: `Sys2 x` by metis_tac[Sys2_rules] `Sys2 y` by metis_tac[Sys1_rules,Sys2_rules] (* Sys1 has no rules for Sys2, so this fails! *) The obvious solution is to just keep them independent and have all the rules in each of them, but I thought I might be missing some elegant way of achieving this. Please let me know if there is such a trick. Thank you, Alex
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
