Theory Tree

theory Tree 
  imports Main

begin
subsection "Tree"

inductive_set
  tree :: "['a ⇒ 'a set,'a] ⇒ (nat * 'a) set"
  for subs :: "'a ⇒ 'a set" and γ :: 'a
    ―‹This set represents the nodes in a tree which may represent a proof of @{term γ}.
   Only storing the annotation and its level.›
  where
    tree0: "(0,γ) ∈ tree subs γ"

  | tree1: "⟦(n,delta) ∈ tree subs γ; sigma ∈ subs delta⟧
            ⟹ (Suc n,sigma) ∈ tree subs γ"

declare tree.cases [elim]
declare tree.intros [intro]

lemma tree0Eq: "(0,y) ∈ tree subs γ = (y = γ)"
  by auto

lemma tree1Eq:
    "(Suc n,Y) ∈ tree subs γ ⟷ (∃sigma ∈ subs γ . (n,Y) ∈ tree subs sigma)"
  by (induct n arbitrary: Y) force+
    ― ‹moving down a tree›

definition
  incLevel :: "nat * 'a ⇒ nat * 'a" where
  "incLevel = (% (n,a). (Suc n,a))"

lemma injIncLevel: "inj incLevel"
  by (simp add: incLevel_def inj_on_def)

lemma treeEquation: "tree subs γ = insert (0,γ) (⋃delta∈subs γ. incLevel ` tree subs delta)"
proof -
  have "a = 0 ∧ b = γ"
    if "(a, b) ∈ tree subs γ"
      and "∀x∈subs γ. ∀(n, x) ∈tree subs x. (a, b) ≠ (Suc n, x)"
    for a b
    using that Zero_not_Suc
    by (smt (verit) case_prod_conv tree.cases tree1Eq)
  then show ?thesis
    by (auto simp: incLevel_def image_iff tree1Eq case_prod_unfold)
qed

definition
  fans :: "['a ⇒ 'a set] ⇒ bool" where
  "fans subs ≡ (∀x. finite (subs x))"


subsection "Terminal"

definition
  terminal :: "['a ⇒ 'a set,'a] ⇒ bool" where
  "terminal subs delta ≡ subs(delta) = {}"

lemma terminalD: "terminal subs Γ ⟹ x ~: subs Γ"
  by(simp add: terminal_def)
  ― ‹not a good dest rule›

lemma terminalI: "x ∈ subs Γ ⟹ ¬ terminal subs Γ"
  by(auto simp add: terminal_def)
  ― ‹not a good intro rule›


subsection "Inherited"

