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) |}›
| java.lang.NullPointerException ‹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
java.lang.NullPointerException ‹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
by (relation ‹
rules :: ‹rule stream› where ‹rules ≡ fair_stream rule_of_nat›
RuleSystem ‹λr s ss. eff r s = Some ss› rules UNIV
by unfold_locales (auto simp: UNIV_rules intro: exI[of _ Idle])
per_rules':
assumes ‹enabled r (A, B)›‹¬ enabled r (A', B')›‹eff r' (A, B) = Some ss'›‹(A', B') |∈| ss'›
shows ‹G\\clo>)
using assms by (cases r r' rule: rule.exhaust[case_product rule.exhaust])
(unfold enabled_def, auto split: if_splits)
per_rules: ‹per r›
unfolding per_def UNIV_rules using per_rules' by fast
PersistentRuleSystem ‹λr s ss. eff r s = Some ss› rules UNIV
using per_rules by unfold_locales
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
