Email Gateway (Aug 18 2022 at 11:45): Email Gateway (Aug 18 2022 at 11:45):From: chouaffe frannck-edmond <chouaffe2000@yahoo.fr>
Hello isabelle users,
I just want to ask if I can use a Mathml file as an input format for isabelle. I have written some mathematical proofs in Mathml, and I would like to check it within isabelle. Is it possible?
Kind regards.
Edmond
Do You Yahoo!?
En finir avec le spam? Yahoo! Mail vous offre la meilleure protection possible contre les messages non sollicités
http://mail.yahoo.fr Yahoo! Mail
Email Gateway (Aug 19 2022 at 15:59):From: mahmoud abdelazim <m.abdelazim@icloud.com>
i am user of Isabelle and i am trying to proof a theorem for example :
theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induct_tac xs)
apply(auto)
done
The steps of auto could be done using separate steps?
The steps of induct_tac could be done using separate steps?
please provide an example
Email Gateway (Aug 19 2022 at 15:59):From: Lawrence Paulson <lp15@cam.ac.uk>
Induction cannot be broken down into smaller steps. It is a primitive concept.
Larry Paulson
Email Gateway (Aug 19 2022 at 15:59):From: Alfio Martini <alfio.martini@acm.org>
Hi Mahmoud,
Yes, you can prove this theorem in a lot of detail using the proof language
Isar (see the
tutorial "Programming and Proving in Isabelle/HOL").
As an example, I attach a theory that shows the proof of one of the lemmas
you need to prove your theorem.
I use one of the several possible styles.
Best!
isarlistexample.thy
Email Gateway (Aug 19 2022 at 16:21):From: Andrew Boyton <Andrew.Boyton@nicta.com.au>
Hi
Auto runs on both subgoals. Tracing what auto does for each shows auto used the following rules.
rev (rev []) = []
simp_thms(6): (?x = ?x) = True
rev.simps(1): rev [] = []
⋀a list. rev (rev list) = list ⟹ rev (rev (a # list)) = a # list
True_implies_equals: (True ⟹ PROP ?P) ≡ PROP ?P
simp_thms(6): (?x = ?x) = True
append_Cons: (?x # ?xs) @ ?ys = ?x # ?xs @ ?ys
append_Nil: [] @ ?ys = ?ys
rev.simps(1): rev [] = []
rev.simps(2): rev (?x # ?xs) = rev ?xs @ [?x]
rev_append: rev (?xs @ ?ys) = rev ?ys @ rev ?xs
rev_rev_ident: rev (rev ?xs) = ?xs
Andrew
Last updated: Apr 24 2024 at 12:33 UTC