theory Formula
imports
"Abstract-Rewriting.Abstract_Rewriting"
TRS.Trs_Impl
First_Order_Terms.Option_Monad
Sorted_Algebra
begin
type_synonym ('v,'t,'d) valuation = "'v × 't ⇒ 'd"
datatype 'a formula =
Atom "'a"
| NegAtom "'a"
| Conjunction "'a formula list"
| Disjunction "'a formula list"
syntax "_list_all" :: "pttrn ⇒ 'a list ⇒ 'b ⇒ 'b" ("(3⋀⇩f _←_. _)" [0, 51, 10] 10)
translations "⋀⇩f x←xs. b" ⇌ "CONST Conjunction (CONST map (λx. b) xs)"
syntax "_list_exists" :: "pttrn ⇒ 'a list ⇒ 'b ⇒ 'b" ("(3⋁⇩f _←_. _)" [0, 51, 10] 10)
translations "⋁⇩f x←xs. b" ⇌ "CONST Disjunction (CONST map (λx. b) xs)"
instantiation formula :: (showl) showl
begin
fun showsl_formula where
"showsl_formula (Atom a) = showsl a"
| "showsl_formula (NegAtom a) = showsl_lit (STR ''! ('') o showsl a o showsl_lit (STR '')'')"
| "showsl_formula (Conjunction a) = showsl_list_gen id (STR ''TRUE'') (STR ''('') (STR '' & '') (STR '')'') (map showsl a)"
| "showsl_formula (Disjunction a) = showsl_list_gen id (STR ''FALSE'') (STR ''('') (STR '' | '') (STR '')'') (map showsl a)"
definition "showsl_list (xs :: 'a formula list) = default_showsl_list showsl xs"
instance ..
end
fun isLit where "isLit (Atom _) = True" | "isLit (NegAtom _) = True" | "isLit _ = False"
abbreviation disj_atoms :: "'a list ⇒ 'a formula" where
"disj_atoms as ≡ Disjunction (map Atom as)"
abbreviation conj_atoms :: "'a list ⇒ 'a formula" where
"conj_atoms as ≡ Conjunction (map Atom as)"
inductive is_conj_lits
where "(⋀φ. φ ∈ set φs ⟹ isLit φ) ⟹ is_conj_lits (Conjunction φs)"
inductive is_clause
where "(⋀φ. φ ∈ set φs ⟹ isLit φ) ⟹ is_clause (Disjunction φs)"
lemma is_clause_code[code]: "is_clause (Disjunction ls) = (∀ l ∈ set ls. isLit l)"
"is_clause (Conjunction xs) = False"
"is_clause (Atom a) = False"
"is_clause (NegAtom a) = False"
by (auto simp: is_clause.simps)
fun is_neg_atom where "is_neg_atom (NegAtom _) = True" | "is_neg_atom _ = False"
inductive is_neg_atom_clause
where "(⋀φ. φ ∈ set φs ⟹ is_neg_atom φ) ⟹ is_neg_atom_clause (Disjunction φs)"
lemma is_neg_atom_clause[code]: "is_neg_atom_clause (Disjunction ls) = (∀ l ∈ set ls. is_neg_atom l)"
"is_neg_atom_clause (Conjunction xs) = False"
"is_neg_atom_clause (Atom a) = False"
"is_neg_atom_clause (NegAtom a) = False"
by (auto simp: is_neg_atom_clause.simps)
fun is_Atom where "is_Atom (Atom _) = True" | "is_Atom _ = False"
fun get_Atom where "get_Atom (Atom a) = a" | "get_Atom (NegAtom a) = a"
inductive is_conj_atoms
where "(⋀φ. φ ∈ set φs ⟹ is_Atom φ) ⟹ is_conj_atoms (Conjunction φs)"
inductive is_cnf
where "(⋀φ. φ ∈ set φs ⟹ is_clause φ) ⟹ is_cnf (Conjunction φs)"
abbreviation form_False :: "'a formula" ("False⇩f")
where "form_False ≡ Disjunction []"
abbreviation form_True :: "'a formula" ("True⇩f")
where "form_True ≡ Conjunction []"
fun form_not :: "'a formula ⇒ 'a formula" ("¬⇩f _" [43] 43)
where "(¬⇩f Atom a) = NegAtom a"
| "(¬⇩f NegAtom a) = Atom a"
| "(¬⇩f Conjunction φs) = Disjunction (map form_not φs)"
| "(¬⇩f Disjunction φs) = Conjunction (map form_not φs)"
fun form_and :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∧⇩f" 42)
where "(True⇩f ∧⇩f ψ) = ψ"
| "(φ ∧⇩f True⇩f) = φ"
| "(Conjunction φs ∧⇩f Conjunction ψs) = Conjunction (φs @ ψs)"
| "(Conjunction φs ∧⇩f ψ) = Conjunction (φs @ [ψ])"
| "(φ ∧⇩f Conjunction ψs) = Conjunction (φ # ψs)"
| "(φ ∧⇩f ψ) = Conjunction [φ,ψ]"
fun form_or :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∨⇩f" 41)
where "(False⇩f ∨⇩f ψ) = ψ"
| "(φ ∨⇩f False⇩f) = φ"
| "(Disjunction φs ∨⇩f Disjunction ψs) = Disjunction (φs @ ψs)"
| "(Disjunction φs ∨⇩f ψ) = Disjunction (φs @ [ψ])"
| "(φ ∨⇩f Disjunction ψs) = Disjunction (φ # ψs)"
| "(φ ∨⇩f ψ) = Disjunction [φ,ψ]"
fun simplify
where "simplify (Disjunction (φ#φs)) = (simplify φ ∨⇩f simplify (Disjunction φs))"
| "simplify (Conjunction [φ]) = simplify φ"
| "simplify (Conjunction (φ#φs)) = (simplify φ ∧⇩f simplify (Conjunction φs))"
| "simplify φ = φ"
lemma is_Atom_neg[simp]: "is_Atom (¬⇩f f) = is_neg_atom f" by (cases f, auto)
lemma is_conj_atoms_neg[simp]: "is_conj_atoms (¬⇩f φ) = is_neg_atom_clause φ"
by (cases φ, auto simp: is_conj_atoms.simps is_neg_atom_clause.simps)
fun cnf_form_or :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∨⇩c⇩f" 41) where
"(Conjunction φs ∨⇩c⇩f Conjunction ψs) = Conjunction [φ ∨⇩f ψ . φ ← φs, ψ ← ψs]"
| "(φ ∨⇩c⇩f ψ) = (φ ∨⇩f ψ)"
lemma map_form_and: "map_formula f (φ ∧⇩f ψ) = (map_formula f φ ∧⇩f map_formula f ψ)"
by (cases "(φ,ψ)" rule:form_and.cases, auto)
lemma map_form_or: "map_formula f (φ ∨⇩f ψ) = (map_formula f φ ∨⇩f map_formula f ψ)"
by (cases "(φ,ψ)" rule:form_or.cases, auto)
lemma map_form_not: "map_formula f (¬⇩f φ) = (¬⇩f map_formula f φ)"
by (induct φ, auto)
text ‹The internal constructs are less useful.›
declare form_and.simps[simp del] form_or.simps[simp del]
abbreviation form_imp (infixr "⟶⇩f" 40) where "(φ ⟶⇩f ψ) ≡ ¬⇩f φ ∨⇩f ψ"
fun form_all
where "form_all [] = True⇩f"
| "form_all (φ#φs) = (φ ∧⇩f form_all φs)"
fun form_ex
where "form_ex [] = False⇩f"
| "form_ex (φ#φs) = (φ ∨⇩f form_ex φs)"
fun form_cnf_ex
where "form_cnf_ex [] = Conjunction [False⇩f]"
| "form_cnf_ex (φ#φs) = (φ ∨⇩c⇩f form_cnf_ex φs)"
fun flatten where
"flatten (Conjunction φs) = form_all (map flatten φs)"
| "flatten (Disjunction φs) = form_cnf_ex (map flatten φs)"
| "flatten φ = Conjunction [Disjunction [φ]]"
fun conjuncts where "conjuncts (Conjunction φs) = φs" | "conjuncts φ = [φ]"
fun disjuncts where "disjuncts (Disjunction φs) = φs" | "disjuncts φ = [φ]"
fun triv_unsat :: "'a formula ⇒ bool"
where "triv_unsat (Conjunction φs) = (∀φ ∈ set φs. triv_unsat φ)"
| "triv_unsat _ = False"
locale formula =
fixes atom :: "'atom ⇒ bool"
and assignment :: "'assignment ⇒ bool"
and eval_true :: "'assignment ⇒ 'atom ⇒ bool"
begin
abbreviation "Assignments ≡ Collect assignment"
subsection ‹Well-formedness›
fun formula :: "'atom formula ⇒ bool" where
"formula (Atom a) = atom a"
| "formula (NegAtom a) = atom a"
| "formula (Conjunction φs) = (∀φ ∈ set φs. formula φ)"
| "formula (Disjunction φs) = (∀φ ∈ set φs. formula φ)"
lemma formula_and[simp]: "formula (φ ∧⇩f ψ) ⟷ formula φ ∧ formula ψ"
by (cases "(φ,ψ)" rule: form_and.cases, auto simp: form_and.simps)
lemma formula_or[simp]: "formula (φ ∨⇩f ψ) ⟷ formula φ ∧ formula ψ"
by (cases "(φ,ψ)" rule: form_or.cases, auto simp: form_or.simps)
lemma formula_not[simp]: "formula (¬⇩f φ) ⟷ formula φ" by (induct φ; auto)
lemma formula_all[simp]: "formula (form_all φs) ⟷ (∀φ ∈ set φs. formula φ)"
by (induct φs, auto)
lemma formula_ex[simp]: "formula (form_ex φs) ⟷ (∀φ ∈ set φs. formula φ)"
by (induct φs, auto)
lemma formula_cnf_or[simp]: "formula φ ⟹ formula ψ ⟹ formula (φ ∨⇩c⇩f ψ)"
by (cases φ; cases ψ, auto)
lemma formula_cnf_ex[simp]: "(∀φ ∈ set φs. formula φ) ⟹ formula (form_cnf_ex φs)"
by (induct φs, auto)
lemma formula_flatten[simp]: "formula φ ⟹ formula (flatten φ)"
by (induct φ rule: flatten.induct, auto simp: Let_def)
lemma formula_simplify[simp]: "formula (simplify φ) ⟷ formula φ"
by (induct φ rule: simplify.induct, auto)
lemma isLit_negate[simp]: "isLit (¬⇩f f) = isLit f" by (cases f, auto)
lemma is_conj_lits_negate[simp]: "is_conj_lits (¬⇩f f) = is_clause f"
by (cases f, auto simp: is_clause.simps is_conj_lits.simps)
lemma is_cnf_form_and[simp]: "is_cnf f ⟹ is_cnf g ⟹ is_cnf (f ∧⇩f g)"
by (cases "(f,g)" rule: form_and.cases; auto simp: is_cnf.simps form_and.simps)
lemma is_clause_form_or[simp]: "is_clause f ⟹ is_clause g ⟹ is_clause (f ∨⇩f g)"
by (cases "(f,g)" rule: form_or.cases; auto simp: is_clause.simps form_or.simps)
lemma is_cnf_cnf_form_or[simp]: "is_cnf f ⟹ is_cnf g ⟹ is_cnf (f ∨⇩c⇩f g)"
by (cases f; cases g; auto simp: is_cnf.simps form_and.simps)
lemma is_cnf_form_True[simp]: "is_cnf True⇩f"
by (simp add: is_cnf.simps)
lemma is_cnf_form_all[simp]: "(⋀ f. f ∈ set fs ⟹ is_cnf f) ⟹ is_cnf (form_all fs)"
by(induct fs, auto)
lemma is_cnf_form_cnf_ex[simp]: "(⋀ f. f ∈ set fs ⟹ is_cnf f) ⟹ is_cnf (form_cnf_ex fs)"
by(induct fs, auto, auto simp: is_cnf.simps is_clause.simps)
lemma is_cnf_Conjunction[simp]: "is_cnf (Conjunction fs) = (∀ f ∈ set fs. is_clause f)"
by (auto simp: is_cnf.simps)
lemma is_clause_Disjunction[simp]: "is_clause (Disjunction fs) = (∀ f ∈ set fs. isLit f)"
by (auto simp: is_clause.simps)
lemma is_cnf_flatten[simp]:
"is_cnf (flatten (φ :: ('f,'v,'t) exp formula))"
by (induct φ rule: flatten.induct, auto intro!: is_cnf_form_all is_cnf_form_cnf_ex)
subsection ‹Valuation›
context fixes α :: "'assignment" begin
fun satisfies :: "'atom formula ⇒ bool" where
"satisfies (Atom a) ⟷ eval_true α a"
| "satisfies (NegAtom a) ⟷ ¬ eval_true α a"
| "satisfies (Conjunction φs) ⟷ (∀φ ∈ set φs. satisfies φ)"
| "satisfies (Disjunction φs) ⟷ (∃φ ∈ set φs. satisfies φ)"
lemma satisfiesI[intro]:
"eval_true α a ⟹ satisfies (Atom a)"
"¬ eval_true α a ⟹ satisfies (NegAtom a)"
"(⋀φ. φ ∈ set φs ⟹ satisfies φ) ⟹ satisfies (Conjunction φs)"
"⋀φ. φ ∈ set φs ⟹ satisfies φ ⟹ satisfies (Disjunction φs)" by auto
lemma form_True[simp]: "satisfies True⇩f" by auto
lemma satisfies_NegAtom[simp]: "satisfies (NegAtom a) ⟷ ¬ satisfies (Atom a)" by simp
lemma satisfies_and[simp]: "satisfies (φ ∧⇩f ψ) ⟷ satisfies φ ∧ satisfies ψ"
by (cases "(φ,ψ)" rule:form_and.cases, auto simp: form_and.simps)
lemma satisfies_or[simp]: "satisfies (φ ∨⇩f ψ) ⟷ satisfies φ ∨ satisfies ψ"
by (cases "(φ,ψ)" rule:form_or.cases, auto simp: form_or.simps)
lemma satisfies_not[simp]: "satisfies (¬⇩f φ) ⟷ ¬ satisfies φ"
by (induct φ, auto)
lemma satisfies_all[simp]:
"satisfies (form_all φs) ⟷ (∀φ ∈ set φs. satisfies φ)" by (induct φs, auto)
lemma satisfies_ex[simp]:
"satisfies (form_ex φs) ⟷ (∃φ ∈ set φs. satisfies φ)" by (induct φs, auto)
end
notation satisfies (infix "⊨" 40)
subsection ‹Language›
definition Language where "Language φ = {α ∈ Assignments. α ⊨ φ}"
notation Language ("ℒ")
lemma Language_dom [dest]: assumes "α ∈ ℒ φ" shows "assignment α"
using assms by (auto simp: Language_def)
lemma Language_simps[simp]:
"ℒ False⇩f = {}"
"ℒ True⇩f = Assignments"
"ℒ (φ ∧⇩f ψ) = ℒ φ ∩ ℒ ψ"
"ℒ (φ ∨⇩f ψ) = ℒ φ ∪ ℒ ψ"
"ℒ (NegAtom a) = Assignments - ℒ (Atom a)"
"ℒ (Conjunction (φ#φs)) = ℒ φ ∩ ℒ (Conjunction φs)"
"ℒ (Disjunction (φ#φs)) = ℒ φ ∪ ℒ (Disjunction φs)" by (auto simp: Language_def)
lemma Language_Conjunction[simp]: "ℒ (Conjunction φs) = Assignments ∩ (⋂φ ∈ set φs. ℒ φ)" by (induct φs, auto)
lemma Language_Disjunction[simp]: "ℒ (Disjunction φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)
lemma Language_not[simp]: "ℒ (¬⇩f φ) = Assignments - ℒ φ" by (induct φ, auto)
lemma Language_all[simp]: "ℒ (form_all φs) = Assignments ∩ (⋂φ ∈ set φs. ℒ φ)" by (induct φs, auto)
lemma Language_ex[simp]: "ℒ (form_ex φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)
lemma all_conjuncts[simplified,simp]: "ℒ (form_all (conjuncts φ)) = ℒ φ" by (cases φ, auto)
lemma formula_conjuncts[simplified,simp]: "(∀φ' ∈ set (conjuncts φ). formula φ') = formula φ" by (cases φ, auto)
lemma ex_disjuncts[simplified,simp]: "ℒ (form_ex (disjuncts φ)) = ℒ φ" by (cases φ, auto)
lemma formula_disjuncts[simplified,simp]: "(∀φ' ∈ set (disjuncts φ). formula φ') = formula φ" by (cases φ, auto)
lemma Language_cnf_form_or[simp]: "ℒ (φ ∨⇩c⇩f ψ) = ℒ φ ∪ ℒ ψ"
by (cases φ; cases ψ, auto)
lemma Language_cnf_ex[simp]: "ℒ (form_cnf_ex φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)
lemma Langage_flatten[simp]: "ℒ (flatten φ) = ℒ φ"
by (induct φ rule: flatten.induct, auto simp: Let_def)
lemma Language_simplify[simp]: "ℒ (simplify φ) = ℒ φ"
by (induct φ rule: simplify.induct, auto)
lemma satisfies_Language: assumes "assignment α" shows "α ⊨ φ ⟷ α ∈ ℒ φ"
using assms by (auto simp: Language_def)
definition implies :: "'atom formula ⇒ 'atom formula ⇒ bool" where
"implies φ ψ ≡ ∀α. assignment α ⟶ α ⊨ φ ⟶ α ⊨ ψ"
notation implies (infix "⟹⇩f" 41)
lemma impliesI[intro]:
assumes "⋀ α. assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ"
shows "φ ⟹⇩f ψ" using assms by (auto simp: implies_def)
lemma impliesD[dest]:
assumes "φ ⟹⇩f ψ"
shows "assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ"
using assms by (auto simp: implies_def)
lemma impliesE[elim]:
assumes "φ ⟹⇩f ψ" "(⋀α. assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ) ⟹ P"
shows P using assms by (auto simp: implies_def)
lemma implies_Language[simp]: "(φ ⟹⇩f ψ) ⟷ ℒ φ ⊆ ℒ ψ"
by (auto simp add: implies_def satisfies_Language)
definition equivalent where "equivalent φ ψ ≡ φ ⟹⇩f ψ ∧ ψ ⟹⇩f φ"
notation equivalent (infix "⟺⇩f" 40)
lemma equivalentI[intro]: assumes "φ ⟹⇩f ψ" and "ψ ⟹⇩f φ" shows "φ ⟺⇩f ψ"
using assms by (auto simp: equivalent_def)
lemma equivalentE[elim]: assumes "φ ⟺⇩f ψ" and "(φ ⟹⇩f ψ) ⟹ (ψ ⟹⇩f φ) ⟹ thesis" shows thesis
using assms by (auto simp: equivalent_def)
lemma equivalent_Language[simp]: "φ ⟺⇩f ψ ⟷ ℒ φ = ℒ ψ" by auto
definition valid where
"(valid φ) = (∀ α. assignment α ⟶ α ⊨ φ)"
notation valid ("⊨⇩f _" [40]40)
lemma validI[intro]:
assumes "⋀ α. assignment α ⟹ α ⊨ φ"
shows "⊨⇩f φ" using assms by (auto simp: valid_def)
lemma validD[dest]:
assumes "⊨⇩f φ"
shows "assignment α ⟹ α ⊨ φ"
using assms by (auto simp: valid_def)
lemma valid_Language:
"⊨⇩f φ ⟷ ℒ φ = Assignments" by (auto simp: satisfies_Language)
lemma valid_simplify [simp]: "⊨⇩f simplify φ ⟷ ⊨⇩f φ"
by (simp add: valid_Language)
lemma valid_flatten [simp]: "⊨⇩f flatten φ ⟷ ⊨⇩f φ"
by (simp add: valid_Language)
lemma valid_implies_trans [trans]:
assumes "⊨⇩f φ" and "φ ⟹⇩f ψ" shows "⊨⇩f ψ"
using assms by (auto simp: valid_Language)
lemma valid_equivalent_trans [trans]:
assumes "⊨⇩f φ" and "φ ⟺⇩f ψ" shows "⊨⇩f ψ"
using assms by (auto simp: valid_Language)
lemma implies_trans [trans]:
assumes "φ ⟹⇩f ψ" and "ψ ⟹⇩f ρ" shows "φ ⟹⇩f ρ"
using assms by auto
lemma implies_equivalent_trans [trans]:
assumes "φ ⟹⇩f ψ" and "ψ ⟺⇩f ρ" shows "φ ⟹⇩f ρ"
using assms by auto
lemma equivalent_implies_trans [trans]:
assumes "φ ⟺⇩f ψ" and "ψ ⟹⇩f ρ" shows "φ ⟹⇩f ρ"
using assms by (auto dest: implies_trans)
end
locale showsl_formula =
fixes showsl_atom :: "'a ⇒ showsl"
begin
fun showsl_formula :: "'a formula ⇒ showsl" where
"showsl_formula (Atom a) = showsl_atom a"
| "showsl_formula (NegAtom a) = showsl (STR ''! ('') o showsl_atom a o showsl (STR '')'')"
| "showsl_formula (Conjunction fs) = (let ss = map showsl_formula fs in
showsl_list_gen id (STR ''True'') (STR ''Conj['') (STR '', '') (STR '']'') ss)"
| "showsl_formula (Disjunction fs) = (let ss = map showsl_formula fs in
showsl_list_gen id (STR ''False'') (STR ''Disj['') (STR '', '') (STR '']'') ss)"
end
subsection ‹Formulas over terms›
fun vars_formula :: "('f,'v) term formula ⇒ 'v set"
where "vars_formula (Atom a) = vars_term a"
| "vars_formula (NegAtom a) = vars_term a"
| "vars_formula (Conjunction φs) = (⋃(vars_formula ` set φs))"
| "vars_formula (Disjunction φs) = (⋃(vars_formula ` set φs))"
fun vars_formula_list :: "('f,'v) term formula ⇒ 'v list"
where "vars_formula_list (Atom a) = vars_term_list a"
| "vars_formula_list (NegAtom a) = vars_term_list a"
| "vars_formula_list (Conjunction φs) = concat (map vars_formula_list φs)"
| "vars_formula_list (Disjunction φs) = concat (map vars_formula_list φs)"
fun in_vars_formula :: "'v ⇒ ('f,'v) term formula ⇒ bool"
where "in_vars_formula x (Atom a) = (x ∈ set (vars_term_list a))"
| "in_vars_formula x (NegAtom a) = (x ∈ set (vars_term_list a))"
| "in_vars_formula x (Conjunction φs) = (∃ φ ∈ set φs. in_vars_formula x φ)"
| "in_vars_formula x (Disjunction φs) = (∃ φ ∈ set φs. in_vars_formula x φ)"
lemma in_vars_formula[code_unfold]: "(x ∈ vars_formula φ) = in_vars_formula x φ"
by (induct φ, auto)
lemma vars_formula_list: "vars_formula φ = set (vars_formula_list φ)"
by (induct φ, auto)
lemma vars_formula_set_formula: "vars_formula φ = ⋃ (vars_term ` set_formula φ)"
by (induct φ, auto)
abbreviation rename_vars_formula :: "('v ⇒ 'w) ⇒ ('f,'v,'t) exp formula ⇒ ('f,'w,'t) exp formula"
where "rename_vars_formula r cls ≡ map_formula (rename_vars r) cls"
adhoc_overloading rename_vars rename_vars_formula
lemma rename_vars_formula_comp[simp]:
"rename_vars f (rename_vars g (φ::('f,'v,'t) exp formula)) = rename_vars (f ∘ g) φ"
by (cases φ, auto simp: formula.map_comp o_def)
locale prelogic =
pre_sorted_algebra where type_fixer = type_fixer
for type_fixer :: "('f×'t×'d) itself"
and Bool_types :: "'t set"
and to_bool :: "'d ⇒ bool"
begin
definition "is_bool e ≡ (∃b ∈ Bool_types. e :⇩f b) ∧ ¬ is_Var e"
lemma is_bool_simps[simp]: "is_bool (Var x) = False"
"is_bool (Fun f es) = (∃b ∈ Bool_types. Fun f es :⇩f b)" by (auto simp: is_bool_def)
abbreviation "BOOL_EXP ≡ Collect is_bool"
sublocale formula is_bool assignment "λα t. to_bool (⟦t⟧α)".
lemma Language_atom[simp]: "ℒ (Atom e) = { α ∈ Assignments. to_bool (⟦e⟧α) }" by (auto simp: Language_def)
lemma is_bool_imp_expression[simp]: "is_bool e ⟹ expression e" unfolding is_bool_def by auto
lemma formula_rename_vars[simp]: "formula (rename_vars r e) = formula e"
proof (induct e)
case (Atom x)
then show ?case by (cases x, auto)
next
case (NegAtom x)
then show ?case by (cases x, auto)
qed auto
lemma formula_rename_vars_map[simp]:
"list_all formula (map (rename_vars r) l) = list_all formula l"
using formula_rename_vars unfolding list_all_def by auto
lemma eval_with_fresh_var[simp]: "xx ∉ vars_term e ⟹ ⟦e⟧ (α(xx:=a)) = ⟦e⟧ α" by auto
lemma satisfies_with_fresh_var[simp]:
assumes fv: "xx ∉ vars_formula φ"
shows "α(xx:=a) ⊨ φ ⟷ α ⊨ φ" by (insert fv, induct φ, auto)
lemma satisfies_rename_vars:
assumes r: "⋀ x t. α (x,t) = β (r x, t)"
shows "β ⊨ (rename_vars r φ) ⟷ α ⊨ φ"
by (induct φ, auto simp: eval_rename_vars[of α, OF r])
definition satisfiable where "satisfiable φ = (∃ α. assignment α ∧ α ⊨ φ)"
end
fun ground_formula where
"ground_formula (Atom a) = ground a"
| "ground_formula (NegAtom a) = ground a"
| "ground_formula (Disjunction fs) = (∀ f ∈ set fs. ground_formula f)"
| "ground_formula (Conjunction fs) = (∀ f ∈ set fs. ground_formula f)"
locale logic = prelogic + sorted_algebra
subsection ‹Checking validity›
type_synonym ('h,'f,'v,'t) logic_checker =
"'h ⇒ ('f,'v,'t) exp formula ⇒ showsl check"
datatype 'h hint =
Default
| Base 'h
| Distribute nat "('h hint list)"
| Erase nat "('h hint)"
| LexStrict "('h hint list)"
| LexWeak "('h hint list)"
primrec showsl_hint where
"showsl_hint Default = showsl_lit (STR '' auto'')"
| "showsl_hint (Base raw) = showsl_lit (STR '' '') o showsl raw"
| "showsl_hint (Distribute i hints) = showsl_lit (STR '' Distribute '') o showsl i o
showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (LexStrict hints) = showsl_lit (STR '' LexStrict'') o
showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (LexWeak hints) = showsl_lit (STR '' LexWeak'') o
showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (Erase i hint) = showsl_lit (STR '' Erase '') o showsl i o showsl_lit (STR '' ['') o showsl_hint hint o showsl_lit (STR '' ]'')"
instantiation hint :: (default) default
begin
definition "default ≡ Default"
instance ..
end
hide_const(open) Default Base Distribute Erase
definition trivial_checker where
"trivial_checker lits = (case partition is_Atom lits of
(as, nas) ⇒ let pos = map get_Atom as; neg = map get_Atom nas
in (∃ a ∈ set pos. a ∈ set neg))"
definition trivial_clause_checker where "trivial_clause_checker f = (case f of Disjunction lits ⇒ trivial_checker lits)"
lemma trivial_checker:
assumes "⋀ l. l ∈ set lits ⟹ isLit l" and "trivial_checker lits"
shows "∃ a. Atom a ∈ set lits ∧ NegAtom a ∈ set lits"
proof -
obtain as nas where part: "partition is_Atom lits = (as,nas)" by force
from assms[unfolded trivial_checker_def part split, simplified]
obtain a where a: "a ∈ set as" "get_Atom a ∈ get_Atom ` set nas" by auto
from partition_filter_conv[of is_Atom lits, unfolded part]
have id: "as = filter is_Atom lits" "nas = filter (λ x. ¬ is_Atom x) lits" by (auto simp: o_def)
from a(1)[unfolded id] have "is_Atom a" and mem: "a ∈ set lits" by auto
then obtain aa where aa: "a = Atom aa" by (cases a, auto)
from a(2)[unfolded aa] obtain na where na: "get_Atom na = aa" "na ∈ set nas" by auto
from na(2)[unfolded id] assms(1) have "¬ is_Atom na" "isLit na" "na ∈ set lits" by auto
with na have "NegAtom aa ∈ set lits" by (cases na, auto)
with mem aa show ?thesis by auto
qed
fun get_disjunctions where
"get_disjunctions (Disjunction phis) = concat (map get_disjunctions phis)"
| "get_disjunctions x = [x]"
fun get_conjunctions where
"get_conjunctions (Conjunction phis) = concat (map get_conjunctions phis)"
| "get_conjunctions x = [x]"
definition check_trivial_implication where
"check_trivial_implication φ ψ =
(∀ phi ∈ set (get_disjunctions φ). let c_phis = get_conjunctions phi in
∃ psi ∈ set (get_disjunctions ψ). ∀ c_psi ∈ set (get_conjunctions psi). c_psi ∈ set c_phis)"
fun trivial_formula where
"trivial_formula (Disjunction φs) = list_ex trivial_formula φs"
| "trivial_formula (Conjunction φs) = list_all trivial_formula φs"
| "trivial_formula _ = False"
context prelogic
begin
lemma get_disjunctions: "(α ⊨ form_ex (get_disjunctions φ)) = (α ⊨ φ)"
by (induct φ, auto)
lemma get_conjunctions: "(α ⊨ form_all (get_conjunctions φ)) = (α ⊨ φ)"
by (induct φ, auto)
lemma check_trivial_implication:
assumes "check_trivial_implication φ ψ" shows "φ ⟹⇩f ψ"
proof
fix α
assume "α ⊨ φ"
then have "α ⊨ form_ex (get_disjunctions φ)" unfolding get_disjunctions .
then obtain phi where phi: "phi ∈ set (get_disjunctions φ)" and sat: "α ⊨ phi" by auto
from assms[unfolded check_trivial_implication_def Let_def, rule_format, OF phi]
obtain psi where psi: "psi ∈ set (get_disjunctions ψ)"
and conj: "⋀ c_psi. c_psi∈set (get_conjunctions psi) ⟹ c_psi ∈ set (get_conjunctions phi)" by auto
{
fix c_psi
assume "c_psi ∈ set (get_conjunctions psi)"
then have mem: "c_psi ∈ set (get_conjunctions phi)" using conj by auto
from sat[folded get_conjunctions[of _ phi]] mem have "α ⊨ c_psi" by auto
}
then have "α ⊨ psi" using get_conjunctions[of _ psi] by auto
then show "α ⊨ ψ" using psi get_disjunctions[of _ ψ] by auto
qed
lemma trivial_formula:
assumes "trivial_formula φ" shows "⊨⇩f φ"
by (insert assms, induct φ, auto simp: list_all_iff list_ex_iff valid_Language)
lemma trivial_clause_checker:
assumes "is_clause φ" and "trivial_clause_checker φ" shows "⊨⇩f φ"
proof -
from assms obtain lits where phi: "φ = Disjunction lits" and lits: "⋀ l. l ∈ set lits ⟹ isLit l"
using is_clause.cases by blast
from assms[unfolded trivial_clause_checker_def phi] have triv: "trivial_checker lits" by auto
from trivial_checker[OF lits this] obtain a where a: "Atom a ∈ set lits" "NegAtom a ∈ set lits" by auto
from split_list[OF a(1)] obtain l1 l2 where lits: "lits = l1 @ Atom a # l2" by auto
from a(2) lits have "NegAtom a ∈ set (l1 @ l2)" by auto
from split_list[OF this] obtain l3 l4 where l12: "l1 @ l2 = l3 @ NegAtom a # l4" by auto
have "set lits = insert (Atom a) (set (l1 @ l2))" unfolding lits by auto
also have "… = insert (Atom a) (insert (NegAtom a) (set l3 ∪ set l4))" unfolding l12 by auto
finally show ?thesis unfolding phi by auto
qed
end
locale pre_logic_checker =
prelogic where type_fixer = "TYPE('f×'t×'d)" +
showsl_formula showsl_atom
for type_fixer :: "('f × 'v :: showl × 't × 'd × 'h :: {default,showl}) itself"
and showsl_atom :: "('f,'v,'t) exp ⇒ showsl"
and logic_checker :: "('h,'f,'v,'t) logic_checker"
and negate_atom :: "('f,'v,'t) exp ⇒ ('f,'v,'t) exp formula"
begin
fun remove_Atom where
"remove_Atom (Conjunction φs) = Conjunction (map remove_Atom φs)"
| "remove_Atom (Disjunction φs) = Disjunction (map remove_Atom φs)"
| "remove_Atom (NegAtom φ) = NegAtom φ"
| "remove_Atom (Atom φ) = (¬⇩f (negate_atom φ))"
definition "check_valid_formula φ ≡
(case flatten φ of Conjunction φs ⇒ check_allm (
λ φ. try (check (trivial_clause_checker φ) (STR ''trivial clause checker failed'')) catch (λ _.
case flatten (remove_Atom φ) of Conjunction φs ⇒ check_allm (logic_checker default) φs)) φs)
<+? (λs. showsl_lit (STR ''problem in checking validity of formula '') o showsl_formula φ o showsl_nl o s)"
fun is_or_and_shape where
"is_or_and_shape (Disjunction [φ1,Conjunction [φ2,φ3]]) = True"
| "is_or_and_shape _ = False"
fun is_conj_shape where
"is_conj_shape [hint1,hint2] (Conjunction [φ1,φ2]) = True"
| "is_conj_shape _ _ = False"
fun is_disj_shape where
"is_disj_shape (hint1#hints) (Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]]) = True"
| "is_disj_shape _ _ = False"
function(sequential) check_formula and check_formula_dist and check_formula_lex_weak and check_formula_lex
where
"check_formula hint.Default φ = check_valid_formula φ"
| "check_formula (hint.Base h) φ = do {
let ψ = remove_Atom (simplify φ);
check (is_neg_atom_clause ψ) (showsl (STR ''base hint given to '') o showsl_formula ψ);
logic_checker h ψ <+? (λ s. showsl (STR ''problem in checking '') o showsl_formula φ o showsl_nl o s)}"
| "check_formula (hint.Erase n hint) φ =
( case φ of formula.Disjunction φs ⇒ do {
let l = length φs;
check (n < l) (showsl (STR ''erase hint at position '') o showsl n o showsl (STR '' while goal is length '') o showsl l);
let pre = take n φs;
let post = drop (Suc n) φs;
check_formula hint (formula.Disjunction (pre @ False⇩f # post))
}
| _ ⇒ error (showsl (STR ''Erase hint to non-Disjunction''))
)"
| "check_formula (hint.Distribute n hints) φ =
( case φ of formula.Disjunction φs ⇒ do {
let l = length φs;
check (n < l) (showsl (STR ''distribute hint at position '') o showsl n o showsl (STR '' while goal is length '') o showsl l);
let pre = take n φs;
let post = drop (Suc n) φs;
case φs ! n of
Conjunction ψs ⇒ check_formula_dist hints pre post ψs
| _ ⇒ error (showsl (STR ''Distribute hint in: ⏎'') o showsl_formula φ o showsl (STR ''⏎ at non-Conjunction position:⏎'') o showsl_formula (φs ! n))
}
| _ ⇒ error (showsl (STR ''Distribute hint for non Disjunction '') o showsl_formula φ)
)"
| "check_formula (hint.LexWeak hints) ψ = (case ψ of
Disjunction (φ#φs) ⇒ check_formula_lex_weak hints φ φs
| _ ⇒ error (showsl (STR ''LexWeak hint applied on '') o showsl_formula ψ))"
| "check_formula (hint.LexStrict hints) ψ = (case ψ of
Disjunction (φ#φs) ⇒ check_formula_lex hints φ φs
| _ ⇒ error (showsl (STR ''LexStrict hint applied on '') o showsl_formula ψ))"
| "check_formula_dist [] pre post [] = succeed"
| "check_formula_dist (h#hs) pre post (φ#φs) =
check_formula h (formula.Disjunction (pre @ φ # post)) ⪢ check_formula_dist hs pre post φs"
| "check_formula_dist _ _ _ _ = error (showsl (STR ''Length mismatch in Distribute hints''))"
| "check_formula_lex_weak [] φ φs =
check (trivial_formula φ) (showsl (STR ''LexWeak base case error: '') o showsl_formula φ)"
| "check_formula_lex_weak (hint#hints) φ φs = (if is_or_and_shape φ then (case φ of
Disjunction [φ1,Conjunction [φ2,φ3]] ⇒ do {
check_formula hint (Disjunction (φ2#φs));
check_formula_lex_weak hints φ3 φs
})
else (case hints of
Nil ⇒ check_formula hint (Disjunction (φ#φs))
| _ ⇒ error (showsl (STR ''LexWeak hint application error''))))"
| "check_formula_lex hints φ φs = (if is_conj_shape hints φ then
(case hints of [hint1,hint2] ⇒ case φ of Conjunction [φ1,φ2] ⇒ do {
check_formula hint1 (Disjunction (φ1#φs));
check_formula hint2 (Disjunction (φ2#φs))
}) else (if is_disj_shape hints φ then
(case hints of hint1#hints2 ⇒ case φ of Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]] ⇒
(case hints2 of
[hint2] ⇒ do {
check_formula hint1 (Disjunction (φ1#φs));
check_formula hint2 (Disjunction (φ2#φs))
}
| _ ⇒ do {
check_formula hint1 (Disjunction (φ3#φs));
check_formula_lex hints2 φ4 φs
}))
else error (showsl (STR ''LexStrict hint application error: '') o
showsl_hint (LexStrict hints) o showsl (STR ''⏎applied on '') o showsl_formula φ)))"
by (pat_completeness,auto)
termination by (relation "measure (λx.
case x of Inl (Inl (x,_)) ⇒ size x
| Inl (Inr (xs,_)) ⇒ size_list size xs
| Inr (Inl (xs,_)) ⇒ size_list size xs
| Inr (Inr (xs,_)) ⇒ size_list size xs)", auto)
lemma isOK_check_formula_dist:
assumes "isOK (check_formula_dist hs pre post φs)" and "φ ∈ set φs"
shows "∃h ∈ set hs. isOK (check_formula h (Disjunction (pre @ φ # post)))"
proof (insert assms, induct φs arbitrary: hs)
case IH: (Cons a φs) then show ?case by(cases hs, auto)
qed auto
end
fun mono_formula where
"mono_formula b (Conjunction fs) = (∀ f ∈ set fs. mono_formula b f)"
| "mono_formula b (Disjunction fs) = (∀ f ∈ set fs. mono_formula b f)"
| "mono_formula b (Atom a) = b"
| "mono_formula b (NegAtom a) = (¬ b)"
lemma mono_formula_negate: "mono_formula (¬ b) f ⟹ mono_formula b (¬⇩f f)"
by (induct f, auto)
lemma mono_formula_and: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∧⇩f g)"
by (induct f g rule: form_and.induct, auto simp: form_and.simps)
lemma mono_formula_form_all: "(⋀ f. f ∈ set fs ⟹ mono_formula b f) ⟹ mono_formula b (form_all fs)"
by (induct fs, auto simp: mono_formula_and)
lemma mono_formula_or: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∨⇩f g)"
by (induct f g rule: form_or.induct, auto simp: form_or.simps)
lemma mono_formula_cnf_form_or: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∨⇩c⇩f g)"
by (induct f g rule: cnf_form_or.induct, auto intro: mono_formula_or)
lemma mono_formula_form_cnf_ex: "(⋀ f. f ∈ set fs ⟹ mono_formula b f) ⟹ mono_formula b (form_cnf_ex fs)"
by (induct fs, auto simp: mono_formula_cnf_form_or)
lemma mono_formula_flatten: "mono_formula b f ⟹ mono_formula b (flatten f)"
by (induct f, auto intro!: mono_formula_form_all mono_formula_form_cnf_ex)
locale logic_checker =
logic where type_fixer = "TYPE(_)" + pre_logic_checker +
assumes logic_checker:
"⋀h φ. isOK(logic_checker h φ) ⟹ formula φ ⟹ is_neg_atom_clause φ ⟹ ⊨⇩f φ"
and negate_atom_formula: "is_bool e ⟹ formula (negate_atom e)"
and negate_atom_mono: "mono_formula True (negate_atom e)"
and negate_atom_negates: "is_bool e ⟹ assignment α ⟹ α ⊨ negate_atom e ⟷ ¬ α ⊨ Atom e"
begin
lemma mono_formula_remove_Atom: "mono_formula False (remove_Atom f)"
by (induct f, auto intro!: mono_formula_negate negate_atom_mono)
lemma formula_remove_Atom: "formula f ⟹ formula (remove_Atom f)"
by (induct f, auto simp: negate_atom_formula)
lemma Language_remove_Atom: "formula f ⟹ ℒ (remove_Atom f) = ℒ f"
by (induct f, auto, auto simp: negate_atom_negates Language_def)
lemma check_valid_formula:
assumes ok: "isOK(check_valid_formula φ)" and φ: "formula φ"
shows "⊨⇩f φ"
proof-
from φ have form: "formula (flatten φ)" by auto
from is_cnf_flatten[of φ] have "is_cnf (flatten φ)" .
then obtain φs where *: "flatten φ = Conjunction φs" "⋀ φ⇩i. φ⇩i ∈ set φs ⟹ is_clause φ⇩i" by (cases, auto)
from form have form: "⋀ψ. ψ ∈ set φs ⟹ formula ψ" by (auto simp: *)
{
fix ψ
assume **: "ψ ∈ set φs"
note form = form[OF **]
note clause = *(2)[OF **]
let ?ψ = "remove_Atom ψ"
from is_cnf_flatten[of ?ψ] have "is_cnf (flatten ?ψ)" .
then obtain χs where 1: "flatten ?ψ = Conjunction χs" "⋀ φ⇩i. φ⇩i ∈ set χs ⟹ is_clause φ⇩i" by (cases, auto)
from formula_remove_Atom[OF form] have form': "⋀ψ. ψ ∈ set χs ⟹ formula ψ"
using 1 formula_flatten by force
from ok[unfolded check_valid_formula_def *, simplified, rule_format, OF **, unfolded 1, simplified]
consider (Triv) "trivial_clause_checker ψ" | (lc) "∀x∈set χs. isOK (logic_checker default x)" by auto
then have "⊨⇩f ψ"
proof (cases)
case lc
{
fix χ
assume chi: "χ ∈ set χs"
with lc have ok: "isOK(logic_checker default χ)" by auto
from 1(2)[OF chi] have "is_clause χ" .
moreover have "mono_formula False χ"
using mono_formula_flatten[OF mono_formula_remove_Atom[of ψ], unfolded 1] chi by auto
ultimately
have "is_neg_atom_clause χ"
proof (induct χ, simp add: is_neg_atom_clause.simps, intro allI impI, goal_cases)
case (1 fs f)
then show ?case by (cases f, force+)
qed
from logic_checker[OF ok form'[OF chi] this]
have "⊨⇩f χ" .
}
then have "⊨⇩f flatten ?ψ" unfolding 1 by (simp add: valid_def)
also have "… ⟺⇩f ψ" by (simp add: Language_remove_Atom form)
finally show ?thesis by simp
next
case Triv
from trivial_clause_checker[OF clause this] show ?thesis .
qed
}
then have "⊨⇩f form_all φs" by (auto simp: valid_Language)
also have "... ⟺⇩f flatten φ" by (auto simp add: *)
finally show ?thesis by simp
qed
lemma isOK_simp: "isOK x = (x = Inr ())" by auto
lemma check_formula:
assumes "isOK(check_formula h φ)" and "formula φ"
shows "⊨⇩f φ"
proof-
have "isOK (check_formula h φ) ⟹ formula φ ⟹ ⊨⇩f φ"
and "isOK (check_formula_dist hs pre post φs) ⟹
(∀φ ∈ set pre. formula φ) ⟹
(∀φ ∈ set post. formula φ) ⟹
(∀φ ∈ set φs. formula φ) ⟹ ∀ φ ∈ set φs. ⊨⇩f Disjunction (pre @ φ # post)"
and "isOK (check_formula_lex_weak hs φ φs) ⟹ formula φ ⟹ ∀φ ∈ set φs. formula φ ⟹ ⊨⇩f Disjunction (φ#φs)"
and "isOK (check_formula_lex hs φ φs) ⟹ formula φ ⟹ ∀φ ∈ set φs. formula φ ⟹ ⊨⇩f Disjunction (φ#φs)"
for h φ hs φs pre post
proof (induct h φ and hs pre post φs and hs φ φs and hs φ φs rule:check_formula_check_formula_dist_check_formula_lex_weak_check_formula_lex.induct)
case (1 φ) with check_valid_formula show ?case by auto
next
case (2 h φ)
then have "formula (remove_Atom (simplify φ))" by (intro formula_remove_Atom, auto)
with 2 have "⊨⇩f remove_Atom (simplify φ)" by (auto dest: logic_checker)
also have "… ⟺⇩f φ" using 2(2) by (simp add: Language_remove_Atom)
finally show ?case .
next
case (3 n h φ)
show ?case
proof (cases φ)
case φ: (Disjunction φs)
show ?thesis
proof (cases "n < length φs")
case True
moreover define pre where "pre = take n φs"
moreover define post where "post = drop (Suc n) φs"
moreover define ψ where "ψ = φs ! n"
ultimately have split: "φs = pre @ ψ # post"
by (simp add: id_take_nth_drop)
from 3(3) have form: "∀φ ∈ set pre. formula φ" "∀φ ∈ set post. formula φ"
by (auto simp: φ pre_def post_def dest: in_set_takeD in_set_dropD)
with 3(2)[unfolded φ, simplified, folded pre_def post_def]
have "⊨⇩f Disjunction (pre @ False⇩f # post)"
by (intro 3(1)[OF φ refl _] pre_def post_def, auto simp: check_def)
then show ?thesis
by (auto simp: φ split valid_Language)
next
case False with 3 φ show ?thesis by auto
qed
qed (insert 3, auto simp: check_def)
next
case *: (4 n hints φ)
show ?case
proof (cases φ)
case φ: (Disjunction φs)
with *(3) have form: "∀ψ ∈ set φs. formula ψ" by auto
show ?thesis
proof (cases "n < length φs")
case [simp]: True
moreover define pre where "pre = take n φs"
moreover define post where "post = drop (Suc n) φs"
moreover define ψ where "ψ = φs ! n"
ultimately have split: "φs = pre @ ψ # post"
by (simp add: id_take_nth_drop)
from True form have form: "formula ψ" "∀ φ ∈ set pre. formula φ" "∀ φ ∈ set post. formula φ"
unfolding ψ_def pre_def post_def by (auto dest:in_set_takeD in_set_dropD)
note [symmetric,simp] = pre_def post_def ψ_def
show ?thesis
proof (cases "ψ")
case [simp]: (Conjunction ψs)
note ψ_def[symmetric,unfolded split this,simp]
from form have form2: "∀ρ ∈ set ψs. formula ρ" by auto
from *(1)[OF φ refl _ pre_def post_def, unfolded check_def, simplified, OF refl] form *(2)
show ?thesis apply (simp add: φ satisfies_Language) apply (unfold split) apply (auto simp: valid_Language) done
qed (insert * φ, auto)
qed (insert * φ, auto)
qed (insert *, auto)
next
case *: (5 h ψ)
from *(2) obtain φ φs where ψ: "ψ = Disjunction (φ#φs)"
by (cases ψ; cases "disjuncts ψ", auto)
with * show ?case by auto
next
case *: (6 h ψ)
from *(2) obtain φ φs where ψ: "ψ = Disjunction (φ#φs)"
by (cases ψ; cases "disjuncts ψ", auto)
with * show ?case by auto
next
case (10 φ φs) then show ?case by (auto dest!: trivial_formula simp: valid_Language)
next
case *: (11 hint hints φ φs)
have ok: "isOK (check_formula_lex_weak (hint # hints) φ φs)" by fact
show ?case
proof (cases "is_or_and_shape φ")
case False
then have "hints = []" "isOK(check_formula hint (Disjunction (φ#φs)))" using ok by (cases hints, auto)+
from *(3)[OF False this] show ?thesis using * by auto
next
case True
from True obtain φ1 x where φ: "φ = Disjunction [φ1, x]"
by (cases φ; cases "disjuncts φ" rule: list_4_cases, auto)
from True φ obtain φ2 φ3 where φ: "φ = Disjunction [φ1,Conjunction [φ2,φ3]]"
by (cases x; cases "conjuncts x" rule: list_4_cases, auto)
note IH = *(1-2)[OF True φ refl refl refl refl refl refl refl]
from ok φ True IH *(5,6)
have "⊨⇩f Disjunction (φ2 # φs)" and "⊨⇩f Disjunction (φ3 # φs)" by auto
then show ?thesis unfolding φ by (auto simp: valid_Language)
qed
next
case *: (12 hints φ φs)
note prems = *(9-)
show ?case
proof (cases "is_conj_shape hints φ")
case True
then obtain h1 h2 where hints: "hints = [h1,h2]"
by (cases hints rule: list_4_cases, auto)
from True hints obtain φ1 φ2 where φ: "φ = Conjunction [φ1, φ2]"
by (cases φ; cases "conjuncts φ" rule: list_4_cases, auto)
note IH = *(1-2)[OF True hints refl refl φ refl refl refl]
from IH prems φ hints show ?thesis by (auto simp:isOK_simp valid_Language)
next
case False
with prems have disj: "is_disj_shape hints φ" by (auto split: if_splits)
then obtain h1 hints2 where hints: "hints = h1 # hints2"
by (cases hints, auto)
from disj obtain x y where φ: "φ = Disjunction [x, y]"
by (cases φ; cases "disjuncts φ" rule: list_4_cases, auto)
from disj φ obtain φ1 φ2 where φ: "φ = Disjunction [Conjunction [φ1,φ2], y]"
by (cases x; cases "conjuncts x" rule: list_4_cases, auto)
from disj φ obtain φ3 φ4 where φ: "φ = Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]]"
by (cases y; cases "conjuncts y" rule: list_4_cases, auto)
note IH = *(3-8)[OF False disj hints φ refl refl refl refl refl refl refl refl refl refl refl]
note prems = prems[unfolded φ hints]
show ?thesis
proof (cases hints2 rule:list_3_cases)
case Nil
from IH(1-2)[OF Nil] prems
show ?thesis by (auto simp: Nil)
next
case (1 h2)
from IH(3-4)[OF 1 refl] prems φ hints
show ?thesis by (auto simp: 1 isOK_simp valid_Language)
next
case (2 h2 h3 hints3)
from IH(5-6)[OF 2 refl] prems φ hints
show ?thesis by (auto simp: 2 isOK_simp valid_Language)
qed
qed
qed auto
from this(1) assms show ?thesis by auto
qed
end
type_synonym ('f,'v,'t) definability_checker = "'v ⇒ 't ⇒ ('f,'v,'t) exp formula ⇒ showsl check"
locale pre_definability_checker =
prelogic where type_fixer = "TYPE('f×'t×'d)"
for type_fixer :: "('f×'v×'t×'d) itself"
and definability_checker :: "('f,'v,'t) definability_checker"
locale definability_checker = pre_definability_checker +
assumes definability_checker:
"⋀x ty φ. isOK (definability_checker x ty φ) ⟹ assignment α ⟹ ∃a ∈ Values_of_type ty. α((x,ty):=a) ⊨ φ"
lemmas [code] =
prelogic.is_bool_def
pre_sorted_algebra.has_type.simps
formula.formula.simps
showsl_formula.showsl_formula.simps
pre_logic_checker.check_valid_formula_def
pre_logic_checker.check_formula.simps
pre_logic_checker.check_formula_dist.simps
pre_logic_checker.check_formula_lex_weak.simps
pre_logic_checker.check_formula_lex.simps
pre_logic_checker.remove_Atom.simps
pre_logic_checker.is_or_and_shape.simps
pre_logic_checker.is_disj_shape.simps
pre_logic_checker.is_conj_shape.simps
end