Theory Embed

section ‹Deep embedding of Pure terms into term-rewriting logic›

theory Embed
imports
  Constructor_Funs.Constructor_Funs
  "../Utils/Code_Utils"
  Eval_Class
keywords "embed" :: thy_goal
begin

fun non_overlapping' :: "term ⇒ term ⇒ bool" where
"non_overlapping' (Const x) (Const y) ⟷ x ≠ y" |
"non_overlapping' (Const _) (_ $ _) ⟷ True" |
"non_overlapping' (_ $ _) (Const _) ⟷ True" |
"non_overlapping' (t⇩1 $ t⇩2) (u⇩1 $ u⇩2) ⟷ non_overlapping' t⇩1 u⇩1 ∨ non_overlapping' t⇩2 u⇩2" |
"non_overlapping' _ _ ⟷ False"

lemma non_overlapping_approx:
  assumes "non_overlapping' t u"
  shows "non_overlapping t u"
using assms
by (induct t u rule: non_overlapping'.induct) fastforce+

fun pattern_compatible' :: "term ⇒ term ⇒ bool" where
"pattern_compatible' (t⇩1 $ t⇩2) (u⇩1 $ u⇩2) ⟷ pattern_compatible' t⇩1 u⇩1 ∧ (t⇩1 = u⇩1 ⟶ pattern_compatible' t⇩2 u⇩2)" |
"pattern_compatible' t u ⟷ t = u ∨ non_overlapping' t u"

lemma pattern_compatible_approx:
  assumes "pattern_compatible' t u"
  shows "pattern_compatible t u"
using assms
proof (induction t u rule: pattern_compatible.induct)
  case "2_1" (* FIXME intro rule setup for non_overlapping is broken *)
  thus ?case
    by (force simp: non_overlapping_approx)
next
  case "2_5"
  thus ?case
    by (force simp: non_overlapping_approx)
qed auto

abbreviation pattern_compatibles' :: "(term × 'a) fset ⇒ bool" where
"pattern_compatibles' ≡ fpairwise (λ(lhs⇩1, _) (lhs⇩2, _). pattern_compatible' lhs⇩1 lhs⇩2)"

definition rules' :: "C_info ⇒ rule fset ⇒ bool" where
"rules' C_info rs ⟷
  fBall rs rule ∧
  arity_compatibles rs ∧
  is_fmap rs ∧
  pattern_compatibles' rs ∧
  rs ≠ {||} ∧
  fBall rs (λ(lhs, _). ¬ pre_constants.shadows_consts C_info (heads_of rs) lhs) ∧
  fdisjnt (heads_of rs) (constructors.C C_info) ∧
  fBall rs (λ(_, rhs). pre_constants.welldefined C_info (heads_of rs) rhs) ∧
  distinct (constructors.all_constructors C_info)"

lemma rules_approx:
  assumes "rules' C_info rs"
  shows "rules C_info rs"
proof
  show "fBall rs rule" "arity_compatibles rs" "is_fmap rs" "rs ≠ {||}"
   and "fBall rs (λ(lhs, _). ¬ pre_constants.shadows_consts C_info (heads_of rs) lhs)"
   and "fBall rs (λ(_, rhs). pre_constants.welldefined C_info (heads_of rs) rhs)"
   and "fdisjnt (heads_of rs) (constructors.C C_info)"
   and "distinct (constructors.all_constructors C_info)"
    using assms unfolding rules'_def by simp+
next
  have "pattern_compatibles' rs"
    using assms unfolding rules'_def by simp
  thus "pattern_compatibles rs"
    by (rule fpairwise_weaken) (blast intro: pattern_compatible_approx)
qed

lemma embed_ext: "f ≡ g ⟹ f x ≡ g x"
by auto

ML_file "embed.ML"

consts "lift_term" :: "'a ⇒ term" (‹⟨_⟩›)

setup‹
  let
    fun embed ((Const (@{const_name lift_term}, _)) $ t) = HOL_Term.mk_term false t
      | embed (t $ u) = embed t $ embed u
      | embed t = t
  in Context.theory_map (Syntax_Phases.term_check 99 "lift" (K (map embed))) end
›

end