Homework 4

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

declare Let_def [simp]
declare [[names_short]]

type_synonym 'a ptree = "(nat * 'a) tree"


consts set_ptree :: "('a::linorder) ptree \<Rightarrow> 'a set"

consts pbst :: "'a::linorder ptree \<Rightarrow> bool"

consts pins :: "(nat * 'a::linorder) \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree"

consts pisin :: "'a::linorder \<Rightarrow> 'a ptree \<Rightarrow> ('a ptree * nat)"

consts reorder :: "('a::linorder) ptree \<Rightarrow> 'a ptree"


end

Template File

theory Submission
  imports Defs
begin

fun set_ptree :: "('a::linorder) ptree \<Rightarrow> 'a set"  where
  "set_ptree _ = undefined"

lemma set_ptree: "set_ptree t = snd ` set_tree t"
  sorry

fun pbst :: "'a::linorder ptree \<Rightarrow> bool"  where
  "pbst _ = undefined"

fun pins :: "(nat * 'a::linorder) \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree"  where
  "pins _ = undefined"

lemma pins_invar: "pbst t \<Longrightarrow> pbst (pins x t)"
  sorry

fun pisin :: "'a::linorder \<Rightarrow> 'a ptree \<Rightarrow> ('a ptree * nat)"  where
  "pisin _ = undefined"

lemma pisin_set: "pbst t \<Longrightarrow> set_ptree (fst (pisin x t)) = set_ptree t"
  sorry

lemma pisin_invar: "pbst t \<Longrightarrow> pbst (fst (pisin x t))"
  sorry

lemma pisin_inc: "pbst t \<Longrightarrow> (n,x) \<in> set_tree t \<Longrightarrow> (Suc n,x) \<in> set_tree (fst (pisin x t))"
  sorry

term "sort"


definition reorder :: "('a::linorder) ptree \<Rightarrow> 'a ptree"  where
  "reorder _ = undefined"

theorem reorder_pbst: "pbst t \<Longrightarrow> pbst (reorder t)"
  sorry

theorem reorder_pset: "pbst t \<Longrightarrow> set_ptree (reorder t) = set_ptree t"
  sorry

theorem reorder_set: "pbst t \<Longrightarrow> set_tree (reorder t) = set_tree t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma set_ptree: "set_ptree t = snd ` set_tree t"
  by (rule Submission.set_ptree)

lemma pins_invar: "pbst t \<Longrightarrow> pbst (pins x t)"
  by (rule Submission.pins_invar)

lemma pisin_set: "pbst t \<Longrightarrow> set_ptree (fst (pisin x t)) = set_ptree t"
  by (rule Submission.pisin_set)

lemma pisin_invar: "pbst t \<Longrightarrow> pbst (fst (pisin x t))"
  by (rule Submission.pisin_invar)

lemma pisin_inc: "pbst t \<Longrightarrow> (n,x) \<in> set_tree t \<Longrightarrow> (Suc n,x) \<in> set_tree (fst (pisin x t))"
  by (rule Submission.pisin_inc)

theorem reorder_pbst: "pbst t \<Longrightarrow> pbst (reorder t)"
  by (rule Submission.reorder_pbst)

theorem reorder_pset: "pbst t \<Longrightarrow> set_ptree (reorder t) = set_ptree t"
  by (rule Submission.reorder_pset)

theorem reorder_set: "pbst t \<Longrightarrow> set_tree (reorder t) = set_tree t"
  by (rule Submission.reorder_set)

end