Re: [isabelle] Isabelle



Hi

Auto runs on both subgoals. Tracing what auto does for each shows auto used the following rules.

 1. rev (rev []) = []
    simp_thms(6): (?x = ?x) = True
    rev.simps(1): rev [] = []

 2. ⋀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


On 30 Sep 2014, at 10:15 pm, mahmoud abdelazim <m.abdelazim at icloud.com<mailto:m.abdelazim at icloud.com>> wrote:

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




________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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