Email Gateway (Aug 22 2022 at 09:49): Email Gateway (Aug 22 2022 at 09:49):From: Mandy Martin <tesleft@hotmail.com>
Hi ,
when programming in Isabelle to use the lemma on a a list defined by let ?aa = "[1,2]"value and thus, still can not show [2,1] in output , what is the correct syntax?
theory Scratch2imports Datatypebegindatatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)(* This is the append function: *)primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)where"[] @ ys = ys" |"(x # xs) @ ys = x # (xs @ ys)"primrec rev :: "'a list => 'a list" where"rev [] = []" |"rev (x # xs) = (rev xs) @ (x # [])"primrec itrev :: "'a list => 'a list => 'a list" where"itrev [] ys = ys" |"itrev (x#xs) ys = itrev xs (x#ys)"value "rev (True # False # [])"lemma app_Nil2 [simp]: "xs @ [] = xs"apply(induct_tac xs)apply(auto)donelemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"apply(induct_tac xs)apply(auto)donelemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"apply(induct_tac xs)let ?aa = "[1,2]" <---- 1 st trialthus ?aa by simp value "rev_app [1,2]" <------------------2nd trial expect reverse to [2,1]
Regards,
Martin Lee
Last updated: Apr 19 2024 at 20:15 UTC