and Induct_on (which calls the former)
will require the order of the variables in the quantification to match the
order they appear as arguments to the relation. In your case Gm has the Gamma
and then the A, but your quantification has A then Gamma.
Michael
From: Alexander Cox
Date: Wednesday
the form ``!Gm. X ==> P Gm``) in this case. I only use Induct and
Induct_on on simple variables like your Γ Γ’ A.
—Chun
> Il giorno 15 gen 2019, alle ore 14:49, Alexander Cox
> mailto:u6060...@anu.edu.au>> ha scritto:
>
> I am having an issue using Induct_on on a Hol_reln
I am having an issue using Induct_on on a Hol_reln called Gm.
If I try to use it on a trivial goal it works, e.g.
> g `!Γ A. Gm Γ A ==> Gm Γ A`;
…
> e (Induct_on `Gm`);
OK..
1 subgoal:
val it =
(∀A. Gm {|A|} A) ∧ …
but if I use on a useful goal such as:
g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ)
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 `…`;
