Exercise 4

Definitions File

theory Defs
  imports "HOL-Data_Structures.Reverse"
begin

type_synonym 'a stk = "'a list \<times> 'a list"

definition empty :: "'a stk" where
  "empty \<equiv> ([],[])"

consts push :: "'a \<Rightarrow> 'a stk \<Rightarrow> 'a stk"
consts pop_top :: "'a stk \<Rightarrow> 'a stk"
consts pop_bot :: "'a stk \<Rightarrow> 'a stk" 

definition T_push :: "'a \<Rightarrow> 'a stk \<Rightarrow> int" where
  "T_push x stk = 1"

fun T_pop_top :: "'a stk \<Rightarrow> int" where
  "T_pop_top (x#xs,ys) = 1"
| "T_pop_top ([],ys) = int (length ys)"

fun T_pop_bot :: "'a stk \<Rightarrow> int" where
  "T_pop_bot (xs,y#ys) = 1"
| "T_pop_bot (xs,[]) = int (length xs)"

consts \<Phi> :: "'a stk \<Rightarrow> int"

end

Template File

theory Submission
  imports Defs
begin

type_synonym 'a stk = "('a list * 'a list)"

definition empty :: "'a stk" where
  "empty \<equiv> ([],[])"


fun push :: "'a \<Rightarrow> 'a stk \<Rightarrow> 'a stk" where
  "push _ _ = undefined"

fun pop_top :: "'a stk \<Rightarrow> 'a stk" where
  "pop_top _ = undefined"

fun pop_bot :: "'a stk \<Rightarrow> 'a stk" where
  "pop_bot _ = undefined"


term "int :: nat \<Rightarrow> int"
fun \<Phi> :: "'a stk \<Rightarrow> int" where
  "\<Phi> _ = undefined"

lemma \<Phi>_ge_0: "\<Phi> (xs,ys) \<ge> 0"
  sorry

lemma \<Phi>_empty_0: "\<Phi> empty = 0"
  sorry

definition c_pop_bot where "c_pop_bot = undefined"

lemma T_pop_bot: "T_pop_bot (xs,ys) + \<Phi> (pop_bot (xs,ys)) - \<Phi> (xs,ys) \<le> c_pop_bot"
  sorry

end

Check File

theory Check
  imports Submission
begin

(* No checks here *)

end