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

### 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 =" |
"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