Exercise 3

Definitions File

theory Defs
  imports Main
begin

end

Template File

theory Submission
  imports Defs
begin

(*
fun norm :: "'a list \<times> 'a list \<Rightarrow> 'a list \<times> 'a list" where
  "norm (fs,rs) = (if fs = [] then (itrev rs [],[]) else (fs,rs))"

fun enq :: "'a \<Rightarrow> 'a list \<times> 'a list \<Rightarrow> 'a list \<times> 'a list" where
  "enq a (fs, rs) = norm (fs, a # rs)"

fun deq :: "'a list \<times> 'a list \<Rightarrow> 'a list \<times> 'a list" where
  "deq (fs,rs) = (if fs = [] then (fs,rs) else norm (tl fs,rs))"

fun first :: "'a list \<times> 'a list \<Rightarrow> 'a" where
  "first (a#_,_) = a"
*)

type_synonym 'a stack = \<comment>\<open>TODO\<close>

fun enq :: "'a::linorder \<Rightarrow> 'a stack \<times> 'a stack \<Rightarrow> 'a stack \<times> 'a stack" where
  "enq _ _ = undefined"

fun deq :: "'a::linorder stack \<times> 'a stack \<Rightarrow> 'a stack \<times> 'a stack" where
  "deq _ = undefined"

fun first :: "'a stack \<times> 'a stack \<Rightarrow> 'a" where
  "first _ = undefined"

fun get_min :: "'a::linorder stack \<times> 'a stack \<Rightarrow> 'a" where
  "get_min _ = undefined"

end

Check File

theory Check
  imports Submission
begin

end