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_decl
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' (t1 $ t2) (u1 $ u2)  non_overlapping' t1 u1  non_overlapping' t2 u2" |
"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' (t1 $ t2) (u1 $ u2)  pattern_compatible' t1 u1  (t1 = u1  pattern_compatible' t2 u2)" |
"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 (λ(lhs1, _) (lhs2, _). pattern_compatible' lhs1 lhs2)"

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" ("_")

setuplet
    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