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
from List.distinct_map.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.