Email Gateway (Aug 18 2022 at 10:39): Email Gateway (Aug 18 2022 at 10:39):From: Wolff Burkhart <bwolff@inf.ethz.ch>
Dear all,
is there any way to erase the following form of
redundant premises in a rule in forward-reasoning?
I.e., I'd like to have a function of type thm => thm that
converts:
[| A ==> True; B |] ==> C
into
B ==> C.
(We are talking about HOL.)
Best,
bu
Email Gateway (Aug 18 2022 at 10:39):From: Amine Chaieb <chaieb@in.tum.de>
Hi,
The following works for me:
lemma annoyTrue: "(P ==> True) == Trueprop True"
apply (atomize (full)) by auto
lemma "[| A ==> True ; B |] ==> C"
apply (simp add: annoyTrue)
proof (prove): step 1
goal (1 subgoal):
1. B ==> C
Amine.
Wolff Burkhart wrote:
Email Gateway (Aug 18 2022 at 10:39):From: Amine Chaieb <chaieb@in.tum.de>
Wolff Burkhart wrote:
I.e., I'd like to have a function of type thm => thm that
converts:
I have forgotten this part of the question:
This solves the problem:
lemma annoyTrue: "(P ==> True) == Trueprop True"
apply (atomize (full)) by auto
lemma annoyTrue': "(True ==> PROP P) == PROP P" by auto
ML{* Simplifier.rewrite_rule [@{thm annoyTrue}, @{thm annoyTrue'}]
(assume @{cterm "[| A ==> True ; B |] ==> C"})*}
The function is then just
Simplifier.rewrite_rule [@{thm annoyTrue}, @{thm annoyTrue'}]
Cheers,
Amine.
Email Gateway (Aug 18 2022 at 10:39):From: Makarius <makarius@sketis.net>
fn thm => TrueI RS thm;
Makarius
Last updated: May 03 2024 at 01:09 UTC