Theorem: is_nullable_def (FOL/Parsing/Brzozowski.lean)

State before:
α : Type
e : RegExp α
⊢ e.is_nullable ↔ [] ∈ RegExp.languageOf α e
Tactic:
induction e
State after:
case char
α : Type
a✝ : α
⊢ (RegExp.char a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a✝)

case epsilon
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon

case zero
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero

case union
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.union a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.union a✝)

case concat
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.concat a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.concat a✝)

case closure
α : Type
a✝ : RegExp α
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ a✝.closure.is_nullable ↔ [] ∈ RegExp.languageOf α a✝.closure

State before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a)
Tactic:
case char a =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
State after:
no goals

State before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
case epsilon =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
State after:
no goals

State before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero
Tactic:
case zero =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
State after:
no goals

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.union s)
Tactic:
case union r s r_ih s_ih =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
  simp only [r_ih]
  simp only [s_ih]
State after:
no goals

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.concat s)
Tactic:
case concat r s r_ih s_ih =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
  simp only [r_ih]
  simp only [s_ih]
State after:
no goals

State before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α e.closure
Tactic:
case closure e _ =>
  simp only [equiv_language_of_closure]
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
State after:
no goals

State before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a)
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ {[a]}

State before:
α : Type
a : α
⊢ (RegExp.char a).is_nullable ↔ [] ∈ {[a]}
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
a : α
⊢ False ↔ [] ∈ {[a]}

State before:
α : Type
a : α
⊢ False ↔ [] ∈ {[a]}
Tactic:
simp
State after:
no goals

State before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ {[]}

State before:
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ {[]}
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
⊢ True ↔ [] ∈ {[]}

State before:
α : Type
⊢ True ↔ [] ∈ {[]}
Tactic:
simp
State after:
no goals

State before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ ∅

State before:
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ ∅
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
⊢ False ↔ [] ∈ ∅

State before:
α : Type
⊢ False ↔ [] ∈ ∅
Tactic:
simp
State after:
no goals

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.union s)
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
simp
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Tactic:
simp only [r_ih]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
Tactic:
simp only [s_ih]
State after:
no goals

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.concat s)
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔
    [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔
    [] ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Tactic:
simp
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s
Tactic:
simp only [r_ih]
State after:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s

State before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s
Tactic:
simp only [s_ih]
State after:
no goals

State before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α e.closure
Tactic:
simp only [equiv_language_of_closure]
State after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.epsilon.union (e.concat e.closure))

State before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.epsilon.union (e.concat e.closure))
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}

State before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Tactic:
simp only [RegExp.is_nullable]
State after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ True ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}

State before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ True ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Tactic:
simp
State after:
no goals