theory Exercise02 imports "HOL-IMP.AExp" begin (* binary trees *) datatype 'a tree = Node "'a tree" 'a "'a tree" | Leaf type_synonym loc = "bool list" (* your definitions here *) consts lookup :: "'a tree \ loc \ 'a tree" contained :: "'a tree \ loc \ bool" update :: "'a tree \ loc \ 'a tree \ 'a tree" (* your proofs here *) lemma "\ contained t loc \ update t loc t' = t" sorry lemma "contained t loc \ lookup (update t loc t') loc = t'" sorry (* where expressions *) datatype wexp = N val | V vname | Plus wexp wexp | Where wexp vname wexp (* your definitions here *) consts wval :: "wexp \ state \ val" inline :: "wexp \ aexp" elim :: "wexp \ wexp" (* your proofs here *) lemma val_inline: "aval (inline e) st = wval e st" sorry lemma "wval (elim e) st = wval e st" sorry end