Re: [isabelle] help
2013/3/16 liujing657949251 <liujing657949251 at 126.com>:
> Dear all proof lovers:
> I am really new to Isabelle. I hope to use Isabell/HOL for proving. Recently I am reading prog-prove in Isabelle.doc. Until now I have read half of it, but I am so puzzled that I really don't know how to combine the little examples in doc with the Isabelle/jEdit.
> They are just some fragments in one proof, I guess. So what should I do next?
> By the way, if I use Isabelle/jEdit, do I need study Isar in chapter 4 of the doc?
> My tutor told me to read some little examples, but I usually do not know why some lemmas should be proved first or some else. I do not know why I read the doc, but it doesn't help me to these question.
> So I really hope to know how to learn.
> Thank you very much!
> Best wishes!
> Liu Jing
You can copy and paste the following example into jEdit:
datatype 'a myList = Nil | Cons 'a "'a myList"
fun app :: "'a myList => 'a myList => 'a myList" where
"app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"
fun rev :: "'a myList => 'a myList" where
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
value "rev (Cons True (Cons False Nil))"
value "rev (Cons a (Cons b Nil))"
lemma app_Nil2 [simp]: "app xs Nil = xs"
lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
lemma rev_app [simp]: "rev (app xs ys) = app (rev ys) (rev xs)"
theorem rev_rev [simp]: "rev (rev xs) = xs"
make sure that you save it in a file called Scratch.thy
This archive was generated by a fusion of
Pipermail (Mailman edition) and