Email Gateway (Aug 18 2022 at 17:34): Email Gateway (Aug 18 2022 at 17:34):From: 张欢欢 <hzhang@ecust.edu.cn>
Hi all:
I am getting stuck in a proof. Besides other questions I am quite confused about this one:
lemma [simp]:"\<forall> f. set f \<subseteq> set (sweep h r f )"
apply(induct h)
...
proof-
fix a h assume IH:"\<forall> f . set
f
\<subseteq> set (sweep h r
f
)"
...
fix f from IH have "set
(a # f)
\<subseteq> set (sweep h r
(a # f)
)" sorry
Why this step is wrong? I did use the \<forall> f? sweep is defined by primrec.
Thanks
Huanhuan Zhang
Email Gateway (Aug 18 2022 at 17:34):From: Makarius <makarius@sketis.net>
It is not immediately clear what you are trying to do, but the approach
looks a bit nonstandard. What is "..." after the initial
"apply (induct h)".
You should not do too many things at the same time, it will make the
development of the proof difficult ("getting stuck") and confuse the
reader of the result.
Here is a standard pattern for plain mathematical induction:
notepad
begin
fix n :: nat
have "P n"
proof (induct n) print_cases
case 0
show ?case sorry
next
case (Suc n)
thm Suc.hyps
show ?case sorry
qed
end
The auxiliary print_cases gives an idea about the local contexts that are
available in each branch of the proof -- that command can be deleted from
the final version.
Also note that auxiliary quantification of the statement is really
ancient. The "induct" method already knows about "arbitrary" variables.
See also ~~/src/HOL/Induct/Common_Patterns.thy for more advanced examples.
Makarius
Last updated: Apr 24 2024 at 04:17 UTC