Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Basic proof techniques

Exercises on basic proof techniques

Resources

Download Files

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

Terms and Conditions