Homework 2

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

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

fun inorder :: "'a ltree \<Rightarrow> 'a list" where
  "inorder (Leaf x) = [x]"
| "inorder (Node l r) = inorder l @ inorder r"  

consts replace_tr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"


consts replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts to_tree :: "'a tree => 'a ltree"


end

Template File

theory Submission
  imports Defs
begin

fun replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  where
  "replace _ = undefined"

lemma replace_len: "length (replace a b xs) = length xs"
  sorry

lemma replace_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace a b xs)"
  sorry

lemma replace_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace a b xs)"
  sorry

fun replace_tr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "replace_tr _ _ acc [] = rev acc" lemma replace_tr_len: "length (replace_tr a b [] xs) = length xs"
  sorry

lemma replace_tr_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace_tr a b [] xs)"
  sorry

lemma replace_tr_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace_tr a b [] xs)"
  sorry

fun to_tree :: "'a tree => 'a ltree"  where
  "to_tree _ = undefined"

lemma to_tree_inorder: "t \<noteq> \<langle>\<rangle> \<Longrightarrow> Tree.inorder t = inorder (to_tree t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma replace_len: "length (replace a b xs) = length xs"
  by (rule Submission.replace_len)

lemma replace_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace a b xs)"
  by (rule Submission.replace_set)

lemma replace_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace a b xs)"
  by (rule Submission.replace_set2)

lemma replace_tr_len: "length (replace_tr a b [] xs) = length xs"
  by (rule Submission.replace_tr_len)

lemma replace_tr_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace_tr a b [] xs)"
  by (rule Submission.replace_tr_set)

lemma replace_tr_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace_tr a b [] xs)"
  by (rule Submission.replace_tr_set2)

lemma to_tree_inorder: "t \<noteq> \<langle>\<rangle> \<Longrightarrow> Tree.inorder t = inorder (to_tree t)"
  by (rule Submission.to_tree_inorder)

end