theory s3 imports Main begin

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

section "Balanced Parentheses"

datatype letter = L | R

type_synonym lang = "letter list set"

-- "a)"

inductive_set S :: "lang"
where
 emptyI:  "[] \<in> S" |
 insertI: "\<lbrakk>xs \<in> S\<rbrakk> \<Longrightarrow> L # (xs @ [R]) \<in> S" |
 appendI: "\<lbrakk>xs \<in> S; ys \<in> S\<rbrakk> \<Longrightarrow> xs @ ys \<in> S"

-- "b)"

lemma eg1: "[L,R,L,L,R,R] \<in> S" 
  apply (rule appendI[where xs="[L,R]" and ys="[L,L,R,R]", simplified])
   apply (rule insertI[where xs="[]", simplified])
   apply (rule emptyI)
  apply (rule insertI[where xs="[L,R]", simplified])
  apply (rule insertI[where xs="[]", simplified])
  apply (rule emptyI)
  done

lemma eg2: "[L,L,R,L,L,R,R,R] \<in> S"
  apply (rule insertI[where xs="[L,R,L,L,R,R]", simplified])
  apply (rule eg1)
  done

-- "c)"

fun is_bal :: "letter list \<Rightarrow> nat \<Rightarrow> bool"
where
  "is_bal [] n = (n = 0)" |
  "is_bal (L # xs) n = is_bal xs (Suc n)" |
  "is_bal (R # xs) n = (n \<noteq> 0 \<and> is_bal xs (n - 1))"

value "is_bal [L,L,R,R] 0"
value "is_bal [L,R,R] 0"
value "is_bal [] 0"
value "is_bal [L,L,R,L,L,R,R,R] 0"

-- "d)"

lemma is_bal_append: "\<lbrakk>is_bal xs n; is_bal ys m\<rbrakk> \<Longrightarrow> is_bal (xs @ ys) (n+m)"
  by (induct xs n rule:is_bal.induct, auto)

lemma "xs \<in> S \<Longrightarrow> is_bal xs 0"
  by (induct xs rule:S.induct, auto intro:is_bal_append[where n=0 and m="Suc 0", simplified] 
                                          is_bal_append[where n=0 and m=0, simplified])
 
-- -----------------------------------------------------

section "Expressions"

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

type_synonym state = "string \<Rightarrow> nat"

-- "a) Evaluating expressions"

primrec aval :: "expr \<Rightarrow> state \<Rightarrow> nat"
where
  "aval (Const n) s = n" |
  "aval (Var x) s = s x" |
  "aval (Plus v w) s = (aval v s) + (aval w s)"

value "aval (Plus (Var ''x'') (Const 5)) ((\<lambda>x. undefined)(''x'':=3))"


-- "b) Simplifying expressions"

type_synonym vars = "string \<Rightarrow> nat option"

fun asimp :: "expr \<Rightarrow> vars \<Rightarrow> expr"
where
   "asimp (Const n) t =  Const n" 
 | "asimp (Var x) t = (case t x of
                       Some n \<Rightarrow> Const n 
                     | None \<Rightarrow> Var x)"
 | "asimp (Plus v w) t = (case (asimp v t, asimp w t) of 
                       (Const k, Const l) \<Rightarrow> Const (k+l)
                     | (Const 0, e) \<Rightarrow> e
                     | (e, Const 0) \<Rightarrow> e
                     | (f,g) \<Rightarrow> Plus f g)"

-- "c) formulate and prove correctness lemma"

lemma asimp_corr: "\<lbrakk>\<forall>x n. t x = Some n \<longrightarrow> s x = n \<rbrakk> \<Longrightarrow> aval (asimp e t) s = aval e s"    
  by (induct e rule:expr.induct, auto split:option.splits expr.splits nat.splits)


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

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:"
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where 
  "sep a (x # y # zs) = x # a # sep a (y # zs)" |
  "sep a xs = xs" 

(* paths are stored in reverse" *)
fun str :: "path \<Rightarrow> string"
where
  "str xs = concat (rev (sep ''/'' (map str_of xs)))" 
  
-- "b) implement chdir"

fun chdir :: "seg \<Rightarrow> path \<Rightarrow> path" 
where 
  "chdir Root x = [Root]" |
  "chdir Parent xs = (case xs of
                         Seg s # xs \<Rightarrow> xs |
                         xs \<Rightarrow> Parent # xs)" |
  "chdir (Seg s) xs = (Seg s) # xs"

-- "c) implement norm"

value "chdir Parent [Parent, Parent, Seg ''a'', Seg ''b'', Root]"

fun norm :: "path \<Rightarrow> path"
where 
  "norm [] = []" | 
  "norm (x # xs) = chdir x (norm xs)"

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

(* Elements of the base path - paths consisting of the root and parent *)

inductive_set basePath :: "path set"
where
  emptyBase: "[] \<in> basePath" |
  rootBase: "[Root] \<in> basePath" |
  parentBase: "p \<in> basePath \<Longrightarrow> (Parent # p) \<in> basePath" 

inductive_set normalisedPaths :: "path set"
where
  baseNorm: "p \<in> basePath \<Longrightarrow> p \<in> normalisedPaths" |
  extendNorm: "p \<in> normalisedPaths \<Longrightarrow> (Seg x # p) \<in> normalisedPaths"

declare basePath.intros[intro]
declare normalisedPaths.intros[intro]

lemma chdir_norm:
  "norm xs \<in> normalisedPaths \<Longrightarrow> chdir x (norm xs) \<in> normalisedPaths"
  apply(induct rule: normalisedPaths.induct)
   apply (case_tac x, auto split: list.splits seg.splits elim: basePath.cases)+
  done

lemma norm_corr: "norm p \<in> normalisedPaths"
  apply (induct p rule:norm.induct)
     apply (simp)
     apply (rule baseNorm)
     apply (rule emptyBase)
    apply (simp only: norm.simps(2))
    apply (erule chdir_norm)
  done 
  
-- "e) prove that norm is the identity on normal paths"

lemma basePath_id: "p \<in> basePath \<Longrightarrow> norm p = p"
  apply (induct p rule:basePath.induct)
    apply simp
   apply simp
  apply (simp only: norm.simps(2))
  apply (erule basePath.cases)
    apply auto
  done

lemma norm_id1: "\<lbrakk>p \<in> normalisedPaths\<rbrakk> \<Longrightarrow> norm p = p" 
  by (induct p rule:normalisedPaths.induct, auto elim:basePath_id)

lemma norm_id2: "\<lbrakk>norm p = p \<rbrakk> \<Longrightarrow> p \<in> normalisedPaths"
  by (erule subst, rule norm_corr)

lemma norm_identity: "norm p = p \<longleftrightarrow> p \<in> normalisedPaths"
  by (intro iffI, (elim norm_id2 norm_id1)+)

end