Two relations are not likely to give you what you want in this scenario. For example, if the first system has a rule for conjunction introduction:
Thm1 p /\ Thm1 q ==> Thm1 (p AND q) then this rule requires Thm1 hypotheses. If you add Thm1 p ==> Thm2 p you don’t get to use Thm2 hypotheses to prove conjunctions using the first rule. If you’re committed to this notion of systems of rules that can be extended in the way you want, I think there’s probably a bit of work required I’m afraid, and it may not really win you much. I agree though that having to repeat rules for things like conjunction introduction feels annoying. Michael From: Alexander Cox <u6060...@anu.edu.au> Date: Friday, 4 January 2019 at 09:11 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] Relations which build upon each other 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
