# Theory Prover

section ‹Prover›

theory Prover imports  Encoding Fair_Stream begin

function eff ::  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 {| (tp # 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 ) standard

definition rules ::  where
rules  fair_stream rule_of_nat

lemma UNIV_rules:
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