How to define an expression translator?

Question

I defined 2 almost identical languages (foo and bar):

theory SimpTr
  imports Main
begin

type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"

datatype foo_exp =
  FooBConst bool |
  FooIConst int |
  FooLet vname foo_exp foo_exp |
  FooVar vname |
  FooAnd foo_exp foo_exp

datatype bar_exp =
  BarBConst bool |
  BarIConst int |
  BarLet vname bar_exp bar_exp |
  BarVar vname |
  BarAnd bar_exp bar_exp

A trivial semantics:

datatype foo_val = FooBValue bool | FooIValue int
datatype bar_val = BarBValue bool | BarIValue int

type_synonym foo_env = "foo_val env"
type_synonym bar_env = "bar_val env"

inductive foo_big_step :: "foo_exp × foo_env ⇒ foo_val ⇒ bool"
  (infix "⇒f" 55) where
"(FooBConst c, e) ⇒f FooBValue c" |
"(FooIConst c, e) ⇒f FooIValue c" |
"(init, e) ⇒f x ⟹
 (body, e(var↦x)) ⇒f v ⟹
 (FooLet var init body, e) ⇒f v" |
"e var = Some v ⟹
 (FooVar var, e) ⇒f v" |
"(a, e) ⇒f FooBValue x ⟹
 (b, e) ⇒f FooBValue y ⟹
 (FooAnd a b, e) ⇒f FooBValue (x ∧ y)"

inductive_cases FooBConstE[elim!]: "(FooBConst c, e) ⇒f v"
inductive_cases FooIConstE[elim!]: "(FooIConst c, e) ⇒f v"
inductive_cases FooLetE[elim!]: "(FooLet var init body, e) ⇒f v"
inductive_cases FooVarE[elim!]: "(FooVar var, e) ⇒f v"
inductive_cases FooAndE[elim!]: "(FooAnd a b, e) ⇒f v"

inductive bar_big_step :: "bar_exp × bar_env ⇒ bar_val ⇒ bool"
  (infix "⇒b" 55) where
"(BarBConst c, e) ⇒b BarBValue c" |
"(BarIConst c, e) ⇒b BarIValue c" |
"(init, e) ⇒b x ⟹
 (body, e(var↦x)) ⇒b v ⟹
 (BarLet var init body, e) ⇒b v" |
"e var = Some v ⟹
 (BarVar var, e) ⇒b v" |
"(a, e) ⇒b BarBValue x ⟹
 (b, e) ⇒b BarBValue y ⟹
 (BarAnd a b, e) ⇒b BarBValue (x ∧ y)"

inductive_cases BarBConstE[elim!]: "(BarBConst c, e) ⇒b v"
inductive_cases BarIConstE[elim!]: "(BarIConst c, e) ⇒b v"
inductive_cases BarLetE[elim!]: "(BarLet var init body, e) ⇒b v"
inductive_cases BarVarE[elim!]: "(BarVar var, e) ⇒b v"
inductive_cases BarAndE[elim!]: "(BarAnd a b, e) ⇒b v"

Typing:

datatype foo_type = FooBType | FooIType
datatype bar_type = BarBType | BarIType

type_synonym foo_tenv = "foo_type env"
type_synonym bar_tenv = "bar_type env"

inductive foo_typing :: "foo_tenv ⇒ foo_exp ⇒ foo_type ⇒ bool"
  ("(1_/ ⊢f/ (_ :/ _))" [50,0,50] 50) where
"Γ ⊢f FooBConst c : FooBType" |
"Γ ⊢f FooIConst c : FooIType" |
"Γ ⊢f init : τ⇩1 ⟹
 Γ(var↦τ⇩1) ⊢f body : τ ⟹
 Γ ⊢f FooLet var init body : τ" |
"Γ var = Some τ ⟹
 Γ ⊢f FooVar var : τ" |
"Γ ⊢f a : BType ⟹
 Γ ⊢f b : BType ⟹
 Γ ⊢f FooAnd a b : BType"

inductive bar_typing :: "bar_tenv ⇒ bar_exp ⇒ bar_type ⇒ bool"
  ("(1_/ ⊢b/ (_ :/ _))" [50,0,50] 50) where
"Γ ⊢b BarBConst c : BarBType" |
"Γ ⊢b BarIConst c : BarIType" |
"Γ ⊢b init : τ⇩1 ⟹
 Γ(var↦τ⇩1) ⊢b body : τ ⟹
 Γ ⊢b BarLet var init body : τ" |
"Γ var = Some τ ⟹
 Γ ⊢b BarVar var : τ" |
"Γ ⊢b a : BType ⟹
 Γ ⊢b b : BType ⟹
 Γ ⊢b BarAnd a b : BType"

inductive_cases [elim!]:
  "Γ ⊢f FooBConst c : τ"
  "Γ ⊢f FooIConst c : τ"
  "Γ ⊢f FooLet var init body : τ"
  "Γ ⊢f FooVar var : τ"
  "Γ ⊢f FooAnd a b : τ"

