Theory Complex_Constant_Removal

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2013, 2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2013-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Complex_Constant_Removal
imports
  QTRS.QDP_Framework
begin

text ‹the following technique allows to replace a ground expression
  like a large constant c or some value "ack(5,5)" by a fresh variable x.
  this variable must then be added as new (last) argument to all pairs.
  this technique is sometimes applied as a preprocessing technique for bounded increase
  where loops like (while i < 1000 do i++) are transformed into (while i < x do i++).
›
text ‹the technique can be improved by only demanding CR of usable rules of c,
   where @{thm normalize_subst_qrsteps_inn_partial} should be useful.
   so far, in example proofs this was never necessary, so it remains as future work›
lemma complex_constant_removal: fixes P :: "('f,'v)trs" 
  assumes fin: "finite_dpp (nfs,m,P',Pw',Q,{},R)" (is "finite_dpp ?P'")
  and CR: "c ∈ NF_trs R ∨ CR (qrstep nfs Q R)"
  and inn: "NF_terms Q ⊆ NF_trs R"
  and ground: "ground c"
  and PPW: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ is_Fun s ∧ is_Fun t ∧ ¬ defined R (the (root t))"
  and x: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ x ∉ vars_rule (s,t)"
  and rel: "⋀ P P' f ss g ts. rel P P' ⟹ (Fun f ss, Fun g ts) ∈ P ⟹
    ∃ ts'. (Fun (ren (f,length ss)) (ss @ [Var x]), Fun (ren (g,length ts)) (ts' @ [Var x])) ∈ P'
      ∧ ts = map (λ t. t ⋅ subst x c) ts'"
  and ren: "⋀ f ss t. (Fun f ss,t) ∈ P ∪ Pw ⟹ Some (ren (f,length ss), Suc (length ss)) ∉ root ` Q"
  and ren2: "⋀ f ss t. (Fun f ss,t) ∈ P ∪ Pw ⟹ ¬ defined R (ren (f,length ss), Suc (length ss))"
  and R: "∀ (l,r) ∈ R. is_Fun l"
  and P: "rel P P'"
  and Pw: "rel Pw Pw'"
  shows "finite_dpp (nfs,m,P,Pw,Q,{},R)" (is "finite_dpp ?P")
