Theory Sorted_Algebra

(*
Author:  Sebastiaan Joosten (2016-2017)
Author:  René Thiemann (2016-2017)
Author:  Akihisa Yamada (2016-2018)
License: LGPL (see file COPYING.LESSER)
*)
theory Sorted_Algebra
imports 
  F_Algebra
begin

type_synonym ('f,'v,'t) exp = "('f,'v ×'t) term"

consts rename_vars :: "('a ⇒ 'b) ⇒ 'c ⇒ 'd"

definition rename_vars_exp :: "('v ⇒ 'w) ⇒ ('f,'v,'t) exp ⇒ ('f,'w,'t) exp" where
  "rename_vars_exp r = map_term id (map_prod r id)"

adhoc_overloading rename_vars rename_vars_exp

lemma rename_vars_exp_simps[simp]:
  "rename_vars_exp r (Var (x,ty)) = Var (r x, ty)"
  "rename_vars_exp r (Fun f ts) = Fun f (map (rename_vars_exp r) ts)"
  by (auto simp: rename_vars_exp_def)

lemma rename_vars_exp_comp[simp]:
  "rename_vars f (rename_vars g (t::(_,_,_) exp)) = rename_vars (f ∘ g) t"
   by (induct t, auto)

lemma vars_term_rename_vars[simp]: "vars_term (rename_vars f t) = map_prod f id ` vars_term t" by (induct t, auto)

lemma rename_vars_exp_id[THEN ext, simp]: "rename_vars id (t :: ('f,'v,'t) exp) = t"
proof (induct t)
  case (Var x)
  then show ?case by (cases x, auto)
next
  case (Fun f ts)
  then show ?case by (auto intro: map_idI)
qed


locale pre_sorted_algebra = algebra I
  for I :: "'f ⇒ 'a list ⇒ 'a"
  and type_of_fun :: "'f ⇒ 't list × 't"
  and Values_of_type :: "'t ⇒ 'a set"
  and type_fixer :: "('f×'t×'a) itself" (* Is this a good solution? *)
begin

abbreviation type_of_var :: "'v × 't ⇒ 't" where "type_of_var ≡ snd"

definition "assignment α ≡ ∀x. α x ∈ Values_of_type (type_of_var x)"

abbreviation return_type where "return_type f ≡ snd (type_of_fun f)"
abbreviation param_types where "param_types f ≡ fst (type_of_fun f)"

lemma assignmentI[intro]:
  assumes "⋀x t. α (x,t) ∈ Values_of_type t" shows "assignment α"
  using assms by (auto simp: assignment_def)

lemma assignmentD[dest]:
  assumes "assignment α" shows "⋀x. α x ∈ Values_of_type (type_of_var x)" using assms by (auto simp: assignment_def)

lemma assignmentE[elim]:
  assumes "assignment α" and "(⋀x. α x ∈ Values_of_type (type_of_var x)) ⟹ thesis" shows thesis
  using assms by (auto simp: assignment_def)

fun has_type (infix ":⇩f" 60) where
  "Var v :⇩f ty ⟷ type_of_var v = ty"
| "Fun f es :⇩f ty ⟷
  (ty = return_type f ∧ length es = length (param_types f) ∧ (∀i < length es. es ! i :⇩f param_types f ! i))"

notation has_type (infix ":⇩f" 60)

abbreviation "expression e ≡ ∃ty. e :⇩f ty"

lemma map_term_has_type:
  assumes "⋀x. x ∈ vars_term e ⟹ type_of_var (r x) = type_of_var x"
      and "⋀f. f ∈ funs_term e ⟹ type_of_fun (rf f) = type_of_fun f"
  shows "map_term rf r e :⇩f ty ⟷ e :⇩f ty"
proof-
  { fix X F
    assume X: "⋀x. x ∈ X ⟹ type_of_var (r x) = type_of_var x"
       and F: "⋀f. f ∈ F ⟹ type_of_fun (rf f) = type_of_fun f"
    have "vars_term e ⊆ X ⟹ funs_term e ⊆ F ⟹ ?thesis"
    proof (induct e arbitrary: ty)
      case (Var x)
      then show ?case using X by auto
    next
      case (Fun f es)
      show ?case
      proof (cases "type_of_fun f")
        case (Pair tys ty')
        moreover {
          fix i assume i: "i < length es" "length es = length tys"
          from Fun X F have "e ∈ set es ⟹ vars_term e ⊆ X ∧ funs_term e ⊆ F" for e by auto
          with i have "vars_term (es!i) ⊆ X" "funs_term (es!i) ⊆ F" by auto
          with Fun(1)[OF _ this, of "tys!i"] i Pair Fun
          have "map_term rf r (es ! i) :⇩f tys ! i = es ! i :⇩f tys ! i" by auto
        }
        moreover from Fun F have "type_of_fun (rf f) = type_of_fun f" by auto
        ultimately show ?thesis by auto
      qed
    qed
  }
  from this[OF assms] show ?thesis by auto
qed

lemma rename_vars_has_type[simp]: "rename_vars r e :⇩f ty ⟷ e :⇩f ty"
  by (unfold rename_vars_exp_def, intro map_term_has_type, auto)

context
  fixes α :: "'v × 't ⇒ 'a" and β :: "'w × 't ⇒ 'a" and r :: "'v ⇒ 'w"
  assumes r: "⋀ x t. α (x,t) = β (r x, t)"
begin

lemma eval_rename_vars: "⟦rename_vars r a⟧ β = ⟦a⟧ α"
proof (induct a)
  case (Var x)
  show ?case by (cases x, auto simp: rename_vars_exp_def r)
next
  case (Fun f ts)
  then show ?case by (auto intro: arg_cong[of _ _ "I f"])
qed

lemma assignment_rename_vars: "assignment β ⟹ assignment α"
  unfolding assignment_def using r by auto

end

end

locale sorted_algebra = pre_sorted_algebra + 
  assumes well_typed:
    "⋀f ds. length ds = length (param_types f) ⟹
     (⋀i. i < length ds ⟹ ds!i ∈ Values_of_type (param_types f ! i)) ⟹ I f ds ∈ Values_of_type (return_type f)"
  and consistent: "⋀ty. Values_of_type ty ≠ {}"
begin

lemma eval_types:
  assumes "assignment α" and "x :⇩f ty" shows "⟦x⟧ α ∈ Values_of_type ty"
  using assms by (induct x arbitrary: ty, insert well_typed, auto)

end

end