[isabelle] how to reverse the list in this case



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


 		 	   		  


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