theory ex03 imports Main AExp BExp begin datatype ifexp = Bc' bool | If ifexp ifexp ifexp | Less' aexp aexp primrec ifval :: "ifexp \ state \ bool" where "ifval (Bc' b) _ = b" | "ifval (If b1 b2 b3) st = (if ifval b1 st then ifval b2 st else ifval b3 st)" | "ifval (Less' a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)" fun Or :: "bexp \ bexp \ bexp" where "Or b1 b2 = Not (And (Not b1) (Not b2))" fun If_bexp :: "bexp \ bexp \ bexp \ bexp" where "If_bexp b1 b2 b3 = Or (And b1 b2) (And (Not b1) b3)" primrec translate :: "ifexp \ bexp" where "translate (Bc' b) = (Bc b)" | "translate (If b1 b2 b3) = If_bexp (translate b1) (translate b2) (translate b3)" | "translate (Less' a1 a2) = Less a1 a2" lemma translate_sound: "bval (translate exp) s = ifval exp s" by (induct exp) auto text {* Relational @{text "aval"}*} inductive is_aval :: "aexp \ state \ val \ bool" where "is_aval (N n) s n" | "s x = v \ is_aval (V x) s v" | "\is_aval a1 s v1; is_aval a2 s v2; v'=v1+v2\ \ is_aval (Plus a1 a2) s v'" text {* Use the introduction rules @{text is_aval.intros} to prove this example lemma. *} lemma "is_aval (Plus (N 2) (Plus (V x) (N 3))) s (2 + (s x + 3))" by (auto intro!: is_aval.intros) text {* Prove that the evaluation relation @{text is_aval} agrees with the evaluation function @{text aval}. Show implications in both directions, and then prove the if-and-only-if form. *} lemma aval1: "is_aval a s v \ aval a s = v" by (induct set: is_aval, auto) lemma aval2: "aval a s = v \ is_aval a s v" by (induct a arbitrary: v, auto intro: is_aval.intros) theorem "is_aval a s v \ aval a s = v" proof assume "is_aval a s v" thus "aval a s = v" by (rule aval1) next assume "aval a s = v" thus "is_aval a s v" by (rule aval2) qed (*The version without equality assumptions also works.*) inductive is_aval' :: "aexp \ state \ val \ bool" where "is_aval' (N n) s n" | "is_aval' (V x) s (s x)" | "\is_aval' a1 s v1; is_aval' a2 s v2\ \ is_aval' (Plus a1 a2) s (v1 + v2)" lemma "is_aval' (Plus (V x) (Plus (V y) (N 3))) s (s x + (s y + 3))" by (auto intro!: is_aval'.intros) theorem "is_aval' a s v \ aval a s = v" apply (rule iffI) apply (induct set: is_aval') apply auto apply (induct a arbitrary: v) apply (auto intro: is_aval'.intros) done end