Theory Abstract_Rewriting_Impl

subsection‹Abstract Rewriting›

theory Abstract_Rewriting_Impl
  imports 
    "Abstract-Rewriting.Abstract_Rewriting"
begin

partial_function (option) compute_NF :: "('a ⇒ 'a option) ⇒ 'a ⇒ 'a option"
  where [simp,code]: "compute_NF f a = (case f a of None ⇒ Some a | Some b ⇒ compute_NF f b)"

lemma compute_NF_sound: assumes res: "compute_NF f a = Some b"
  and f_sound: "⋀ a b. f a = Some b ⟹ (a,b) ∈ r"
shows "(a,b) ∈ r^*"
proof (induct rule: compute_NF.raw_induct[OF _ res, of "λ g a b. g = f ⟶ (a,b) ∈ r^*", THEN mp[OF _ refl]])
  case (1 cnf g a b)
  show ?case
  proof
    assume "g = f"
    note 1 = 1[unfolded this]
    show "(a,b) ∈ r^*"
    proof (cases "f a")
      case None
      with 1(2) show ?thesis by simp
    next
      case (Some c)
      from 1(2)[unfolded this] have "cnf f c = Some b" by simp
      from 1(1)[OF this] have "(c,b) ∈ r^*" by auto
      with f_sound[OF Some] show ?thesis by auto
    qed
  qed
qed

lemma compute_NF_complete: assumes res: "compute_NF f a = Some b"
  and f_complete: "⋀ a. f a = None ⟹ a ∈ NF r"
shows "b ∈ NF r"
proof (induct rule: compute_NF.raw_induct[OF _ res, of "λ g a b. g = f ⟶ b ∈ NF r", THEN mp[OF _ refl]])
  case (1 cnf g a b)
  show ?case
  proof
    assume "g = f"
    note 1 = 1[unfolded this]
    show "b ∈ NF r"
    proof (cases "f a")
      case None
      with f_complete[OF None] 1(2)
      show ?thesis by simp
    next
      case (Some c)
      from 1(2)[unfolded this] have "cnf f c = Some b" by simp
      from 1(1)[OF this] show ?thesis by simp
    qed
  qed
qed

lemma compute_NF_SN: assumes SN: "SN r"
  and f_sound: "⋀ a b. f a = Some b ⟹ (a,b) ∈ r"
shows "∃ b. compute_NF f a = Some b" (is "?P a")
proof -
  let ?r = "{(a,b). f a = Some b}"
  have "?r ⊆ r" using f_sound by auto
  from SN_subset[OF SN this] have SNr: "SN ?r" .
  show ?thesis
  proof (induct rule: SN_induct[OF SNr, of "λ a. ?P a"])
    case (1 a)
    show ?case
    proof (cases "f a")
      case None then show ?thesis by auto
    next
      case (Some b)
      then have "(a,b) ∈ ?r" by simp
      from 1[OF this] f_sound[OF Some] show ?thesis 
        using Some by auto
    qed
  qed
qed

definition "compute_trancl A R = R^+ `` A"
lemma compute_trancl_rtrancl[code_unfold]: "{b. (a,b) ∈ R^*} = insert a (compute_trancl {a} R)"
proof -
  have id: "R^* = (Id ∪ R^+)" by regexp
  show ?thesis unfolding id compute_trancl_def by auto
qed

lemma compute_trancl_code[code]: "compute_trancl A R = (let B = R `` A in 
  if B ⊆ {} then {} else B ∪ compute_trancl B { ab ∈ R . fst ab ∉ A ∧ snd ab ∉ B})"
proof -
  have R: "R^+ = R O R^*" by regexp
  define B where "B = R `` A"
  define R' where "R' = {ab ∈ R. fst ab ∉ A ∧ snd ab ∉ B}"
  note d = compute_trancl_def
  show ?thesis unfolding Let_def B_def[symmetric] R'_def[symmetric] d
  proof (cases "B ⊆ {}")
    case True
    then show "R⇧+ `` A = (if B ⊆ {} then {} else B ∪ R'^+ `` B)" unfolding B_def R by auto
  next
    case False
    have "R' ⊆ R" unfolding R'_def by auto 
    then have "R'^+ ⊆ R^+" by (rule trancl_mono_set)
    also have "… ⊆ R^*" by auto
    finally have mono: "R'^+ ⊆ R^*" .
    have "B ∪ R'⇧+ `` B = R⇧+ `` A"  
    proof
      show "B ∪ R'⇧+ `` B ⊆ R^+ `` A" unfolding B_def R using mono
        by blast
    next
      show "R^+ `` A ⊆ B ∪ R'^+ `` B"
      proof
        fix x
        assume "x ∈ R^+ `` A"
        then obtain a where a: "a ∈ A" and ax: "(a,x) ∈ R^+" by auto
        from ax a show "x ∈ B ∪ R'^+ `` B"
        proof (induct)
          case base
          then show ?case unfolding B_def by auto
        next
          case (step x y)
          from step(3)[OF step(4)] have x: "x ∈ B ∪ R'^+ `` B" .
          show ?case
          proof (cases "y ∈ B")
            case False note y = this
            show ?thesis
            proof (cases "x ∈ A")
              case True
              with y step(2) show ?thesis unfolding B_def by auto
            next
              case False
              with y step(2) have "(x,y) ∈ R'" unfolding R'_def by auto
              with x have "y ∈  (R' ∪ (R'^+ O R')) `` B" by blast
              also have "R' ∪ (R'^+ O R') = R'^+" by regexp
              finally show ?thesis by blast
            qed
          qed auto
        qed
      qed 
    qed      
    with False show "R⇧+ `` A = (if B ⊆ {} then {} else B ∪ R'^+ `` B)" by auto
  qed 
qed

lemma trancl_image_code[code_unfold]: "R^+ `` A = compute_trancl A R" unfolding compute_trancl_def by auto
lemma compute_rtrancl[code_unfold]: "R^* `` A = A ∪ compute_trancl A R"
proof -
  have id: "R^* = (Id ∪ R^+)" by regexp
  show ?thesis unfolding id compute_trancl_def by auto
qed
lemma trancl_image_code'[code_unfold]: "(a,b) ∈ R^+ ⟷ b ∈ compute_trancl {a} R" unfolding compute_trancl_def by auto
lemma rtrancl_image_code[code_unfold]: "(a,b) ∈ R^* ⟷ b = a ∨ b ∈ compute_trancl {a} R"
  using compute_rtrancl[of R "{a}"] by auto

end