proof -
  let ?xc = "subst x c"
  let ?QR = "qrstep nfs Q R"
  let ?Q = "NF_terms Q"
  let ?NFR = "NF_trs R"
  let ?prop = "λ u. (c,u) ∈ ?QR^* ∧ u ∈ ?Q"
  have "?NFR = NF (qrstep nfs {} R)" by simp
  also have "… ⊆ NF ?QR"
    by (rule NF_anti_mono, auto)
  finally have NFR_imp_NF: "?NFR ⊆ NF ?QR" .
  with inn have Q_imp_NF: "?Q ⊆ NF ?QR" by auto
  {
    fix s t σ    
    assume "min_ichain ?P s t σ"
    note chain = this[unfolded min_ichain.simps ichain.simps, simplified]
    from chain have PP: "⋀ i. (s i, t i) ∈ P ∪ Pw" by auto
    from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?QR^*" by auto
    from chain have NF: "⋀ i. s i ⋅ σ i ∈ ?Q" by auto
    from chain have m: "⋀ i. m ⟹ SN_on ?QR {t i ⋅ σ i}" unfolding minimal_cond_def by auto
    (* in principle we want to instantiate x by some normal form of c (which is unique due to CR).
       however, we do not know, whether c is normalizing (perhaps the chain only uses pairs where 
       c does not occur), but still need a normal form for filling the fresh variable in the additional
       argument of every pair. therefore, nf is defined via the following case distinction *)
    def nf ≡ "if (∃ u. ?prop u) then (SOME u. ?prop u) else (SOME u. u ∈ ?Q)"
    have nf: "nf ∈ ?Q"
    proof (cases "∃ u. ?prop u")
      case True
      from someI_ex[of ?prop, OF True] show ?thesis unfolding nf_def by auto
    next
      case False
      from someI[of "λ u. u ∈ ?Q", OF NF] False show ?thesis unfolding nf_def by auto
    qed
    (* now we can define the new substitution *)
    def σ' ≡ "λ i. (σ i)(x := nf)"
    (* and the substitutions which corresponds to the unmodified chain *)
    def σ'' ≡ "λ i. (σ i)(x := c)"
    (* next we extract all the pairs in more explicit form *)
    {
      fix i
      from PPW[OF PP[of i]] obtain f ss where si: "s i = Fun f ss" by (cases "s i", auto)
      from PPW[OF PP[of i]] obtain g ts where ti: "t i = Fun g ts" by (cases "t i", auto)
      have "∃ f g ss ts. s i = Fun f ss ∧ t i = Fun g ts" using si ti by auto
    }
    from choice[OF allI[OF this]] obtain f where "∀ i. ∃ g ss ts. s i = Fun (f i) ss ∧ t i = Fun g ts" ..
    from choice[OF this] obtain g where "∀ i. ∃ ss ts. s i = Fun (f i) ss ∧ t i = Fun (g i) ts" ..
    from choice[OF this] obtain ss where "∀ i. ∃ ts. s i = Fun (f i) (ss i) ∧ t i = Fun (g i) ts" ..
    from choice[OF this] obtain ts where si_ti: "⋀ i. s i = Fun (f i) (ss i)" "⋀ i. t i = Fun (g i) (ts i)" by auto
    {
      fix i
      from PPW[OF PP[of i], unfolded si_ti] have ndef: "¬ defined R (g i, length (ts i))" by simp
      from nondef_root_imp_arg_qrsteps[OF steps[of i, unfolded si_ti, simplified] R] ndef
      have "g i = f (Suc i)" "length (ts i) = length (ss (Suc i))" "¬ defined R (f (Suc i), length (ss (Suc i)))" by auto
    } note gi = this    
    note si_ti = si_ti[unfolded gi]
    let ?g = "λ i. f (Suc i)"
    let ?lss = "λ i. length (ss i)"
    let ?lts = "λ i. length (ss (Suc i))"
    (* make sure that strict pairs P are translated into strict pairs P' ... *)
    def Pb ≡ "λ i. if (s i, t i) ∈ P then P else Pw"
    def Pb' ≡ "λ i. if (s i, t i) ∈ P then P' else Pw'"
    (* ... in the following way to obtain the new pairs *)
    {
      fix i
      have mem: "(s i, t i) ∈ Pb i" using PP[of i] unfolding Pb_def by auto
      have Pb: "rel (Pb i) (Pb' i)" using P Pw unfolding Pb_def Pb'_def by (cases "(s i, t i) ∈ P", auto)
      note mem = mem[unfolded si_ti]
      from rel[OF Pb mem, unfolded gi] have "∃ ts'. (Fun (ren (f i , ?lss i)) (ss i @ [Var x]), Fun (ren (?g i, ?lts i)) (ts' @ [Var x])) ∈ Pb' i
        ∧ ts i = map (λt. t ⋅ ?xc) ts'" by auto
    }
    from choice[OF allI[OF this]] obtain ts' where "∀ i. (Fun (ren (f i , ?lss i)) (ss i @ [Var x]), Fun (ren (?g i, ?lts i)) (ts' i @ [Var x])) ∈ Pb' i
        ∧ ts i = map (λt. t ⋅ ?xc) (ts' i)" ..
    hence ts: "⋀ i. ts i = map (λt. t ⋅ ?xc) (ts' i)" 
      and Pb': "⋀ i. (Fun (ren (f i , ?lss i)) (ss i @ [Var x]), Fun (ren (?g i, ?lts i)) (ts' i @ [Var x])) ∈ Pb' i" by blast+
    let ?s = "λ i. Fun (ren (f i, ?lss i)) (ss i @ [Var x])"
    let ?t = "λ i. Fun (ren (?g i, ?lts i)) (ts' i @ [Var x])"
    def s' ≡ ?s
    def t' ≡ ?t
    (* we have all ingredients to define our new chain, so it remains to prove that it really is a chain *)
    have "min_ichain ?P' s' t' σ'"
    proof -    
      {
        fix t :: "('f,'v)term" and i
        assume x: "x ∉ vars_term t"
        have "t ⋅ σ' i = t ⋅ σ i"
          by (rule term_subst_eq, insert x, unfold σ'_def, auto)
      } note σ' = this
      have [simp]: "⋀ i. σ' i x = nf" unfolding σ'_def by auto
      have [simp]: "⋀ σ. c ⋅ σ = c" by (rule ground_subst_apply[OF ground])
      {
        fix i
        let ?ss = "map (λ s. s ⋅ σ i) (ss i)"
        {
          fix s
          assume "s ∈ set (ss i)"
          with x[OF PP[of i, unfolded si_ti]] have x: "x ∉ vars_term s" unfolding vars_rule_def by auto
          from σ'[OF this] have "s ⋅ σ' i = s ⋅ σ i" .
        } 
        hence "s' i ⋅ σ' i = Fun (ren (f i,?lss i)) (?ss @ [nf])" unfolding s'_def by simp
      } note sis = this (* represent s' i ⋅ σ' i more conveniently *)
      {
        fix i
        let ?ts = "map (λ t. t ⋅ σ'' i) (ts' i)"
        have "map (λt. t ⋅ ?xc ⋅ σ i) (ts' i) = ?ts"
        proof (rule nth_map_conv[OF refl], intro allI impI)
          fix j
          have "ts' i ! j ⋅ ?xc ⋅ σ i = ts' i ! j ⋅ (?xc ∘⇩s σ i)" by auto
          also have "… = ts' i ! j ⋅ σ'' i"
            by (rule term_subst_eq, unfold subst_compose_def σ''_def subst_def, auto)
          finally show "ts' i ! j ⋅ ?xc ⋅ σ i = ts' i ! j ⋅ σ'' i" .
        qed
        hence "t i ⋅ σ i = Fun (?g i) ?ts" "t' i ⋅ σ' i = Fun (ren (?g i,?lts i)) (map (λ t. t ⋅ σ' i) (ts' i) @ [nf])"
          unfolding si_ti ts t'_def by auto        
      } note tis = this (* represent t i ⋅ σ i and t' i ⋅ σ' i more conveniently *)
      {
        (* show all properties I, II, ... of a chain for each i *)
        fix i
        let ?si = "?s i"
        let ?ti = "?t i"
        let ?ss = "map (λ s. s ⋅ σ i) (ss i)"
        let ?ts = "map (λ s. s ⋅ σ' i) (ts' i)"
        let ?sss = "map (λ s. s ⋅ σ (Suc i)) (ss (Suc i))"
        note memP = PP[of i, unfolded si_ti]
        have mem: "(?si, ?ti) ∈ Pb' i" by (rule Pb')
        hence I: "(s' i, t' i) ∈ P' ∪ Pw'" "(s' i, t' i) ∈ Pb' i" unfolding s'_def t'_def Pb'_def
          by (cases "(s i, t i) ∈ P", auto)
        have II: "s' i ⋅ σ' i ∈ ?Q" unfolding sis
        proof (rule NF_args_imp_NF[OF _ nf])
          show "Some (ren (f i, ?lss i), length (?ss @ [nf])) ∉ root ` Q"
            using ren[OF memP]  by auto
        next
          fix s
          assume "s ∈ set (?ss @ [nf])"
          hence "s ∈ set ?ss ∨ s = nf" by auto
          thus "s ∈ NF_terms Q"
          proof
            assume "s = nf" with nf show ?thesis by auto
          next
            assume "s ∈ set ?ss"
            hence "Fun (f i) (ss i) ⋅ σ i ⊳ s" by auto
            with NF_imp_subt_NF[OF NF[of i, unfolded si_ti]] show ?thesis by blast
          qed
        qed  
        {
          (* for strong normalization and evaluation between pairs, first consider
             some arbitrary argument of (ts i) *)
          fix j
          assume j: "j < length (ts' i)"
          have "(ts' i ! j ⋅ σ'' i, ts' i ! j ⋅ σ' i) ∈ ?QR^* ∧ (c ∈ ?NFR ⟶ ts' i ! j ⋅ σ'' i = ts' i ! j ⋅ σ' i)"
          proof (cases "x ∈ vars_term (ts' i ! j)")
            case False
            have "ts' i ! j ⋅ σ'' i = ts' i ! j ⋅ σ' i"
              by (rule term_subst_eq, insert False, auto simp: σ'_def σ''_def subst_def)
            thus ?thesis by auto
          next
            case True
            from j have arg: "t i ⋅ σ i ⊵ ts' i ! j ⋅ σ'' i" 
              unfolding tis by auto
            from True have "ts' i ! j ⊵ Var x" by auto
            from supteq_subst[OF this, of "σ'' i"] have "ts' i ! j ⋅ σ'' i ⊵ c"
              by (simp add: σ''_def subst_def)
            from supteq_trans[OF arg this] have "t i ⋅ σ i ⊵ c" .
            from supteq_imp_subt_at[OF this] 
              obtain p where c: "t i ⋅ σ i |_ p = c" and p: "p ∈ poss (t i ⋅ σ i)" by auto
            from normalize_subterm_qrsteps[OF p steps[of i] NF, unfolded c] obtain u
              where cu: "(c,u) ∈ ?QR^*" and u: "u ∈ ?Q" by auto
            hence propu: "∃ u. ?prop u" by auto
            hence "nf = (SOME u. ?prop u)" unfolding nf_def by auto
            from someI_ex[of ?prop, OF propu, folded this] have cnf: "(c,nf) ∈ ?QR^*" ..            
            show ?thesis
            proof (intro conjI impI, rule all_ctxt_closed_subst_step)
              fix y
              show "(σ'' i y, σ' i y) ∈ ?QR^*"
                by (cases "y = x", insert cnf, auto simp: subst_def σ'_def σ''_def)
            next
              assume "c ∈ ?NFR"
              with NFR_imp_NF have "c ∈ NF ?QR" by auto
              with cnf have nf: "nf = c" by (induct, auto)
              show "ts' i ! j ⋅ σ'' i = ts' i ! j ⋅ σ' i" unfolding σ'_def σ''_def nf ..
            qed auto
          qed
          hence ts_ts': "(ts' i ! j ⋅ σ'' i, ts' i ! j ⋅ σ' i) ∈ ?QR^*" and 
            ts_ts'': "c ∈ ?NFR ⟹ ts' i ! j ⋅ σ' i = ts' i ! j ⋅ σ'' i" by auto
          from nondef_root_imp_arg_qrsteps[OF steps[of i, unfolded si_ti, simplified] R]
            j ts gi[of i] 
          have "(ts i ! j ⋅ σ i, ?sss ! j) ∈ ?QR^*" by auto
          with tis[of i, unfolded si_ti] j ts 
          have arg_steps: "(ts' i ! j ⋅ σ'' i, ?sss ! j) ∈ ?QR^*" by auto
          have steps: "(ts' i ! j ⋅ σ' i, ?sss ! j) ∈ ?QR^*"
          proof (cases "c ∈ ?NFR")
            case True
            from ts_ts''[OF this] show ?thesis using arg_steps by simp
          next
            case False
            with CR have CR: "CR ?QR" by simp
            from CR_divergence_imp_join[OF CR ts_ts' arg_steps] obtain u where
              join: "(ts' i ! j ⋅ σ' i, u) ∈ ?QR^*" and u: "(?sss ! j, u) ∈ ?QR^*" by auto
            have "?sss ! j ∈ ?Q"
              by (rule NF_subterm[OF NF[of "Suc i", unfolded si_ti]], insert j ts gi, auto)
            hence "?sss ! j ∈ NF ?QR" using Q_imp_NF by auto
            with u have u: "u = ?sss ! j" by (induct, auto)
            from join u show "(ts' i ! j ⋅ σ' i, ?sss ! j) ∈ ?QR^*" by simp
          qed
          {
            assume m
            have "SN_on ?QR {ts i ! j ⋅ σ i}"
              by (rule SN_imp_SN_arg_gen[OF ctxt_closed_qrstep m[OF ‹m›, of i, unfolded si_ti, simplified]],
                insert j ts, auto)
            with tis[of i] j ts si_ti have "SN_on ?QR {ts' i ! j ⋅ σ'' i}" by auto
            from steps_preserve_SN_on[OF ts_ts' this] have "SN_on ?QR {ts' i ! j ⋅ σ' i}" .
          }
          note steps this
        }
        note steps_SN = this   
        (* using steps_SN allows to easily derive III and IV *)
        from arg_cong[OF ts, of length] gi have ts': "length (ts' i) = length (ss (Suc i))" by simp
        have III: "(t' i ⋅ σ' i, s' (Suc i) ⋅ σ' (Suc i)) ∈ ?QR^*"
          unfolding sis tis
        proof (rule all_ctxt_closedD[of UNIV])
          fix j
          assume "j < length (?ts @ [nf])"
          hence j: "j < Suc (length (ts' i))" by auto
          show "((?ts @ [nf]) ! j, (?sss @ [nf]) ! j) ∈ ?QR^*"
          proof (cases "j < length (ts' i)")
            case True
            from steps_SN(1)[OF True] show ?thesis using ts' True by (auto simp: nth_append)
          next
            case False
            with j have j: "j = length (ts' i)" by auto
            thus ?thesis using ts' by (auto simp: nth_append)
          qed
        qed (auto simp: ts')
        have IV: "m ⟹ SN_on ?QR {t' i ⋅ σ' i}"
        proof -
          assume m
          show "SN_on (qrstep nfs Q R) {t' i ⋅ σ' i}"
            unfolding tis
          proof (rule SN_args_imp_SN[OF _ R ndef_applicable_rules])
            from ren2[OF PP[of "Suc i", unfolded si_ti]]
            show "¬ defined R (ren (f (Suc i), ?lts i), length (?ts @ [nf]))"
              using ts' by auto
          next
            fix t
            assume "t ∈ set (?ts @ [nf])"
            hence "t ∈ set ?ts ∨ t = nf" by auto
            thus "SN_on ?QR {t}"
            proof
              assume "t = nf"
              with nf Q_imp_NF show ?thesis by blast
            next
              assume "t ∈ set ?ts"
              from this[unfolded set_conv_nth] obtain j where 
                j: "j < length (ts' i)" and t: "t = ts' i ! j ⋅ σ' i" by auto
              from steps_SN(2)[OF j ‹m›] show ?thesis unfolding t .
            qed
          qed
        qed
        have V: "NF_subst nfs (s' i, t' i) (σ' i) Q"
        proof
          fix y
          assume nfs and y: "y ∈ vars_term (s' i) ∨ y ∈ vars_term (t' i)"
          have "vars_term (s' i) ∪ vars_term (t' i) = vars_term (s i) ∪ (vars_term (Fun h (ts' i)) ∪ {x})"
            unfolding s'_def t'_def si_ti by auto
          also have "… ⊆ vars_term (s i) ∪ vars_term (Fun h (ts' i) ⋅ ?xc) ∪ {x}"
            unfolding vars_term_subst subst_def fun_upd_def by auto
          also have "… = vars_rule (s i, t i) ∪ {x}" unfolding si_ti ts vars_rule_def by auto
          finally have "y = x ∨ y ≠ x ∧ y ∈ vars_rule (s i, t i)" using y by blast
          thus "σ' i y ∈ ?Q"
          proof
            assume "y = x"
            with nf show ?thesis by simp
          next
            assume y: "y ≠ x ∧ y ∈ vars_rule (s i, t i)"
            from chain have "NF_subst nfs (s i, t i) (σ i) Q" by simp
            from this[unfolded NF_subst_def, rule_format, OF ‹nfs›] y have "σ i y ∈ ?Q" by auto
            with y show ?thesis unfolding σ'_def by auto
          qed
        qed
        note I II III IV V
      }
      note main = this
      have "INFM i. (s' i, t' i) ∈ P'"
        unfolding INFM_nat_le
      proof
        fix i
        from chain[unfolded INFM_nat_le] obtain j where j: "j ≥ i" and mem: "(s j, t j) ∈ P" by blast
        from main(2)[of j] mem have "(s' j, t' j) ∈ P'" unfolding Pb'_def by auto
        with j show "∃ j ≥ i. (s' j, t' j) ∈ P'" by auto
      qed
      thus "min_ichain ?P' s' t' σ'"
        unfolding min_ichain.simps ichain.simps using main by (auto simp: minimal_cond_def)
    qed
    with fin have False unfolding finite_dpp_def by auto
  }
  thus ?thesis unfolding finite_dpp_def by blast
qed

end