Isaac Freund (Oct 14 2022 at 15:37): Isaac Freund (Oct 14 2022 at 15:37):Ich möchte ∃c::In. (Foo c) auf Foo cin vereinfachen da In als typedef In = "{cin}" definiert ist. Wahrscheinlich übersehe ich etwas, aber ich finde kein Regel was ich dafür anwenden kann. Hat jemand einen Tip?
Mathias Fleury (Oct 14 2022 at 15:47):(answering in English)
Foo cin does not make sense as ti does not type. But you can the use the lifting (default name Abs_In) to convert the type. For example:
typedef test = "{False}"
by auto
lemma "(∃x :: test. P x) = P (Abs_test False)"
by (metis(full_types) Rep_test Rep_test_inject singletonD)
(Sledgehammer is great)
Isaac Freund (Oct 14 2022 at 15:58):My bad, I meant to edit to English before pressing enter. The actual subgoal I'm working with is somewhat more complex
1. (LEAST n::lnat. ∃c::In. n = #⇩√ (Abs_sb (λc::In. ↑(Timed (TOne True))) ▸ c)) = (1::lnat)
It seems like singletonD may be useful though thanks
Last updated: Apr 27 2024 at 01:05 UTC