Theory Messages

(*  Title:      Messages.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Protocol Messages as (First-Order) Terms›

theory Messages
  imports Miscellaneous "First_Order_Terms.Term"
begin

subsection ‹Term-related definitions: subterms and free variables›
abbreviation "the_Fun  un_Fun1"
lemmas the_Fun_def = un_Fun1_def

fun subterms::"('a,'b) term  ('a,'b) terms" where
  "subterms (Var x) = {Var x}"
| "subterms (Fun f T) = {Fun f T}  (t  set T. subterms t)"

abbreviation subtermeq (infix "" 50) where "t'  t  (t'  subterms t)"
abbreviation subterm (infix "" 50) where "t'  t  (t'  t  t'  t)"

abbreviation "subtermsset M  (subterms ` M)"
abbreviation subtermeqset (infix "set" 50) where "t set M  (t  subtermsset M)"

abbreviation fv where "fv  vars_term"
lemmas fv_simps = term.simps(17,18)

fun fvset where "fvset M = (fv ` M)"

abbreviation fvpair where "fvpair p  case p of (t,t')  fv t  fv t'"

fun fvpairs where "fvpairs F = (fvpair ` set F)"

abbreviation ground where "ground M  fvset M = {}"


subsection ‹Variants that return lists insteads of sets›
fun fv_list where
  "fv_list (Var x) = [x]"
| "fv_list (Fun f T) = concat (map fv_list T)"

definition fv_listpairs where
  "fv_listpairs F  concat (map (λ(t,t'). fv_list t@fv_list t') F)"

fun subterms_list::"('a,'b) term  ('a,'b) term list" where
  "subterms_list (Var x) = [Var x]"
| "subterms_list (Fun f T) = remdups (Fun f T#concat (map subterms_list T))"

lemma fv_list_is_fv: "fv t = set (fv_list t)"
by (induct t) auto

lemma fv_listpairs_is_fvpairs: "fvpairs F = set (fv_listpairs F)"
by (induct F) (auto simp add: fv_list_is_fv fv_listpairs_def)

lemma subterms_list_is_subterms: "subterms t = set (subterms_list t)"
by (induct t) auto


subsection ‹The subterm relation defined as a function›
fun subterm_of where
  "subterm_of t (Var y) = (t = Var y)"
| "subterm_of t (Fun f T) = (t = Fun f T  list_ex (subterm_of t) T)"

lemma subterm_of_iff_subtermeq[code_unfold]: "t  t' = subterm_of t t'"
proof (induction t')
  case (Fun f T) thus ?case
  proof (cases "t = Fun f T")
    case False thus ?thesis
      using Fun.IH subterm_of.simps(2)[of t f T]
      unfolding list_ex_iff by fastforce
  qed simp
qed simp

lemma subterm_of_ex_set_iff_subtermeqset[code_unfold]: "t set M = (t'  M. subterm_of t t')"
using subterm_of_iff_subtermeq by blast


subsection ‹The subterm relation is a partial order on terms›
interpretation "term": order "(⊑)" "(⊏)"
proof
  show "s  s" for s :: "('a,'b) term"
    by (induct s rule: subterms.induct) auto

  show trans: "s  t  t  u  s  u" for s t u :: "('a,'b) term"
    by (induct u rule: subterms.induct) auto

  show "s  t  t  s  s = t" for s t :: "('a,'b) term"
  proof (induction s arbitrary: t rule: subterms.induct[case_names Var Fun])
    case (Fun f T)
    { assume 0: "t  Fun f T"
      then obtain u::"('a,'b) term" where u: "u  set T" "t  u" using Fun.prems(2) by auto
      hence 1: "Fun f T  u" using trans[OF Fun.prems(1)] by simp
   
      have 2: "u  Fun f T"
        by (cases u) (use u(1) in force, use u(1) subterms.simps(2)[of f T] in fastforce)
      hence 3: "u = Fun f T" using Fun.IH[OF u(1) _ 1] by simp

      have "u  t" using trans[OF 2 Fun.prems(1)] by simp
      hence 4: "u = t" using Fun.IH[OF u(1) _ u(2)] by simp
  
      have "t = Fun f T" using 3 4 by simp
      hence False using 0 by simp
    }
    thus ?case by auto
  qed simp
  thus "(s  t) = (s  t  ¬(t  s))" for s t :: "('a,'b) term"
    by blast
qed


subsection ‹Lemmata concerning subterms and free variables›
lemma fv_listpairs_append: "fv_listpairs (F@G) = fv_listpairs F@fv_listpairs G"
by (simp add: fv_listpairs_def)

lemma distinct_fv_list_idx_fv_disjoint:
  assumes t: "distinct (fv_list t)" "Fun f T  t"
    and ij: "i < length T" "j < length T" "i < j"
  shows "fv (T ! i)  fv (T ! j) = {}"
using t
proof (induction t rule: fv_list.induct)
  case (2 g S)
  have "distinct (fv_list s)" when s: "s  set S" for s
    by (metis (no_types, lifting) s "2.prems"(1) concat_append distinct_append 
          map_append split_list fv_list.simps(2) concat.simps(2) list.simps(9))
  hence IH: "fv (T ! i)  fv (T ! j) = {}"
    when s: "s  set S" "Fun f T  s" for s
    using "2.IH" s by blast

  show ?case
  proof (cases "Fun f T = Fun g S")
    case True
    define U where "U  map fv_list T"

    have a: "distinct (concat U)"
      using "2.prems"(1) True unfolding U_def by auto
    
    have b: "i < length U" "j < length U"
      using ij(1,2) unfolding U_def by simp_all

    show ?thesis
      using b distinct_concat_idx_disjoint[OF a b ij(3)]
            fv_list_is_fv[of "T ! i"] fv_list_is_fv[of "T ! j"]
      unfolding U_def by force
  qed (use IH "2.prems"(2) in auto)
qed force

lemma distinct_fv_list_Fun_param:
  assumes f: "distinct (fv_list (Fun f ts))"
    and t: "t  set ts"
  shows "distinct (fv_list t)"
proof -
  obtain pre suf where "ts = pre@t#suf" using t by (meson split_list)
  thus ?thesis using distinct_append f by simp
qed

lemmas subtermeqI'[intro] = term.eq_refl

lemma subtermeqI''[intro]: "t  set T  t  Fun f T"
by force

lemma finite_fv_set[intro]: "finite M  finite (fvset M)"
by auto

lemma finite_fun_symbols[simp]: "finite (funs_term t)"
by (induct t) simp_all

lemma fv_set_mono: "M  N  fvset M  fvset N"
by auto

lemma subtermsset_mono: "M  N  subtermsset M  subtermsset N"
by auto

lemma ground_empty[simp]: "ground {}"
by simp

lemma ground_subset: "M  N  ground N  ground M"
by auto

lemma fv_map_fv_set: "(set (map fv L)) = fvset (set L)"
by (induct L) auto

lemma fvset_union: "fvset (M  N) = fvset M  fvset N"
by auto

lemma finite_subset_Union:
  fixes A::"'a set" and f::"'a  'b set"
  assumes "finite (a  A. f a)"
  shows "B. finite B  B  A  (b  B. f b) = (a  A. f a)"
by (metis assms eq_iff finite_subset_image finite_UnionD)

lemma inv_set_fv: "finite M  (set (map fv (inv set M))) = fvset M"
using fv_map_fv_set[of "inv set M"] inv_set_fset by auto

lemma ground_subterm: "fv t = {}  t'  t  fv t' = {}" by (induct t) auto

lemma empty_fv_not_var: "fv t = {}  t  Var x" by auto

lemma empty_fv_exists_fun: "fv t = {}  f X. t = Fun f X" by (cases t) auto

lemma vars_iff_subtermeq: "x  fv t  Var x  t" by (induct t) auto

lemma vars_iff_subtermeq_set: "x  fvset M  Var x  subtermsset M"
using vars_iff_subtermeq[of x] by auto

lemma vars_if_subtermeq_set: "Var x  subtermsset M  x  fvset M"
by (metis vars_iff_subtermeq_set)

lemma subtermeq_set_if_vars: "x  fvset M  Var x  subtermsset M"
by (metis vars_iff_subtermeq_set)

lemma vars_iff_subterm_or_eq: "x  fv t  Var x  t  Var x = t"
by (induct t) (auto simp add: vars_iff_subtermeq)

lemma var_is_subterm: "x  fv t  Var x  subterms t"
by (simp add: vars_iff_subtermeq)

lemma subterm_is_var: "Var x  subterms t  x  fv t"
by (simp add: vars_iff_subtermeq)

lemma no_var_subterm: "¬t  Var v" by auto

lemma fun_if_subterm: "t  u  f X. u = Fun f X" by (induct u) simp_all

lemma subtermeq_vars_subset: "M  N  fv M  fv N" by (induct N) auto

lemma fv_subterms[simp]: "fvset (subterms t) = fv t"
by (induct t) auto

lemma fv_subterms_set[simp]: "fvset (subtermsset M) = fvset M"
using subtermeq_vars_subset by auto

lemma fv_subset: "t  M  fv t  fvset M"
by auto

lemma fv_subset_subterms: "t  subtermsset M  fv t  fvset M"
using fv_subset fv_subterms_set by metis

lemma subterms_finite[simp]: "finite (subterms t)" by (induction rule: subterms.induct) auto

lemma subterms_union_finite: "finite M  finite (t  M. subterms t)"
by (induction rule: subterms.induct) auto

lemma subterms_subset: "t'  t  subterms t'  subterms t"
by (induction rule: subterms.induct) auto

lemma subterms_subset_set: "M  subterms t  subtermsset M  subterms t"
by (metis SUP_least contra_subsetD subterms_subset)

lemma subset_subterms_Union[simp]: "M  subtermsset M" by auto

lemma in_subterms_Union: "t  M  t  subtermsset M" using subset_subterms_Union by blast

lemma in_subterms_subset_Union: "t  subtermsset M  subterms t  subtermsset M"
using subterms_subset by auto

lemma subterm_param_split: 
  assumes "t  Fun f X"
  shows "pre x suf. t  x  X = pre@x#suf"
proof -
  obtain x where "t  x" "x  set X" using assms by auto
  then obtain pre suf where "X = pre@x#suf" "x  set pre  x  set suf"
    by (meson split_list_first split_list_last)
  thus ?thesis using t  x by auto
qed

lemma ground_iff_no_vars: "ground (M::('a,'b) terms)  (v. Var v  (m  M. subterms m))"
proof
  assume "ground M"
  hence "v. m  M. v  fv m" by auto
  hence "v. m  M. Var v  subterms m" by (simp add: vars_iff_subtermeq)
  thus "(v. Var v  (m  M. subterms m))" by simp
next
  assume no_vars: "v. Var v  (m  M. subterms m)"
  moreover
  { assume "¬ground M"
    then obtain v and m::"('a,'b) term" where "m  M" "fv m  {}" "v  fv m" by auto
    hence "Var v  (subterms m)" by (simp add: vars_iff_subtermeq)
    hence "v. Var v  (t  M. subterms t)" using m  M by auto
    hence False using no_vars by simp
  }
  ultimately show "ground M" by blast
qed

lemma index_Fun_subterms_subset[simp]: "i < length T  subterms (T ! i)  subterms (Fun f T)"
by auto

lemma index_Fun_fv_subset[simp]: "i < length T  fv (T ! i)  fv (Fun f T)"
using subtermeq_vars_subset by fastforce

lemma subterms_union_ground:
  assumes "ground M"
  shows "ground (subtermsset M)"
proof -
  { fix t assume "t  M"
    hence "fv t = {}"
      using ground_iff_no_vars[of M] assms
      by auto
    hence "t'  subterms t. fv t' = {}" using subtermeq_vars_subset[of _ t] by simp
    hence "ground (subterms t)" by auto
  }
  thus ?thesis by auto
qed

lemma Var_subtermeq: "t  Var v  t = Var v" by simp

lemma subtermeq_imp_funs_term_subset: "s  t  funs_term s  funs_term t"
by (induct t arbitrary: s) auto

lemma subterms_const: "subterms (Fun f []) = {Fun f []}" by simp

lemma subterm_subtermeq_neq: "t  u; u  v  t  v"
  using term.dual_order.strict_trans1 by blast 

lemma subtermeq_subterm_neq: "t  u; u  v  t  v"
by (metis term.order.eq_iff)

lemma subterm_size_lt: "x  y  size x < size y"
using not_less_eq size_list_estimation by (induct y, simp, fastforce)

lemma in_subterms_eq: "x  subterms y; y  subterms x  subterms x = subterms y"
  using term.order.antisym by auto

lemma Fun_param_size_lt:
  "t  set ts  size t < size (Fun f ts)"
by (induct ts) auto

lemma Fun_zip_size_lt:
  assumes "(t,s)  set (zip ts ss)"
  shows "size t < size (Fun f ts)"
    and "size s < size (Fun g ss)"
by (metis assms Fun_param_size_lt in_set_zipE)+

lemma Fun_gt_params: "Fun f X  (x  set X. subterms x)"
proof -
  have "size_list size X < size (Fun f X)" by simp
  hence "Fun f X  set X" by (meson less_not_refl size_list_estimation) 
  hence "x  set X. Fun f X  subterms x  x  subterms (Fun f X)"
    using subtermeq_subterm_neq by blast 
  moreover have "x  set X. x  subterms (Fun f X)" by fastforce
  ultimately show ?thesis by auto
qed

lemma params_subterms[simp]: "set X  subterms (Fun f X)" by auto

lemma params_subterms_Union[simp]: "subtermsset (set X)  subterms (Fun f X)" by auto

lemma Fun_subterm_inside_params: "t  Fun f X  t  (x  (set X). subterms x)"
using Fun_gt_params by fastforce

lemma Fun_param_is_subterm: "x  set X  x  Fun f X"
using Fun_subterm_inside_params by fastforce

lemma Fun_param_in_subterms: "x  set X  x  subterms (Fun f X)"
using Fun_subterm_inside_params by fastforce

lemma Fun_not_in_param: "x  set X  ¬Fun f X  x"
  by (meson Fun_param_in_subterms term.less_le_not_le) 

lemma Fun_ex_if_subterm: "t  s  f T. Fun f T  s  t  set T"
proof (induction s)
  case (Fun f T)
  then obtain s' where s': "s'  set T" "t  s'" by auto
  show ?case
  proof (cases "t = s'")
    case True thus ?thesis using s' by blast
  next
    case False
    thus ?thesis
      using Fun.IH[OF s'(1)] s'(2) term.order_trans[OF _ Fun_param_in_subterms[OF s'(1), of f]]
      by metis
  qed
qed simp

lemma const_subterm_obtain:
  assumes "fv t = {}"
  obtains c where "Fun c []  t"
using assms
proof (induction t)
  case (Fun f T) thus ?case by (cases "T = []") force+
qed simp

lemma const_subterm_obtain': "fv t = {}  c. Fun c []  t"
by (metis const_subterm_obtain)

lemma subterms_singleton:
  assumes "(v. t = Var v)  (f. t = Fun f [])"
  shows "subterms t = {t}"
using assms by (cases t) auto

lemma subtermeq_Var_const:
  assumes "s  t"
  shows "t = Var v  s = Var v" "t = Fun f []  s = Fun f []"
using assms by fastforce+

lemma subterms_singleton':
  assumes "subterms t = {t}"
  shows "(v. t = Var v)  (f. t = Fun f [])"
proof (cases t)
  case (Fun f T)
  { fix s S assume "T = s#S"
    hence "s  subterms t" using Fun by auto
    hence "s = t" using assms by auto
    hence False
      using Fun_param_is_subterm[of s "s#S" f] T = s#S Fun
      by auto
  }
  hence "T = []" by (cases T) auto
  thus ?thesis using Fun by simp
qed (simp add: assms)

lemma funs_term_subterms_eq[simp]:
  "(s  subterms t. funs_term s) = funs_term t" 
  "(s  subtermsset M. funs_term s) = (funs_term ` M)"
proof -
  show "t. (funs_term ` subterms t) = funs_term t"
    using term.order_refl subtermeq_imp_funs_term_subset by blast
  thus "(funs_term ` (subtermsset M)) = (funs_term ` M)" by force
qed

lemmas subtermI'[intro] = Fun_param_is_subterm

lemma funs_term_Fun_subterm: "f  funs_term t  T. Fun f T  subterms t"
proof (induction t)
  case (Fun g T)
  hence "f = g  (s  set T. f  funs_term s)" by simp
  thus ?case
  proof
    assume "s  set T. f  funs_term s"
    then obtain s where "s  set T" "T. Fun f T  subterms s" using Fun.IH by auto
    thus ?thesis by auto
  qed (auto simp add: Fun)
qed simp

lemma funs_term_Fun_subterm': "Fun f T  subterms t  f  funs_term t"
by (induct t) auto

lemma zip_arg_subterm:
  assumes "(s,t)  set (zip X Y)"
  shows "s  Fun f X" "t  Fun g Y"
proof -
  from assms have *: "s  set X" "t  set Y" by (meson in_set_zipE)+
  show "s  Fun f X" by (metis Fun_param_is_subterm[OF *(1)])
  show "t  Fun g Y" by (metis Fun_param_is_subterm[OF *(2)])
qed

lemma fv_disj_Fun_subterm_param_cases:
  assumes "fv t  X = {}" "Fun f T  subterms t"
  shows "T = []  (sset T. s  Var ` X)"
proof (cases T)
  case (Cons s S)
  hence "s  subterms t"
    using assms(2) term.order_trans[of _ "Fun f T" t]
    by auto
  hence "fv s  X = {}" using assms(1) fv_subterms by force
  thus ?thesis using Cons by auto
qed simp

lemma fv_eq_FunI:
  assumes "length T = length S" "i. i < length T  fv (T ! i) = fv (S ! i)"
  shows "fv (Fun f T) = fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  have "fv (T ! i) = fv (S ! i)" when "i < length T" for i
    using that Cons.prems(2)[of "Suc i"] unfolding S' by simp
  hence "fv (Fun f T) = fv (Fun g S)"
    using Cons.prems(1) Cons.IH[of S] unfolding S' by simp
  thus ?case using Cons.prems(2)[of 0] unfolding S' by auto
qed simp

lemma fv_eq_FunI':
  assumes "length T = length S" "i. i < length T  x  fv (T ! i)  x  fv (S ! i)"
  shows "x  fv (Fun f T)  x  fv (Fun g S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  show ?case using Cons.prems Cons.IH[of S] unfolding S' by fastforce
qed simp

lemma funs_term_eq_FunI:
  assumes "length T = length S" "i. i < length T  funs_term (T ! i) = funs_term (S ! i)"
  shows "funs_term (Fun f T) = funs_term (Fun f S)"
using assms
proof (induction T arbitrary: S)
  case (Cons t T S')
  then obtain s S where S': "S' = s#S" by (cases S') simp_all
  have "funs_term (T ! i) = funs_term (S ! i)" when "i < length T" for i
    using that Cons.prems(2)[of "Suc i"] unfolding S' by simp
  hence "funs_term (Fun f T) = funs_term (Fun f S)"
    using Cons.prems(1) Cons.IH[of S] unfolding S' by simp
  thus ?case using Cons.prems(2)[of 0] unfolding S' by auto
qed simp

lemma finite_fvpairs[simp]: "finite (fvpairs x)" by auto

lemma fvpairs_Nil[simp]: "fvpairs [] = {}" by simp

lemma fvpairs_singleton[simp]: "fvpairs [(t,s)] = fv t  fv s" by simp

lemma fvpairs_Cons: "fvpairs ((s,t)#F) = fv s  fv t  fvpairs F" by simp

lemma fvpairs_append: "fvpairs (F@G) = fvpairs F  fvpairs G" by simp

lemma fvpairs_mono: "set M  set N  fvpairs M  fvpairs N" by auto

lemma fvpairs_inI[intro]:
  "f  set F  x  fvpair f  x  fvpairs F"
  "f  set F  x  fv (fst f)  x  fvpairs F"
  "f  set F  x  fv (snd f)  x  fvpairs F"
  "(t,s)  set F  x  fv t  x  fvpairs F"
  "(t,s)  set F  x  fv s  x  fvpairs F"
using UN_I by fastforce+

lemma fvpairs_cons_subset: "fvpairs F  fvpairs (f#F)"
by auto

lemma in_Fun_fv_iff_in_args_nth_fv:
  "x  fv (Fun f ts)  (i < length ts. x  fv (ts ! i))"
  (is "?A  ?B")
proof
  assume ?A
  hence "x  (fv ` set ts)" by auto
  thus ?B by (metis UN_E in_set_conv_nth)
qed auto


subsection ‹Other lemmata›
lemma nonvar_term_has_composed_shallow_term:
  fixes t::"('f,'v) term"
  assumes "¬(x. t = Var x)"
  shows "f T. Fun f T  t  (s  set T. (c. s = Fun c [])  (x. s = Var x))"
proof -
  let ?Q = "λS. s  set S. (c. s = Fun c [])  (x. s = Var x)"
  let ?P = "λt. g S. Fun g S  t  ?Q S"
  { fix t::"('f,'v) term"
    have "(x. t = Var x)  ?P t"
    proof (induction t)
      case (Fun h R) show ?case
      proof (cases "R = []  (r  set R. x. r = Var x)")
        case False
        then obtain r g S where "r  set R" "?P r" "Fun g S  r" "?Q S" using Fun.IH by fast
        thus ?thesis by auto
      qed force
    qed simp
  } thus ?thesis using assms by blast
qed

end