inductive_cases [elim!]:
  "Γ ⊢b BarBConst c : τ"
  "Γ ⊢b BarIConst c : τ"
  "Γ ⊢b BarLet var init body : τ"
  "Γ ⊢b BarVar var : τ"
  "Γ ⊢b BarAnd a b : τ"

lemma foo_typing_is_fun:
  "Γ ⊢f exp : τ⇩1 ⟹
   Γ ⊢f exp : τ⇩2 ⟹
   τ⇩1 = τ⇩2"
  apply (induct Γ exp τ⇩1 arbitrary: τ⇩2 rule: foo_typing.induct)
  apply blast
  apply blast
  apply blast
  apply fastforce
  by blast

lemma bar_typing_is_fun:
  "Γ ⊢b exp : τ⇩1 ⟹
   Γ ⊢b exp : τ⇩2 ⟹
   τ⇩1 = τ⇩2"
  apply (induct Γ exp τ⇩1 arbitrary: τ⇩2 rule: bar_typing.induct)
  apply blast
  apply blast
  apply blast
  apply fastforce
  by blast

Also I defined a translator from foo to bar:

primrec FooToBar :: "foo_exp ⇒ bar_exp option" where
  "FooToBar (FooBConst c) = Some (BarBConst c)" |
  "FooToBar (FooIConst c) = None" |
  "FooToBar (FooLet var init body) = (case FooToBar init of
    Some barInit ⇒ (case FooToBar body of
      Some barBody ⇒ Some (BarLet var barInit barBody) |
    _ ⇒ None) | _ ⇒ None)" |
  "FooToBar (FooVar var) = Some (BarVar var)" |
  "FooToBar (FooAnd a b) = (case (FooToBar a, FooToBar b) of
    (Some a1, Some b1) ⇒ Some (BarAnd a1 b1) | _ ⇒ None)"

And I'm trying to prove that the translator transforms foo-expressions to bar-expressions with similar types:

inductive type_equiv :: "foo_type ⇒ bar_type ⇒ bool" (infix "∼" 50) where
"FooBType ∼ BarBType" |
"FooIType ∼ BarIType"

lemma FooToBarPreserveType:
  "FooToBar fooExp = Some barExp ⟹
   Γ1 ⊢f fooExp : t1 ⟹
   Γ2 ⊢b barExp : t2 ⟹
   t1 ∼ t2"
  apply (induct fooExp arbitrary: barExp Γ1 Γ2 t1 t2)

And also the transformation preserves semantics of expressions:

inductive val_equiv :: "foo_val ⇒ bar_val ⇒ bool" (infix "≈" 50) where
"v⇩F = v⇩B ⟹ FooBValue v⇩F ≈ BarBValue v⇩B" |
"v⇩F = v⇩B ⟹ FooIValue v⇩F ≈ BarIValue v⇩B"

lemma FooToBarPreserveValue:
  "FooToBar fooExp = Some barExp ⟹
   FooEval fooExp fooEnv = Some v1 ⟹
   BarEval barExp barEnv = Some v2 ⟹
   v1 ≈ v2"
  apply (induct fooExp arbitrary: barExp fooEnv barEnv v1 v2)

I even proved some induction cases. But I can't prove lemmas for FooToBar (FooVar x) case.

In general It can't be proved that FooVar x has a similar type or value to BarVar x.

I guess that FooToBar must be more complicated. It must involve also some kind of expression environment or variable mapping. Could you suggest a better signature for FooToBar? I think such a translator is a trivial thing, but I can't find any textbook describing it.

Answer 1

It's better to use inductive (relational) declarations instead of functional. Also one must add typing environments into transformation:

inductive foo_to_bar :: "foo_tenv ⇒ foo_exp ⇒ bar_tenv ⇒ bar_exp ⇒ bool"
  ("_ ⊢/ _ ↝/ _ ⊢/ _" 50) where
"Γ⇩F ⊢ FooBConst c ↝ Γ⇩B ⊢ BarBConst c" |
"Γ⇩F ⊢ init⇩F ↝ Γ⇩B ⊢ init⇩B ⟹
 Γ⇩F ⊢f init⇩F : τ⇩F⇩1 ⟹
 Γ⇩B ⊢b init⇩B : τ⇩B⇩1 ⟹
 Γ⇩F(var↦τ⇩F⇩1) ⊢ body⇩F ↝ Γ⇩B(var↦τ⇩B⇩1) ⊢ body⇩B ⟹
 Γ⇩F ⊢f FooLet var init⇩F body⇩F : τ⇩F ⟹
 Γ⇩B ⊢b BarLet var init⇩B body⇩B : τ⇩B ⟹
 τ⇩F ∼ τ⇩B ⟹
 Γ⇩F ⊢ FooLet var init⇩F body⇩F ↝ Γ⇩B ⊢ BarLet var init⇩B body⇩B" |
