Theory Indexed_Term

section ‹Indexed Terms›

text ‹We provide a method to index all subterms of a term by numbers.›

theory Indexed_Term
  imports 
    First_Order_Terms.Subterm_and_Context
begin

type_synonym index = int
type_synonym ('f, 'v) indexed_term = "(('f × ('f,'v)term × index), ('v × ('f,'v)term × index)) term"

fun index_term_aux :: "index ⇒ ('f, 'v) term ⇒ index × ('f, 'v) indexed_term"
  and index_term_aux_list :: "index ⇒ ('f, 'v) term list ⇒ index × ('f, 'v) indexed_term list"
  where
    "index_term_aux i (Var v) = (i + 1, Var (v,Var v, i))"
  | "index_term_aux i (Fun f ts) = (case index_term_aux_list i ts of (j, ss) ⇒ (j + 1, Fun (f,Fun f ts,j) ss))" 
  | "index_term_aux_list i [] = (i,[])" 
  | "index_term_aux_list i (t # ts) = (case index_term_aux i t of (j,s) ⇒ map_prod id (Cons s) (index_term_aux_list j ts))"


definition index_term :: "('f, 'v) term ⇒ ('f, 'v) indexed_term"
  where
    "index_term t = snd (index_term_aux 0 t)" 

fun unindex :: "('f, 'v) indexed_term ⇒ ('f, 'v) term"
  where
    "unindex (Var (v,_)) = Var v"
  | "unindex (Fun (f,_) ts) = Fun f (map unindex ts)"

fun stored :: "('f, 'v) indexed_term ⇒ ('f, 'v) term"
  where
    "stored (Var (v,(s,_))) = s"
  | "stored (Fun (f,(s,_)) ts) = s"

fun name_of :: "('a × 'b) ⇒ 'a"
  where
    "name_of (a,_) = a"

fun index :: "('f, 'v) indexed_term ⇒ index"
  where
    "index (Var (_,(_,i))) = i"
  | "index (Fun (_,(_,i)) _) = i"

definition "index_term_prop f s = (∀ u. s ⊵ u ⟶ f (index u) = Some (unindex u) ∧ stored u = unindex u)" 

lemma index_term_aux: fixes t :: "('f,'v)term" and ts :: "('f,'v)term list"
  shows "index_term_aux i t = (j,s) ⟹ unindex s = t ∧ i < j ∧ (∃ f. dom f = {i ..< j} ∧ index_term_prop f s)" 
    and "index_term_aux_list i ts = (j,ss) ⟹ map unindex ss = ts ∧ i ≤ j ∧
    (∃ f. dom f = {i ..< j} ∧ Ball (set ss) (index_term_prop f))" 
proof (induct i t and i ts arbitrary: j s and j ss rule: index_term_aux_index_term_aux_list.induct)
  case (1 i v)
  then show ?case by (auto intro!: exI[of _ "(λ _. None)(i := Some (Var v))"] split: if_splits simp: index_term_prop_def supteq_var_imp_eq) 
next
  case (2 i g ts j s)
  obtain k ss where rec: "index_term_aux_list i ts = (k,ss)" by force
  from 2(2)[unfolded index_term_aux.simps rec split]
  have j: "j = k + 1" and s: "s = Fun (g, Fun g ts, k) ss" by auto
  from 2(1)[OF rec] obtain f where fss: "map unindex ss = ts" and
    ik: "i ≤ k" and f: "dom f = {i..<k}" "⋀ s. s ∈ set ss ⟹ index_term_prop f s" 
    by auto
  have set: "{i..< k + 1} = insert k {i..<k}" using ik by auto
  define h where "h = f(k := Some (Fun g ts))" 
  show ?case unfolding s unindex.simps fss j set index_term_prop_def
  proof (intro conjI exI[of _ h] refl allI)
    show "i < k + 1" using ik by simp
    show "dom h = insert k {i..<k}" using ik f(1) unfolding h_def by auto
    fix u
    show "Fun (g, Fun g ts, k) ss ⊵ u ⟶ h (index u) = Some (unindex u) ∧ stored u = unindex u" 
    proof (cases "u = Fun (g, Fun g ts, k) ss")
      case True
      thus ?thesis by (auto simp: fss h_def index_term_prop_def)
    next
      case False
      show ?thesis
      proof (intro impI)
        assume "Fun (g, Fun g ts, k) ss ⊵ u" 
        with False obtain si where "si ∈ set ss" and "si ⊵ u"
          by (metis Fun_supt suptI)
        from f(2)[unfolded index_term_prop_def, rule_format, OF this] f(1) ik 
        show "h (index u) = Some (unindex u) ∧ stored u = unindex u" unfolding h_def by auto
      qed
    qed
  qed
next
  case (4 i t ts j sss)
  obtain k s where rec1: "index_term_aux i t = (k,s)" by force
  with 4(3) obtain ss where rec2: "index_term_aux_list k ts = (j,ss)" and sss: "sss = s # ss" 
    by (cases "index_term_aux_list k ts", auto)
  from 4(1)[OF rec1] obtain f where fs: "unindex s = t" and ik: "i < k" and f: "dom f = {i..<k}" 
    "index_term_prop f s" by auto
  from 4(2)[unfolded rec1, OF refl rec2] obtain g where fss: "map unindex ss = ts" and kj: "k ≤ j" 
    and g: "dom g = {k..<j}" "⋀ si. si ∈ set ss ⟹ index_term_prop g si"  
    by auto
  define h where "h = (λ n. if n ∈ {i..<k} then f n else g n)" 
  show ?case unfolding sss list.simps fs fss
  proof (intro conjI exI[of _ h] refl allI ballI)
    have "dom h = {i ..< k} ∪ {k ..< j}" unfolding h_def using f(1) g(1) by force
    also have "… = {i ..< j}" using ik kj by auto
    finally show "dom h = {i..<j}" by auto
    show "i ≤ j" using ik kj by auto
    fix si
    assume si: "si ∈ insert s (set ss)"
    show "index_term_prop h si"
    proof (cases "si = s")
      case True
      from f show ?thesis unfolding True h_def index_term_prop_def by auto
    next
      case False
      with si have si: "si ∈ set ss" by auto
      have disj: "{i..<k} ∩ {k..<j} = {}" by auto
      from g(1) g(2)[OF si]
      show ?thesis unfolding index_term_prop_def h_def using disj
        by (metis disjoint_iff domI)
    qed
  qed
qed auto


lemma index_term_index_unindex: "∃ f. ∀ t. index_term s ⊵ t ⟶ f (index t) = unindex t ∧ stored t = unindex t" 
proof -
  obtain t i where aux: "index_term_aux 0 s = (i,t)" by force
  from index_term_aux(1)[OF this] show ?thesis unfolding index_term_def aux index_term_prop_def by force
qed

lemma unindex_index_term[simp]: "unindex (index_term s) = s"
proof -
  obtain t i where aux: "index_term_aux 0 s = (i,t)" by force
  from index_term_aux(1)[OF this] show ?thesis unfolding index_term_def aux by force
qed

end