definition
  inherited :: "['a ⇒ 'a set,(nat * 'a) set ⇒ bool] ⇒ bool" where
  "inherited subs P ≡ (∀A B. (P A ∧ P B) = P (A Un B))
                    ∧ (∀A. P A = P (incLevel ` A))
                    ∧ (∀n Γ A. ¬(terminal subs Γ) ⟶ P A = P (insert (n,Γ) A))
                    ∧ (P {})"

    (******
     inherited properties:
        - preserved under: dividing into 2, join 2 parts
                           moving up/down levels
                           inserting non terminal nodes
        - hold on empty node set
     ******)

  ― ‹FIXME tjr why does it have to be invariant under inserting nonterminal nodes?›

lemma inheritedUn[rule_format]:"inherited subs P ⟶ P A ⟶ P B ⟶ P (A Un B)"
  by (auto simp add: inherited_def)

lemma inheritedIncLevel[rule_format]: "inherited subs P ⟶ P A ⟶ P (incLevel ` A)"
  by (auto simp add: inherited_def)

lemma inheritedEmpty[rule_format]: "inherited subs P ⟶ P {}"
  by (auto simp add: inherited_def)

lemma inheritedInsert[rule_format]:
  "inherited subs P ⟶ ~(terminal subs Γ) ⟶ P A ⟶ P (insert (n,Γ) A)"
  by (auto simp add: inherited_def)

lemma inheritedI[rule_format]: "⟦∀A B . (P A ∧ P B) = P (A Un B);
  ∀A . P A = P (incLevel ` A);
  ∀n Γ A . ~(terminal subs Γ) ⟶ P A = P (insert (n,Γ) A);
  P {}⟧ ⟹ inherited subs P"
  by (simp add: inherited_def)

(* These only for inherited join, and a few more places... *)
lemma inheritedUnEq[rule_format, symmetric]: "inherited subs P ⟶ (P A ∧ P B) = P (A Un B)"
  by (auto simp add: inherited_def)

lemma inheritedIncLevelEq[rule_format, symmetric]: "inherited subs P ⟶ P A = P (incLevel ` A)"
  by (auto simp add: inherited_def)

lemma inheritedInsertEq[rule_format, symmetric]: "inherited subs P ⟶ ~(terminal subs Γ) ⟶ P A = P (insert (n,Γ) A)"
  by (auto simp add: inherited_def)

lemmas inheritedUnD = iffD1[OF inheritedUnEq]

lemmas inheritedInsertD = inheritedInsertEq[THEN iffD1]

lemmas inheritedIncLevelD = inheritedIncLevelEq[THEN iffD1]

lemma inheritedUNEq:
  "finite A ⟹ inherited subs P ⟹ (∀x∈A. P (B x)) = P (⋃ a∈A. B a)"
  by (induction rule: finite_induct) (simp_all add: inherited_def)

lemmas inheritedUN  = inheritedUNEq[THEN iffD1]

lemmas inheritedUND[rule_format] = inheritedUNEq[THEN iffD2]

lemma inheritedPropagateEq: 
  assumes "inherited subs P"
  and "fans subs"
  and "¬ (terminal subs delta)"
shows "P(tree subs delta) = (∀sigma∈subs delta. P(tree subs sigma))"
  using assms unfolding fans_def
  by (metis (mono_tags, lifting) inheritedIncLevelEq inheritedInsertEq inheritedUNEq treeEquation)

lemma inheritedPropagate:
 " ⟦¬ P (tree subs delta); inherited subs P; fans subs; ¬ terminal subs delta⟧
    ⟹ ∃sigma∈subs delta. ¬ P (tree subs sigma)"
  by (simp add: inheritedPropagateEq)

lemma inheritedViaSub:
  "⟦inherited subs P; fans subs; P (tree subs delta); sigma ∈ subs delta⟧ ⟹ P (tree subs sigma)"
  by (simp add: inheritedPropagateEq terminalI)

lemma inheritedJoin:
    "⟦inherited subs P; inherited subs Q⟧ ⟹ inherited subs (λx. P x ∧ Q x)"
  by (smt (verit, best) inherited_def)

lemma inheritedJoinI:
  "⟦inherited subs P; inherited subs Q; R = (λx. P x ∧ Q x)⟧
    ⟹ inherited subs R"
  by (simp add: inheritedJoin)


subsection "bounded, boundedBy"

definition
  boundedBy :: "nat ⇒ (nat * 'a) set ⇒ bool" where
  "boundedBy N A ≡ (∀(n,delta) ∈ A. n < N)"

definition
  bounded :: "(nat * 'a) set ⇒ bool" where
  "bounded A ≡ (∃N . boundedBy N A)"

lemma boundedByEmpty[simp]: "boundedBy N {}"
  by(simp add: boundedBy_def)

lemma boundedByInsert: "boundedBy N (insert (n,delta) B)     = (n < N ∧ boundedBy N B)"
  by(simp add: boundedBy_def)

lemma boundedByUn: "boundedBy N (A Un B) = (boundedBy N A ∧ boundedBy N B)"
  by(auto simp add: boundedBy_def)

lemma boundedByIncLevel': "boundedBy (Suc N) (incLevel ` A) = boundedBy N A"
  by(auto simp add: incLevel_def boundedBy_def)

lemma boundedByAdd1: "boundedBy N B ⟹ boundedBy (N+M) B"
  by(auto simp add: boundedBy_def)

lemma boundedByAdd2: "boundedBy M B ⟹ boundedBy (N+M) B"
  by(auto simp add: boundedBy_def)

lemma boundedByMono: "boundedBy m B ⟹ m < M ⟹ boundedBy M B"
  by(auto simp: boundedBy_def)

lemmas boundedByMonoD  = boundedByMono

lemma boundedBy0: "boundedBy 0 A = (A = {})"
  by (auto simp add: boundedBy_def)

lemma boundedBySuc': "boundedBy N A ⟹ boundedBy (Suc N) A"
  by (auto simp add: boundedBy_def)

lemma boundedByIncLevel: "boundedBy n (incLevel ` (tree subs γ)) ⟷ (∃m . n = Suc m ∧ boundedBy m (tree subs γ))"
  by (metis boundedBy0 boundedByIncLevel' boundedBySuc' emptyE old.nat.exhaust
      tree.tree0)

lemma boundedByUN: "boundedBy N (UN x:A. B x) = (!x:A. boundedBy N (B x))"
  by(simp add: boundedBy_def)

lemma boundedBySuc[rule_format]: "sigma ∈ subs Γ ⟹ boundedBy (Suc n) (tree subs Γ) ⟹ boundedBy n (tree subs sigma)"
  by (metis boundedByIncLevel' boundedByInsert boundedByUN treeEquation)


subsection "Inherited Properties- bounded"

lemma boundedEmpty: "bounded {}"
  by(simp add: bounded_def)

lemma boundedUn: "bounded (A Un B) ⟷ (bounded A ∧ bounded B)"
  by (metis boundedByAdd1 boundedByAdd2 boundedByUn bounded_def)

lemma boundedIncLevel: "bounded (incLevel` A) ⟷ (bounded A)"
  by (meson boundedByIncLevel' boundedBySuc' bounded_def)

lemma boundedInsert: "bounded (insert a B) ⟷ (bounded B)"
proof (cases a)
  case (Pair a b)
  then show ?thesis
  by (metis Un_insert_left Un_insert_right boundedByEmpty boundedByInsert boundedUn
      bounded_def lessI)
qed

lemma inheritedBounded: "inherited subs bounded"
  by(blast intro!: inheritedI boundedUn[symmetric] boundedIncLevel[symmetric]
    boundedInsert[symmetric] boundedEmpty)


subsection "founded"

definition
  founded :: "['a ⇒ 'a set,'a ⇒ bool,(nat * 'a) set] ⇒ bool" where
  "founded subs Pred = (%A. !(n,delta):A. terminal subs delta ⟶ Pred delta)"

lemma foundedD: "founded subs P (tree subs delta) ⟹ terminal subs delta ⟹ P delta"
  by(simp add: treeEquation [of _ delta] founded_def)

lemma foundedMono: "⟦founded subs P A; ∀x. P x ⟶ Q x⟧ ⟹ founded subs Q A"
  by (auto simp: founded_def)

lemma foundedSubs: "founded subs P (tree subs Γ) ⟹ sigma ∈ subs Γ ⟹ founded subs P (tree subs sigma)"
  using tree1Eq by (fastforce simp: founded_def)


subsection "Inherited Properties- founded"

lemma foundedInsert: "¬ terminal subs delta ⟹ founded subs P (insert (n,delta) B) = (founded subs P B)"
  by (simp add: terminal_def founded_def) 

lemma foundedUn: "(founded subs P (A Un B)) = (founded subs P A ∧ founded subs P B)"
  by(force simp add: founded_def)

lemma foundedIncLevel: "founded subs P (incLevel ` A) = (founded subs P A)"
  by (simp add: case_prod_unfold founded_def incLevel_def)

lemma foundedEmpty: "founded subs P {}"
  by(auto simp add: founded_def)

lemma inheritedFounded: "inherited subs (founded subs P)"
  by (simp add: foundedEmpty foundedIncLevel foundedInsert foundedUn inherited_def)


subsection "Inherited Properties- finite"

lemma finiteUn: "finite (A Un B) = (finite A ∧ finite B)"
  by simp

lemma finiteIncLevel: "finite (incLevel ` A) = finite A"
  by (meson finite_imageD finite_imageI injIncLevel inj_on_subset subset_UNIV)

lemma inheritedFinite: "inherited subs finite"
  by (simp add: finiteIncLevel inherited_def)



subsection "path: follows a failing inherited property through tree"

definition
  failingSub :: "['a ⇒ 'a set,(nat * 'a) set ⇒ bool,'a] ⇒ 'a" where
  "failingSub subs P γ ≡ (SOME sigma. (sigma:subs γ ∧ ~P(tree subs sigma)))"

lemma failingSubProps: 
  "⟦inherited subs P; ¬ P (tree subs γ); ¬ terminal subs γ; fans subs⟧
   ⟹ failingSub subs P γ ∈ subs γ ∧ ¬ P (tree subs (failingSub subs P γ))"
  unfolding failingSub_def
  by (metis (mono_tags, lifting) inheritedPropagateEq some_eq_ex)

lemma failingSubFailsI: 
  "⟦inherited subs P; ¬ P (tree subs γ); ¬ terminal subs γ; fans subs⟧
   ⟹ ¬ P (tree subs (failingSub subs P γ))"
  by (simp add: failingSubProps)

lemmas failingSubFailsE = failingSubFailsI[THEN notE]

lemma failingSubSubs: 
  "⟦inherited subs P; ¬ P (tree subs γ); ¬ terminal subs γ; fans subs⟧
    ⟹ failingSub subs P γ ∈ subs γ"
  by (simp add: failingSubProps)


primrec path :: "['a ⇒ 'a set,'a,(nat * 'a) set ⇒ bool,nat] ⇒ 'a"
where
  path0:   "path subs γ P 0       = γ"
| pathSuc: "path subs γ P (Suc n) = (if terminal subs (path subs γ P n)
                                          then path subs γ P n
                                          else failingSub subs P (path subs γ P n))"

lemma pathFailsP: 
  "⟦inherited subs P; fans subs; ¬ P (tree subs γ)⟧
    ⟹ ¬ P (tree subs (path subs γ P n))"
  by (induction n) (simp_all add: failingSubProps)

lemmas PpathE = pathFailsP[THEN notE]

lemma pathTerminal:
  "⟦inherited subs P; fans subs; terminal subs γ⟧
   ⟹ terminal subs (path subs γ P n)"
  by (induct n, simp_all)

lemma pathStarts:  "path subs γ P 0 = γ"
  by simp

lemma pathSubs: 
  "⟦inherited subs P; fans subs; ¬ P (tree subs γ); ¬ terminal subs (path subs γ P n)⟧
    ⟹ path subs γ P (Suc n) ∈ subs (path subs γ P n)"
  by (metis PpathE failingSubSubs pathSuc)

lemma pathStops: "terminal subs (path subs γ P n) ⟹ path subs γ P (Suc n) = path subs γ P n"
  by simp


subsection "Branch"

definition
  branch :: "['a ⇒ 'a set,'a,nat ⇒ 'a] ⇒ bool" where
  "branch subs Γ f ⟷ f 0 = Γ
    ∧ (!n . terminal subs (f n) ⟶ f (Suc n) = f n)
    ∧ (!n . ¬ terminal subs (f n) ⟶ f (Suc n) ∈ subs (f n))"

lemma branch0: "branch subs Γ f ⟹ f 0 = Γ"
  by (simp add: branch_def)

lemma branchStops: "branch subs Γ f ⟹ terminal subs (f n) ⟹ f (Suc n) = f n"
  by (simp add: branch_def)

lemma branchSubs: "branch subs Γ f ⟹ ¬ terminal subs (f n) ⟹ f (Suc n) ∈ subs (f n)"
  by (simp add: branch_def)

lemma branchI: "⟦f 0 = Γ;
  ∀n . terminal subs (f n) ⟶ f (Suc n) = f n;
  ∀n . ¬ terminal subs (f n) ⟶ f (Suc n) ∈ subs (f n)⟧ ⟹ branch subs Γ f"
  by (simp add: branch_def)

lemma branchTerminalPropagates: "branch subs Γ f ⟹ terminal subs (f m) ⟹ terminal subs (f (m + n))"
  by (induct n, simp_all add: branchStops)

lemma branchTerminalMono: 
  "branch subs Γ f ⟹ m < n ⟹ terminal subs (f m) ⟹ terminal subs (f n)"
  by (metis branchTerminalPropagates
      canonically_ordered_monoid_add_class.lessE)

lemma branchPath:
      "⟦inherited subs P; fans subs; ¬ P(tree subs γ)⟧
       ⟹ branch subs γ (path subs γ P)"
  by(auto intro!: branchI pathStarts pathSubs pathStops)



subsection "failing branch property: abstracts path defn"

lemma failingBranchExistence:  
  "⟦inherited subs P; fans subs; ~P(tree subs γ)⟧
  ⟹ ∃f . branch subs γ f ∧ (∀n . ¬ P(tree subs (f n)))"
  by (metis PpathE branchPath)

definition
  infBranch :: "['a ⇒ 'a set,'a,nat ⇒ 'a] ⇒ bool" where
  "infBranch subs Γ f ⟷ f 0 = Γ ∧ (∀n. f (Suc n) ∈ subs (f n))"

lemma infBranchI: "⟦f 0 = Γ; ∀n . f (Suc n) ∈ subs (f n)⟧ ⟹ infBranch subs Γ f"
  by (simp add: infBranch_def)


subsection "Tree induction principles"

  ― ‹we work hard to use nothing fancier than induction over naturals›

lemma boundedTreeInduction':
 "⟦ fans subs;
    ∀delta. ¬ terminal subs delta ⟶ (∀sigma ∈ subs delta. P sigma) ⟶ P delta ⟧
  ⟹ ∀Γ. boundedBy m (tree subs Γ) ⟶  founded subs P (tree subs Γ) ⟶ P Γ"
proof (induction m)
  case 0
  then show ?case by (metis boundedBy0 empty_iff tree.tree0)
next
  case (Suc m)
  then show ?case by (metis boundedBySuc foundedD foundedSubs)
qed
  
 
  ― ‹tjr tidied and introduced new lemmas›

lemma boundedTreeInduction:
   "⟦fans subs;
     bounded (tree subs Γ); founded subs P (tree subs Γ);
  ⋀delta. ⟦¬ terminal subs delta; (∀sigma ∈ subs delta. P sigma)⟧ ⟹ P delta
  ⟧ ⟹ P Γ"
  by (metis boundedTreeInduction' bounded_def)

lemma boundedTreeInduction2:
 "⟦fans subs;
    ∀delta. (∀sigma ∈ subs delta. P sigma) ⟶ P delta⟧
  ⟹ boundedBy m (tree subs Γ) ⟶ P Γ"
proof (induction m arbitrary: Γ)
  case 0
  then show ?case by (metis boundedBy0 empty_iff tree.tree0)
next
  case (Suc m)
  then show ?case by (metis boundedBySuc)
qed

end