Basic proof techniques

Definitions File

theory Defs
imports Main 
begin

fun strangeAppend :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"strangeAppend l1 [] = l1" |
"strangeAppend l1 (x#xs) = (x#(strangeAppend l1 xs))"

fun sumList:: "nat list \<Rightarrow> nat"
where
"sumList []=0" |
"sumList (x#xs)= x+(sumList xs)"

value "sumList [1,2,3,4,5]"

fun sumNat:: "nat \<Rightarrow> nat"
where
"sumNat 0= 0" |
"sumNat i= (i+(sumNat (i - 1)))"

value "sumNat 5"

fun makeList:: "nat \<Rightarrow> nat list"
where
"makeList 0 =[0]" |
"makeList i = (i#(makeList (i - 1)))"

fun noDouble:: "'a list \<Rightarrow> bool"
where
"noDouble []=True" |
"noDouble (x#xs)=(if (List.member xs x) then False else (noDouble xs))"


datatype 'a binTree= Leaf | Node 'a "'a binTree" "'a binTree"

fun memberTree:: "'a \<Rightarrow> 'a binTree \<Rightarrow> bool"
where
"memberTree _ Leaf = False" |
"memberTree x (Node y tg td)= (if x=y then True else ((memberTree x tg) \<or> (memberTree x td)))"

fun subTree:: "'a binTree \<Rightarrow> 'a binTree \<Rightarrow> bool"
where
"subTree Leaf Leaf = True" |
"subTree _ Leaf=False" |
"subTree x (Node y tg td)= (if x=(Node y tg td) then True else ((subTree x tg) \<or> (subTree x td)))"


value "subTree (Node (1::nat) Leaf Leaf) (Node 2 (Node 1 Leaf Leaf) Leaf)"

fun leq::"nat => nat => bool"   (infix "=<" 65)
where 
"leq 0 _ = True" |
"leq (Suc _) 0 = False" |
"leq (Suc x) (Suc y) = leq x y"


fun div2 :: "nat \<Rightarrow> nat" 
where
"div2 0 = 0" |
"div2 (Suc 0) = 0" |
"div2 (Suc(Suc n)) = Suc(div2 n)"


function zip:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  where
"zip [] l = l" |
"zip (e#r) l = e#(zip l r)"
apply pat_completeness
apply auto
done
termination zip
  apply (relation "measure (\<lambda>(l1,l2). (length l1 + length l2))")
   apply auto
  done
end

Template File

theory Submission
imports Defs
begin

lemma length_makeList: "length(makeList i)=i+1"
  sorry


lemma sumNat_nat: "sumNat i >= i"
  sorry

lemma sumNat_nat2: "sumNat i = (i*(i+1)) div 2"
  sorry

lemma sumNat_makeList: "sumNat i= sumList(makeList i)"
  sorry

lemma sumNatInf: "(i < 3) \<longrightarrow> ((sumNat i) < 10)"
  sorry

lemma noDoubleMakeList: "(noDouble (makeList i))"
  sorry

lemma lengthStrangeAppend: "length (strangeAppend l1 l2) \<ge> (length l2)"
  sorry


lemma memberSubtree: "((memberTree e t) \<and> (subTree t t2)) \<longrightarrow> (memberTree e t2)"
  sorry

lemma sym: "((x=<y) \<and> (y=< x)) \<longrightarrow> (x=y)"
  sorry

lemma div2_nat: "(div2 n) \<le>  n"
  sorry

lemma proofZip: "((List.member l1 x) \<or> (List.member l2 x)) = (List.member (zip l1 l2) x)"
  sorry
end

Check File

theory Check
imports Submission
begin


lemma "length(makeList i)=i+1" by (rule Submission.length_makeList)

lemma "sumNat i >= i" by (rule Submission.sumNat_nat)

lemma "sumNat i = (i*(i+1)) div 2"  by (rule Submission.sumNat_nat2)

lemma "sumNat i= sumList(makeList i)"  by (rule Submission.sumNat_makeList)

lemma "(i < 3) \<longrightarrow> ((sumNat i) < 10)" by (rule Submission.sumNatInf)

lemma "(noDouble (makeList i))"  by (rule Submission.noDoubleMakeList)

lemma "length (strangeAppend l1 l2) \<ge> (length l2)"  by (rule Submission.lengthStrangeAppend)

lemma "((memberTree e t) \<and> (subTree t t2)) \<longrightarrow> (memberTree e t2)" by (rule Submission.memberSubtree)

lemma "((x=<y) \<and> (y=< x)) \<longrightarrow> (x=y)" by (rule Submission.sym)

lemma "(div2 n) \<le>  n" by (rule Submission.div2_nat)

lemma "((List.member l1 x) \<or> (List.member l2 x)) = (List.member (zip l1 l2) x)"  by (rule Submission.proofZip)

end