section ‹Prover›

theory Prover imports "Abstract_Completeness.Abstract_Completeness" Encoding Fair_Stream begin

function eff :: ‹rule → sequent → (sequent fset) option› where
  ‹eff Idle (A, B) = Some {| (A, B) |}›
| ‹eff (Axiom P ts) (A, B) = (if \‡P ts [∈] A ∧ \‡P ts [∈] B then Some {||} else None)›
| ‹eff FlsL (A, B) = (if \⊥ [∈] A then Some {||} else None)›
| ‹eff FlsR (A, B) = (if \⊥ [∈] B then Some {| (A, B [÷] \⊥) |} else None)›
| ‹eff (ImpL p q) (A, B) = (if (p \⟶ q) [∈] A then
 Some {| (A [÷] (p \⟶ q), p # B), (q # A [÷] (p \⟶ q), B) |} else None)›
| ‹eff (ImpR p q) (A, B) = (if (p \⟶ q) [∈] B then
 Some {| (p # A, q # B [÷] (p \⟶ q)) |} else None)›
| ‹eff (UniL t p) (A, B) = (if \∀p [∈] A then Some {| (⟨t⟩p # A, B) |} else None)›
| ‹eff (UniR p) (A, B) = (if \∀p [∈] B then
 Some {| (A, ⟨#(fresh (A @ B))⟩p # B [÷] \∀p) |} else None)›
  by pat_completeness auto
termination by (relation ‹measure size›) standard

definition rules :: ‹rule stream› where
  ‹rules ≡ fair_stream rule_of_nat›

lemma UNIV_rules: ‹sset rules = UNIV›
  unfolding rules_def using UNIV_stream surj_rule_of_nat .

interpretation RuleSystem ‹λr s ss. eff r s = Some ss› rules UNIV
  by unfold_locales (auto simp: UNIV_rules intro: exI[of _ Idle])

lemma per_rules':
  assumes ‹enabled r (A, B)› ‹¬ enabled r (A', B')› ‹eff r' (A, B) = Some ss'› ‹(A', B') |∈| ss'›
  shows ‹r' = r›
  using assms by (cases r r' rule: rule.exhaust[case_product rule.exhaust])
    (unfold enabled_def, auto split: if_splits)

lemma per_rules: ‹per r›
  unfolding per_def UNIV_rules using per_rules' by fast

interpretation PersistentRuleSystem ‹λr s ss. eff r s = Some ss› rules UNIV
  using per_rules by unfold_locales

definition ‹prover ≡ mkTree rules›

end