Theory Eval_Class

section ‹A type class for correspondence between HOL expressions and terms›

theory Eval_Class
imports
  "../Rewriting/Rewriting_Term"
  "../Utils/ML_Utils"
  Deriving.Derive_Manager
  "Dict_Construction.Dict_Construction"
begin

no_notation Mpat_Antiquot.mpaq_App (infixl ‹$$› 900)
hide_const (open) Strong_Term.wellformed
declare Strong_Term.wellformed_term_def[simp del]

class evaluate =
  fixes eval :: "rule fset ⇒ term ⇒ 'a ⇒ bool" (‹_/ ⊢/ (_ ≈/ _)› [50,0,50] 50)
  assumes eval_wellformed: "rs ⊢ t ≈ a ⟹ wellformed t"
begin

definition eval' :: "rule fset ⇒ term ⇒ 'a ⇒ bool" (‹_/ ⊢/ (_ ↓/ _)› [50,0,50] 50) where
"rs ⊢ t ↓ a ⟷ wellformed t ∧ (∃t'. rs ⊢ t ⟶* t' ∧ rs ⊢ t' ≈ a)"

lemma eval'I[intro]:
  assumes "wellformed t" "rs ⊢ t ⟶* t'" "rs ⊢ t' ≈ a"
  shows "rs ⊢ t ↓ a"
using assms unfolding eval'_def by auto

lemma eval'E[elim]:
  assumes "rs ⊢ t ↓ a"
  obtains t' where "wellformed t" "rs ⊢ t ⟶* t'" "rs ⊢ t' ≈ a"
using assms unfolding eval'_def by auto

lemma eval_trivI: "rs ⊢ t ≈ a ⟹ rs ⊢ t ↓ a"
by (auto dest: eval_wellformed)

lemma eval_compose:
  assumes "wellformed t" "rs ⊢ t ⟶* t'" "rs ⊢ t' ↓ a"
  shows "rs ⊢ t ↓ a"
proof -
  from ‹rs ⊢ t' ↓ a› obtain t'' where "rs ⊢ t' ⟶* t''" "rs ⊢ t'' ≈ a"
    by blast
  moreover hence "rs ⊢ t ⟶* t''"
    using assms by auto
  ultimately show "rs ⊢ t ↓ a"
    using assms by auto
qed

end

instantiation "fun" :: (evaluate, evaluate) evaluate begin

  definition eval_fun where
  "eval_fun rs t a ⟷ wellformed t ∧ (∀x t⇩x. rs ⊢ t⇩x ↓ x ⟶ rs ⊢ t $ t⇩x ↓ a x)"

  instance
    by standard (simp add: eval_fun_def)

end

corollary eval_funD:
  assumes "rs ⊢ t ≈ f" "rs ⊢ t⇩x ↓ x"
  shows "rs ⊢ t $ t⇩x ↓ f x"
using assms unfolding eval_fun_def by blast

corollary eval'_funD:
  assumes "rs ⊢ t ↓ f" "rs ⊢ t⇩x ↓ x"
  shows "rs ⊢ t $ t⇩x ↓ f x"
proof -
  from assms obtain t' where "rs ⊢ t ⟶* t'" "rs ⊢ t' ≈ f"
    by auto
  have "wellformed (t $ t⇩x)"
    using assms by auto
  moreover have "rs ⊢ t $ t⇩x ⟶* t' $ t⇩x"
    using ‹rs ⊢ t ⟶* t'› by (rule rewrite.rt_fun[unfolded app_term_def])
  moreover have "rs ⊢ t' $ t⇩x ↓ f x"
    using ‹rs ⊢ t' ≈ f› assms(2) by (rule eval_funD)
  ultimately show "rs ⊢ t $ t⇩x ↓ f x"
    by (rule eval_compose)
qed

lemma eval_ext:
  assumes "wellformed f" "⋀x t. rs ⊢ t ↓ x ⟹ rs ⊢ f $ t ↓ a x"
  shows "rs ⊢ f ≈ a"
using assms unfolding eval_fun_def by blast

lemma eval'_ext:
  assumes "wellformed f" "⋀x t. rs ⊢ t ↓ x ⟹ rs ⊢ f $ t ↓ a x"
  shows "rs ⊢ f ↓ a"
apply (rule eval'I[OF ‹wellformed f›])
apply (rule rtranclp.rtrancl_refl)
apply (rule eval_ext)
using assms by auto

lemma eval'_ext_alt:
  fixes f :: "'a::evaluate ⇒ 'b::evaluate"
  assumes "wellformed' 1 t" "⋀u x. rs ⊢ u ↓ x ⟹ rs ⊢ t [u]⇩β ↓ f x"
  shows "rs ⊢ Λ t ↓ f"
proof (rule eval'_ext)
  show "wellformed (Λ t)"
    using assms by simp
next
  fix x :: 'a and u
  assume "rs ⊢ u ↓ x"
  show "rs ⊢ Λ t $ u ↓ f x"
    proof (rule eval_compose)
      show "wellformed (Λ t $ u)"
        using assms ‹rs ⊢ u ↓ x› by auto
    next
      show "rs ⊢ Λ t $ u ⟶* t [u]⇩β"
        using ‹rs ⊢ u ↓ x› by (auto intro: rewrite.beta)
    next
      show "rs ⊢ t [u]⇩β ↓ f x"
        using assms ‹rs ⊢ u ↓ x› by auto
    qed
qed

lemma eval_impl_wellformed[dest]: "rs ⊢ t ≈ a ⟹ wellformed' n t"
by (auto dest: wellformed_inc eval_wellformed[unfolded wellformed_term_def])

lemma eval'_impl_wellformed[dest]: "rs ⊢ t ↓ a ⟹ wellformed' n t"
unfolding eval'_def by (auto dest: wellformed_inc)

lemma wellformed_unpack:
  "wellformed' n (t $ u) ⟹ wellformed' n t"
  "wellformed' n (t $ u) ⟹ wellformed' n u"
  "wellformed' n (Λ t) ⟹ wellformed' (Suc n) t"
by auto

lemma replace_bound_aux:
  "n < 0 ⟷ False"
  "Suc n < Suc m ⟷ n < m"
  "0 < Suc n ⟷ True"
  "((0::nat) = 0) ⟷ True"
  "(0 = Suc m) ⟷ False"
  "(Suc m = Suc n) ⟷ n = m"
  "(Suc m = 0) ⟷ False"
  "(if True then P else Q) = P"
  "(if False then P else Q) = Q"
  "int (0::nat) = 0"
by auto

named_theorems eval_data_intros
named_theorems eval_data_elims

context begin

(* for code generation, used in Tactics.code_tac *)
private definition rewrite_step_term :: "term × term ⇒ term ⇒ term option" where
"rewrite_step_term = rewrite_step"

private lemmas rewrite_rt_fun = rewrite.rt_fun[unfolded app_term_def]
private lemmas rewrite_rt_arg = rewrite.rt_arg[unfolded app_term_def]

ML_file "tactics.ML"

end

method_setup wellformed = ‹Scan.succeed (SIMPLE_METHOD' o Tactics.wellformed_tac)›

end