Re: [isabelle] help

2013/3/16 liujing657949251 <liujing657949251 at>:
> 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:

theory Scratch
imports Main

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"
apply(induction xs)

lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
apply(induction xs)

lemma rev_app [simp]: "rev (app xs ys) = app (rev ys) (rev xs)"
apply(induction xs)

theorem rev_rev [simp]: "rev (rev xs) = xs"
apply(induction 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 MHonArc.