Quelle  Chop.thy

(*  Title:       The Chop Operation on Lambda-Free Higher-Order Terms
    Author:      Alexander Bentkamp <a.bentkamp at vu.nl>, 2018
    Maintainer:  Alexander Bentkamp <a.bentkamp at vu.nl>
*)

section ‹The Chop Operation on Lambda-Free Higher-Order Terms›

theory Chop
imports Embeddings
begin

definition chop :: "('s, 'v) tm ==> ('s, 'v) tm" where
  "chop t = apps (hd (args t)) (tl (args t))"

subsection ‹Basic properties›

lemma chop_App_Hd: "is_Hd s ==> chop (App s t) = t" 
  unfolding chop_def args.simps 
  using args_Nil_iff_is_Hd by force

lemma chop_apps: "is_App t ==> chop (apps t ts) = apps (chop t) ts" 
  unfolding chop_def by (simp add: args_Nil_iff_is_Hd)

lemma vars_chop: "is_App t ==> vars (chop t) ∪ vars_hd (head t) = vars t" 
  by (induct rule:tm_induct_apps; metis (no_types, lifting) chop_def UN_insert Un_commute list.exhaust_sel list.simps(15)
      args_Nil_iff_is_Hd tm.simps(17) tm_exhaust_apps_sel vars_apps)

lemma ground_chop: "is_App t ==> ground t ==> ground (chop t)" 
  using vars_chop by auto

lemma hsize_chop: "is_App t ==> (Suc (hsize (chop t))) = hsize t"
  unfolding hsize_args[of t, symmetric] chop_def hsize_apps
  by (metis Nil_is_map_conv args_Nil_iff_is_Hd list.exhaust_sel list.map_sel(1) map_tl plus_1_eq_Suc sum_list.Cons)

lemma hsize_chop_lt: "is_App t ==> hsize (chop t) < hsize t"
  by (simp add: Suc_le_lessD less_or_eq_imp_le hsize_chop)

lemma chop_fun:
  assumes "is_App t" "is_App (fun t)" 
  shows "App (chop (fun t)) (arg t) = chop t"  
proof -
  have "args (fun t) ≠ []"
    using assms(2) args_Nil_iff_is_Hd by blast
  then show ?thesis 
    unfolding chop_def
    using assms(1) by (metis (no_types) App_apps args.simps(2) hd_append2 tl_append2 tm.collapse(2))
qed

subsection ‹Chop and the Embedding Relation›

lemma emb_step_chop: "is_App t ==> t →_emb chop t" 
proof (induct "num_args t - 1" arbitrary:t)
  case 0
  have nil: "num_args t = 0 ==> t →_emb chop t" unfolding chop_def using 0 args_Nil_iff_is_Hd by force
  have single: "∧a. args t = [a] ==> t →_emb chop t" unfolding chop_def 
    by (metis "0.prems" apps.simps(1) args.elims args_Nil_iff_is_Hd emb_step_arg last.simps last_snoc list.sel(1) list.sel(3) tm.sel(6))
  then show ?case using nil single
    by (metis "0.hyps" length_0_conv length_tl list.exhaust_sel)