"Γ⇩F var = Some τ⇩F ⟹
 Γ⇩B var = Some τ⇩B ⟹
 τ⇩F ∼ τ⇩B ⟹
 Γ⇩F ⊢ FooVar var ↝ Γ⇩B ⊢ BarVar var" |
"Γ⇩F ⊢ a⇩F ↝ Γ⇩B ⊢ a⇩B ⟹
 Γ⇩F ⊢ b⇩F ↝ Γ⇩B ⊢ b⇩B ⟹
 Γ⇩F ⊢ FooAnd a⇩F b⇩F ↝ Γ⇩B ⊢ BarAnd a⇩B b⇩B"

inductive_cases [elim!]: "Γ⇩F ⊢ FooBConst c ↝ Γ⇩B ⊢ BarBConst c"
inductive_cases FooLetToBarE[elim!]: "Γ⇩F ⊢ FooLet var init⇩F body⇩F ↝ Γ⇩B ⊢ exp⇩B"
inductive_cases [elim!]: "Γ⇩F ⊢ FooVar var ↝ Γ⇩B ⊢ BarVar var"
inductive_cases [elim!]: "Γ⇩F ⊢ FooAnd a⇩F b⇩F ↝ Γ⇩B ⊢ exp⇩B"

lemma foo_to_bar_is_fun :
  "Γ⇩F ⊢ exp⇩F ↝ Γ⇩B ⊢ exp⇩B⇩1 ⟹
   Γ⇩F ⊢ exp⇩F ↝ Γ⇩B ⊢ exp⇩B⇩2 ⟹
   exp⇩B⇩1 = exp⇩B⇩2"
  apply (induct Γ⇩F exp⇩F Γ⇩B exp⇩B⇩1 arbitrary: exp⇩B⇩2 rule: foo_to_bar.induct)
  apply (erule foo_to_bar.cases; simp)
  apply (smt FooLetToBarE bar_typing_is_fun foo_typing_is_fun)
  apply (erule foo_to_bar.cases; simp)
  by blast

After that it's easy enough to prove type preservation:

lemma foo_to_bar_preserve_type:
  "Γ⇩F ⊢ exp⇩F ↝ Γ⇩B ⊢ exp⇩B ⟹
   Γ⇩F ⊢f exp⇩F : τ⇩F ⟹
   Γ⇩B ⊢b exp⇩B : τ⇩B ⟹
   τ⇩F ∼ τ⇩B"
  apply (induct Γ⇩F exp⇩F Γ⇩B exp⇩B arbitrary: τ⇩F τ⇩B rule: foo_to_bar.induct)
  using type_equiv.intros(1) apply blast
  using foo_typing_is_fun bar_typing_is_fun apply blast
  apply auto[1]
  by blast

And semantics preservation:

inductive_cases [elim!]:
  "FooBValue v⇩F ≈ BarBValue v⇩B"
  "FooIValue v⇩F ≈ BarIValue v⇩B"

lemma val_equiv_is_fun:
  "v⇩F ≈ v⇩B⇩1 ⟹ v⇩F ≈ v⇩B⇩2 ⟹ v⇩B⇩1 = v⇩B⇩2"
  using val_equiv.simps by auto

primrec foo_to_bar_val :: "foo_val ⇒ bar_val option" where
  "foo_to_bar_val (FooBValue v) = Some (BarBValue v)" |
  "foo_to_bar_val (FooIValue v) = Some (BarIValue v)"

lemma foo_to_bar_val_eq_value_equiv:
  "(foo_to_bar_val v⇩F = Some v⇩B) = (v⇩F ≈ v⇩B)"
  by (metis foo_to_bar_val.simps(1) foo_to_bar_val.simps(2) foo_val.exhaust option.inject val_equiv.simps)

definition foo_to_bar_env :: "foo_env ⇒ bar_env" where
  "foo_to_bar_env env ≡ map_comp foo_to_bar_val env"

value "foo_to_bar_env (Map.empty(''x''↦FooBValue True)) ''x''"

lemma foo_to_bar_val_distr:
  "v⇩F ≈ v⇩B ⟹
   foo_to_bar_env (env⇩F(var↦v⇩F)) = (foo_to_bar_env env⇩F)(var↦v⇩B)"
  by (auto simp: map_comp_def foo_to_bar_val_eq_value_equiv foo_to_bar_env_def)

lemma foo_to_bar_preserve_semantics:
  "Γ⇩F ⊢ exp⇩F ↝ Γ⇩B ⊢ exp⇩B ⟹
   (exp⇩F, env⇩F) ⇒f v⇩F ⟹
   (exp⇩B, foo_to_bar_env env⇩F) ⇒b v⇩B ⟹
   v⇩F ≈ v⇩B"
  apply (induct Γ⇩F exp⇩F Γ⇩B exp⇩B arbitrary: env⇩F v⇩F v⇩B rule: foo_to_bar.induct)
  using val_equiv.simps apply auto[1]
  using foo_to_bar_val_distr apply fastforce
  using foo_to_bar_val_eq_value_equiv foo_to_bar_env_def apply auto[1]
  using val_equiv.simps by blast