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.
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