theory a3 imports Main begin

-- -----------------------------------------------------

section "Balanced Parentheses"

datatype letter = L | R

type_synonym lang = "letter list set"

-- "a) define grammar for S inductively"

-- "b) prove examples"

-- "c) define is_bal"

-- "d) show correctness of is_bal"


-- -----------------------------------------------------

section "Expressions"

datatype expr = Const nat | Var string | Plus expr expr

type_synonym state = "string \<Rightarrow> nat"

-- "a) change to a function definition:"
consts aval :: "expr \<Rightarrow> state \<Rightarrow> nat"


-- "b)"
type_synonym vars = "string \<Rightarrow> nat option"

-- "change to a function definition:"
consts asimp :: "expr \<Rightarrow> vars \<Rightarrow> expr"

-- "c) formulate and prove correctness lemma"


-- -----------------------------------------------------

section "File System Paths"

datatype seg = Root | Parent | Seg string

type_synonym path = "seg list" 

fun str_of where
  "str_of Root = ''//''" |
  "str_of Parent = ''..''" |
  "str_of (Seg s) = s"

-- "a)"

-- "implement sep and str:"
consts sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" 

consts str :: "path \<Rightarrow> string" 
  
-- "b) implement chdir"
consts chdir :: "seg \<Rightarrow> path \<Rightarrow> path" 

-- "c) implement norm"
consts norm :: "path \<Rightarrow> path"


-- "d) formulate and prove correctness of norm"


-- "e) prove that norm is the identity on normal paths"


end