Re: [isabelle] [Q]Question about Isabelle/hol
On 22.07.2012 08:13, 後藤 裕貴 wrote:
> I am sorry for the delay in my response.
> I am grateful for all the help you game me while we were try to fix the issue.
> I ask you a question about proof of "'a list list" this time.
> I want to prove that there is not overlap even if I append it in each top on the list when "'a list list" does not have overlap.
> fun prefix_app :: "'a list list => 'a list => 'a list list" where
> "prefix_app  y = " |
> "prefix_app xs  = xs" |
> "prefix_app (x#xs) y = (y @ x) # (prefix_app xs y)"
> lemma "(distinct xs) ==> (distinct (prefix_app xs y))"
> apply (induct_tac y)
I would probably proceed by proving that
"prefix_app xs y = map (%z. y @ z) xs"
holds and that "%z. y @ z" is injective. Then the proposition follows
This archive was generated by a fusion of
Pipermail (Mailman edition) and