next
  case (Suc x)
  have 1:"apps (Hd (head t)) (butlast (args t)) →_emb chop (apps (Hd (head t)) (butlast (args t)))"
    using Suc(1)[of "apps (Hd (head t)) (butlast (args t))"]
    by (metis Suc.hyps(2) Suc_eq_plus1 add_diff_cancel_right' args_Nil_iff_is_Hd length_butlast list.size(3) nat.distinct(1) tm_exhaust_apps_sel tm_inject_apps)
  have 2:"App (apps (Hd (head t)) (butlast (args t))) (last (args t)) = t"
    by (simp add: App_apps Suc.prems args_Nil_iff_is_Hd)
  have 3:"App (chop (apps (Hd (head t)) (butlast (args t)))) (last (args t)) = chop t"
  proof -
    have f1: "hd (args t) = hd (butlast (args t))"
      by (metis Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd hd_append2 length_0_conv length_butlast nat.simps(3))
    have "tl (args t) = tl (butlast (args t)) @ [last (args t)]"
      by (metis (no_types) Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd length_0_conv length_butlast nat.simps(3) tl_append2)
    then show ?thesis
      using f1 chop_def 
      by (metis App_apps append_Nil args.simps(1) args_apps)
  qed
  then show ?case using 1 2 3 by (metis context_left)
qed 

lemma chop_emb_step_at:
  assumes "is_App t"
  shows "chop t = emb_step_at (replicate (num_args (fun t)) Left) Right t"
using assms proof (induct "num_args (fun t)" arbitrary: t)
  case 0
  then have rep_Nil:"replicate (num_args (fun t)) dir.Left = []" 
    by simp 
  then show ?case unfolding rep_Nil 
    by (metis "0.hyps" "0.prems" emb_step_at_right append_Nil apps.simps(1) args.simps(2) chop_def length_0_conv list.sel(1) list.sel(3) tm.collapse(2)) 
next
  case (Suc n)
  then show ?case using Suc.hyps(1)[of "fun t"]
    using emb_step_at_left_context args.elims args_Nil_iff_is_Hd chop_fun butlast_snoc diff_Suc_1 length_0_conv length_butlast nat.distinct(1) replicate_Suc tm.collapse(2) tm.sel(4)
    by metis
qed

lemma emb_step_at_chop:
  assumes emb_step_at: "emb_step_at p Right t = s"
    and pos:"position_of t (p @ [Right])"
    and all_Left: "list_all (λx. x = Left) p"
  shows "chop t = s ∨ chop t →_emb s"
proof -
  have "is_App t" 
    by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos)
  have p_replicate: "replicate (length p) Left = p" using replicate_length_same[of p Left]
    by (simp add: Ball_set all_Left)
  show ?thesis
  proof (cases "Suc (length p) = num_args t")
    case True
    then have "p = replicate (num_args (fun t)) Left" using p_replicate 
      by (metis Suc_inject ‹is_App t› args.elims args_Nil_iff_is_Hd length_append_singleton tm.sel(4))
    then have "chop t = s" unfolding chop_emb_step_at[OF ‹is_App t›] 
      using pos emb_step_at by blast
    then show ?thesis by blast
  next
    case False
    then have "Suc (length p) < num_args t"
      using pos emb_step_at ‹is_App t› ‹list_all (λx. x = dir.Left) p›
    proof (induct p arbitrary:t s)
      case Nil
      then show ?case 
        by (metis Suc_lessI args_Nil_iff_is_Hd length_greater_0_conv list.size(3))
    next
      case (Cons a p)
      have "a = Left" 
        using Cons.prems(5) by auto
      have 1:"Suc (length p) ≠ num_args (fun t)"  
        by (metis (no_types, lifting) Cons.prems(1) Cons.prems(4) args.elims args_Nil_iff_is_Hd length_Cons length_append_singleton tm.sel(4))
      have 2:"position_of (fun t) (p @ [Right])"
        using ‹position_of t ((a # p) @ [Right])› ‹is_App t›  
          Cons.prems(5)
        by (simp add: list_all_iff flip: position_of_left [of ‹fun t› ‹arg t›])
      have 3: "emb_step_at p dir.Right (fun t) = emb_step_at p dir.Right (fun t)" 
        using emb_step_at_left_context[of p Right "fun t" "arg t"] by blast
      have ‹is_App (fun t)›
        by (metis "2" Embeddings.emb_step_at_head emb_step_at_if_position emb_step_equiv
            tm.collapse(1))
      from 1 2 3 ‹is_App (fun t)› have "Suc (length p) < num_args (fun t)"
        apply (rule Cons.hyps)
        using Cons.prems(5)
        apply (simp add: list_all_iff)
        done
      then show ?case 
        by (metis Cons.prems(4) Suc_less_eq2 args.simps(2) length_Cons length_append_singleton tm.collapse(2))
    qed      
    define q where "q = replicate (num_args (fun t) - Suc (length p)) dir.Left"
    have "chop t = emb_step_at (p @ [Left] @ q) dir.Right t"
    proof -
      have "length p + (num_args (fun t) - length p) = num_args (fun t)" 
        using ‹Suc (length p) < num_args t›
        by (metis Suc_less_eq2 ‹is_App t› args.simps(2) diff_Suc_1 leD length_butlast nat_le_linear 
            ordered_cancel_comm_monoid_diff_class.add_diff_inverse snoc_eq_iff_butlast tm.collapse(2))
      then have 1:"replicate (num_args (fun t)) dir.Left = p @ replicate (num_args (fun t) - length p) dir.Left" 
        by (metis p_replicate replicate_add)
      have "0 < num_args (fun t) - length p"
        by (metis (no_types) False ‹is_App t› ‹length p + (num_args (fun t) - length p) = num_args (fun t)› args.simps(2) length_append_singleton less_Suc_eq less_add_Suc1 tm.collapse(2) zero_less_diff)
      then have "replicate (num_args (fun t) - length p) dir.Left = [Left] @ q" unfolding q_def
        by (metis (no_types) Cons_replicate_eq Nat.diff_cancel Suc_eq_plus1 ‹length p + (num_args (fun t) - length p) = num_args (fun t)› append_Cons self_append_conv2)
      then show ?thesis using chop_emb_step_at
        using ‹is_App t› 1
        by (simp add: chop_emb_step_at)
    qed
    then have "chop t →_emb s"
      using pos merge_emb_step_at[of p Right q Right t] 
      by (metis emb_step_at_if_position opp_simps(1) emb_step_at pos_emb_step_at_opp)
    then show ?thesis by blast
  qed
qed

lemma emb_step_at_remove_arg:
  assumes emb_step_at: "emb_step_at p Left t = s"
    and pos:"position_of t (p @ [Left])"
    and all_Left: "list_all (λx. x = Left) p"
  shows "let i = num_args t - Suc (length p) in
  head t = head s ∧ i < num_args t ∧ args s = take i (args t) @ drop (Suc i) (args t)"
proof -
  have "is_App t" 
    by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos)
  have C1: "head t = head s" 
    using all_Left emb_step_at pos proof (induct p arbitrary:s t)
    case Nil
    then have "s = emb_step_at [] dir.Left (App (fun t) (arg t))"
      by (metis position_of.elims(2) snoc_eq_iff_butlast tm.collapse(2) tm.discI(2))
    then have "s = fun t" by simp
    then show ?case by simp
  next
    case (Cons a p)
    then have "a = Left" by simp
    then have "head (emb_step_at p Left (fun t)) = head t" 
      by (metis Cons.hyps Cons.prems(1) head_fun list.pred_inject(2) position_if_emb_step_at)
    then show ?case using emb_step_at_left_context[of p a "fun t" "arg t"]
      by (metis Cons.prems(2) ‹a = Left› emb_step_at_is_App head_App tm.collapse(2)) 
  qed

  let ?i = "num_args t - Suc (length p)"

  have C2:"?i < num_args t" 
    by (simp add: ‹is_App t› args_Nil_iff_is_Hd)

  have C3:"args s = take ?i (args t) @ drop (Suc ?i) (args t)"
    using all_Left pos emb_step_at ‹is_App t› proof (induct p arbitrary:s t)
    case Nil
    then show ?case using emb_step_at_left[of "fun t" "arg t"]
      by (simp, metis One_nat_def args.simps(2) butlast_conv_take butlast_snoc tm.collapse(2))
  next
    case (Cons a p)
    have *: "position_of (fun t) (p @ [Left])"
      by (metis (full_types) Cons.prems(1) Cons.prems(2) Cons.prems(4) position_of_left 
          append_Cons list.pred_inject(2) tm.collapse(2))
    have 0:"args (emb_step_at p Left (fun t))
                   = take (num_args (fun t) - Suc (length p)) (args (fun t))
                   @ drop (Suc (num_args (fun t) - Suc (length p))) (args (fun t))"
      apply (rule Cons.hyps [of "fun t"])
      using * Cons.prems apply (simp_all add: list_all_iff)
      apply (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv')
      done
    have 1:"s = App (emb_step_at p Left (fun t)) (arg t)" using emb_step_at_left_context[of p Left "fun t" "arg t"] 
      using Cons.prems by auto
    define k where k_def:"k = (num_args (fun t) - Suc (length p))"
    have 2:"take k (args (fun t)) = take (num_args t - Suc (length (a # p))) (args t)"
      by (metis (no_types, lifting) Cons.prems(4) args.elims args_Nil_iff_is_Hd butlast_snoc
          diff_Suc_eq_diff_pred diff_less k_def length_Cons length_butlast length_greater_0_conv
          take_butlast tm.sel(4) zero_less_Suc)
    have k_def': "k = num_args t - Suc (Suc (length p))" using k_def
      by (metis args.simps(2) diff_Suc_Suc length_append_singleton local.Cons(5) tm.collapse(2))
    have 3:"args (fun t) @ [arg t] = args t"
      by (metis Cons.prems(4) args.simps(2) tm.collapse(2))
    have "num_args t > 1" using ‹position_of t ((a # p) @ [Left])›
      by (metis "3" ‹position_of (fun t) (p @ [dir.Left])› args_Nil_iff_is_Hd butlast_snoc emb_step.simps emb_step_at_if_position length_butlast length_greater_0_conv tm.discI(2) zero_less_diff)
    then have "Suc k<num_args t" unfolding k_def'
      using ‹1 < num_args t› by linarith
    have "∀k< num_args t. drop k (args (fun t)) @ [arg t] = drop k (args t)"
      by (metis (no_types, lifting) ‹args (fun t) @ [arg t] = args t› drop_butlast drop_eq_Nil last_drop leD snoc_eq_iff_butlast)
    then show ?case using 0 1 2 3 k_def'
      using ‹Suc k < num_args t› k_def by auto
  qed
  show ?thesis using C1 C2 C3 by simp
qed

lemma emb_step_cases [consumes 1, case_names chop extended_chop remove_arg under_arg]:
  assumes emb:"t →_emb s"
    and chop:"chop t = s ==> P"
    and extended_chop:"chop t →_emb s ==> P"
    and remove_arg:"∧i. head t = head s ==> i<num_args t ==> args s = take i (args t) @ drop (Suc i) (args t) ==> P"
    and under_arg:"∧i. head t = head s ==> num_args t = num_args s ==> args t ! i →_emb args s ! i ==>
         (∧j. j<num_args t ==> i ≠ j ==> args t ! j = args s ! j) ==> P"
  shows P
proof -
  obtain p d where pd_def:"emb_step_at p d t = s" "position_of t (p @ [d])"
    using emb emb_step_equiv' position_if_emb_step_at by metis
  have "is_App t"
    by (metis emb emb_step_at_is_App emb_step_equiv)
  show ?thesis 
  proof (cases "list_all (λx. x = Left) p")
    case True
    show ?thesis 
    proof (cases d)
      case Left
      then show P using emb_step_at_remove_arg 
        by (metis True pd_def(1) pd_def(2) remove_arg)
    next
      case Right
      then show P 
        using True chop emb_step_at_chop extended_chop pd_def(1) pd_def(2) by blast
    qed
  next
    case False
    have 1:"num_args t = num_args s" using emb_step_under_args_num_args
      by (metis False pd_def(1))
    have 2:"head t = head s" using emb_step_under_args_head
      by (metis False pd_def(1))
    show ?thesis using 1 2 under_arg emb_step_under_args_emb_step
      by (metis False pd_def(1) pd_def(2))
  qed
qed

lemma chop_position_of:
  assumes "is_App s"
  shows "position_of s (replicate (num_args (fun s)) dir.Left @ [Right])"
  by (metis Suc_n_not_le_n assms chop_emb_step_at lessI less_imp_le_nat position_if_emb_step_at hsize_chop)

subsection ‹Chop and Substitutions›

(* TODO: move *)
lemma Suc_num_args: "is_App t ==> Suc (num_args (fun t)) = num_args t" 
  by (metis args.simps(2) length_append_singleton tm.collapse(2))

(* TODO: move *)
lemma fun_subst: "is_App s ==> subst ρ (fun s) = fun (subst ρ s)"
  by (metis subst.simps(2) tm.collapse(2) tm.sel(4))

(* TODO: move *)
lemma args_subst_Hd:
  assumes "is_Hd (subst ρ (Hd (head s)))"
  shows  "args (subst ρ s) = map (subst ρ) (args s)"
  using assms 
  by (metis append_Nil args_Nil_iff_is_Hd args_apps subst_apps tm_exhaust_apps_sel)

lemma chop_subst_emb0:
  assumes "is_App s"
  assumes "chop (subst ρ s) ≠ subst ρ (chop s)"
  shows "emb_step_at (replicate (num_args (fun s)) Left) Right (chop (subst ρ s)) = subst ρ (chop s)"
proof -
  have "is_App (subst ρ s)"
    by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2))
  have 1:"subst ρ (chop s) = emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (subst ρ s)"
    using chop_emb_step_at[OF assms(1)] using emb_step_at_subst chop_position_of[OF ‹is_App s›] 
    by (metis)
  have "num_args (fun s) ≤ num_args (fun (subst ρ s))" 
    using fun_subst[OF ‹is_App s›] 
    by (metis args_subst leI length_append length_map not_add_less2)
  then have "num_args (fun s) < num_args (fun (subst ρ s))" 
    using assms(2) "1" ‹is_App (subst ρ s)› chop_emb_step_at le_imp_less_or_eq 
    by fastforce
  then have "num_args s ≤ num_args (fun (subst ρ s))" 
    using Suc_num_args[OF ‹is_App s›] by linarith
  then have  "replicate (num_args (fun s)) dir.Left @
        [opp dir.Right] @ replicate (num_args (fun (subst ρ s)) - num_args s) dir.Left =
        replicate (num_args (fun (subst ρ s))) dir.Left" 
    unfolding append.simps opp_simps replicate_Suc[symmetric] replicate_add[symmetric]
    using Suc_num_args[OF ‹is_App s›]
    by (metis add_Suc_shift ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
  then show ?thesis unfolding 1
    unfolding  chop_emb_step_at[OF ‹is_App (subst ρ s)›]
    by (metis merge_emb_step_at)
qed

lemma chop_subst_emb:
  assumes "is_App s"
  shows "chop (subst ρ s) ⊵_emb subst ρ (chop s)"
  using chop_subst_emb0
  by (metis assms emb.refl emb_step_equiv emb_step_is_emb)

lemma chop_subst_Hd:
  assumes "is_App s"
  assumes "is_Hd (subst ρ (Hd (head s)))"
  shows "chop (subst ρ s) = subst ρ (chop s)" 
proof -
  have "is_App (subst ρ s)"
    by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2))
  have "num_args (fun s) = num_args (fun (subst ρ s))" unfolding fun_subst[OF ‹is_App s›,symmetric]
    using args_subst_Hd using assms(2) by auto
  then show ?thesis
    unfolding chop_emb_step_at[OF assms(1)] chop_emb_step_at[OF ‹is_App (subst ρ s)›]
    using emb_step_at_subst[OF chop_position_of[OF ‹is_App s›]]
    by simp
qed

lemma chop_subst_Sym:
  assumes "is_App s"
  assumes "is_Sym (head s)"
  shows "chop (subst ρ s) = subst ρ (chop s)" 
  by (metis assms(1) assms(2) chop_subst_Hd ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.simps(17))

end