Yiming Xu (Dec 14 2024 at 15:51): Yiming Xu (Dec 14 2024 at 15:51):Say, I have this thm, may call it Property.simps
Property a b <=> (a = 0 /\ P1 b) \/ (?a0. R a a0 /\ P2 b)
Within my goal, I may have proved something like p:"Property (n + 1) b". Then I would like to write
p[THEN iffD1,THEN ...] where p[THEN iffD1] should give me a local thm(n+1 = 0 /\ P1 b) \/ (?a0. R (n+1) a0 /\ P2 b)
Then I want to apply a conversion on this local thm to eliminate the first conj, since we have \not n+1 = 0.
Yiming Xu (Dec 14 2024 at 15:52):In the case that this makes sense, I would like the Isabelle counterpart of such a thing:
val act_by_def = new_specification(
"act_by_def",
["act_by"],
lemma |> SIMP_RULE bool_ss [SKOLEM_THM]
|> CONV_RULE (RENAME_VARS_CONV ["t"] (* to allow rename of f' back to f *)
THENC BINDER_CONV (RENAME_VARS_CONV ["f", "g", "x", "y"])));
SIMP_RULE takes a simpset and some theorems, and gives a rule (i.e. a function thm -> thm) that manipulates on thms that simps the input theorem using the simpset and the extra thm.
Yiming Xu (Dec 14 2024 at 15:54):CONV_RULE takes a conv, which only outputs iffs, into a rule that transforms the given thm according to the iff thm produced by the given conv.
Yiming Xu (Dec 14 2024 at 15:54):Can we write in Isabelle after a THEN to do something similar?
Mathias Fleury (Dec 14 2024 at 16:12):not a then, but:
context
fixes P1 P2 :: ‹nat ⇒ bool› and
R :: ‹nat ⇒ nat ⇒ bool›
begin
definition Property where
‹Property a b ⟷ (a = 0 ∧ P1 b) ∨ (∃a0. R a a0 ∧ P2 b)›
thm Property_def[of ‹Suc n›, simplified]
Aha that is the sort of thing I want. Although less flexible, this already helps a lot!
Last updated: Dec 30 2024 at 16:22 UTC