# Theory FOL_Extra

```theory FOL_Extra
imports
Type_Instances_Impl
"FOL-Fitting.FOL_Fitting"
"HOL-Library.FSet"
begin

subsection ‹Iff›

definition Iff where
"Iff p q = And (Impl p q) (Impl q p)"

lemma eval_Iff:
"eval e f g (Iff p q) ⟷ (eval e f g p ⟷ eval e f g q)"
by (auto simp: Iff_def)

subsection ‹Replacement of subformulas›

datatype ('a, 'b) ctxt
= Hole
| And1 "('a, 'b) ctxt" "('a, 'b) form"
| And2 "('a, 'b) form" "('a, 'b) ctxt"
| Or1 "('a, 'b) ctxt" "('a, 'b) form"
| Or2 "('a, 'b) form" "('a, 'b) ctxt"
| Impl1 "('a, 'b) ctxt" "('a, 'b) form"
| Impl2 "('a, 'b) form" "('a, 'b) ctxt"
| Neg1 "('a, 'b) ctxt"
| Forall1 "('a, 'b) ctxt"
| Exists1 "('a, 'b) ctxt"

primrec apply_ctxt :: "('a, 'b) ctxt ⇒ ('a, 'b) form ⇒ ('a, 'b) form" where
"apply_ctxt Hole p = p"
| "apply_ctxt (And1 c v) p = And (apply_ctxt c p) v"
| "apply_ctxt (And2 u c) p = And u (apply_ctxt c p)"
| "apply_ctxt (Or1 c v) p = Or (apply_ctxt c p) v"
| "apply_ctxt (Or2 u c) p = Or u (apply_ctxt c p)"
| "apply_ctxt (Impl1 c v) p = Impl (apply_ctxt c p) v"
| "apply_ctxt (Impl2 u c) p = Impl u (apply_ctxt c p)"
| "apply_ctxt (Neg1 c) p = Neg (apply_ctxt c p)"
| "apply_ctxt (Forall1 c) p = Forall (apply_ctxt c p)"
| "apply_ctxt (Exists1 c) p = Exists (apply_ctxt c p)"

lemma replace_subformula:
assumes "⋀e. eval e f g (Iff p q)"
shows "eval e f g (Iff (apply_ctxt c p) (apply_ctxt c q))"
by (induct c arbitrary: e) (auto simp: assms[unfolded eval_Iff] Iff_def)

subsection ‹Propositional identities›

lemma prop_ids:
"eval e f g (Iff (And p q) (And q p))"
"eval e f g (Iff (Or p q) (Or q p))"
"eval e f g (Iff (Or p (Or q r)) (Or (Or p q) r))"
"eval e f g (Iff (And p (And q r)) (And (And p q) r))"
"eval e f g (Iff (Neg (Or p q)) (And (Neg p) (Neg q)))"
"eval e f g (Iff (Neg (And p q)) (Or (Neg p) (Neg q)))"
(* ... *)
by (auto simp: Iff_def)

subsection ‹de Bruijn index manipulation for formulas; cf. @{term liftt}›

primrec liftti :: "nat ⇒ 'a term ⇒ 'a term" where
"liftti i (Var j) = (if i > j then Var j else Var (Suc j))"
| "liftti i (App f ts) = App f (map (liftti i) ts)"

lemma liftts_def':
"liftts ts = map liftt ts"
by (induct ts) auto

text ‹@{term liftt} is a special case of @{term liftti}›
lemma lifttti_0:
"liftti 0 t = liftt t"
by (induct t) (auto simp: liftts_def')

primrec lifti :: "nat ⇒ ('a, 'b) form ⇒ ('a, 'b) form" where
"lifti i FF = FF"
| "lifti i TT = TT"
| "lifti i (Pred b ts) = Pred b (map (liftti i) ts)"
| "lifti i (And p q) = And (lifti i p) (lifti i q)"
| "lifti i (Or p q) = Or (lifti i p) (lifti i q)"
| "lifti i (Impl p q) = Impl (lifti i p) (lifti i q)"
| "lifti i (Neg p) = Neg (lifti i p)"
| "lifti i (Forall p) = Forall (lifti (Suc i) p)"
| "lifti i (Exists p) = Exists (lifti (Suc i) p)"

abbreviation lift where
"lift ≡ lifti 0"

text ‹interaction of @{term lifti} and @{term eval}›

lemma evalts_def':
"evalts e f ts = map (evalt e f) ts"
by (induct ts) auto

lemma evalt_liftti:
"evalt (e⟨i:z⟩) f (liftti i t) = evalt e f t"
by (induct t) (auto simp: evalts_def' cong: map_cong)

lemma eval_lifti [simp]:
"eval (e⟨i:z⟩) f g (lifti i p) = eval e f g p"
by (induct p arbitrary: e i) (auto simp: evalt_liftti evalts_def' comp_def)

subsection ‹Quantifier Identities›

lemma quant_ids:
"eval e f g (Iff (Neg (Exists p)) (Forall (Neg p)))"
"eval e f g (Iff (Neg (Forall p)) (Exists (Neg p)))"
"eval e f g (Iff (And p (Forall q)) (Forall (And (lift p) q)))"
"eval e f g (Iff (And p (Exists q)) (Exists (And (lift p) q)))"
"eval e f g (Iff (Or p (Forall q)) (Forall (Or (lift p) q)))"
"eval e f g (Iff (Or p (Exists q)) (Exists (Or (lift p) q)))"
(* ... *)
by (auto simp: Iff_def)

(* We'd need a bit of more machinery to deal with "∀x y. P(x,y) ⟷ ∀y x. P(x, y)":
* swapping of de Bruijn indices (perhaps arbitrary permutation?) *)

subsection ‹Function symbols and predicates, with arities.›

primrec predas_form :: "('a, 'b) form ⇒ ('b × nat) set" where
"predas_form FF = {}"
| "predas_form TT = {}"
| "predas_form (Pred b ts) = {(b, length ts)}"
| "predas_form (And p q) = predas_form p ∪ predas_form q"
| "predas_form (Or p q) = predas_form p ∪ predas_form q"
| "predas_form (Impl p q) = predas_form p ∪ predas_form q"
| "predas_form (Neg p) = predas_form p"
| "predas_form (Forall p) = predas_form p"
| "predas_form (Exists p) = predas_form p"

primrec funas_term :: "'a term ⇒ ('a × nat) set" where
"funas_term (Var x) = {}"
| "funas_term (App f ts) = {(f, length ts)} ∪ ⋃(set (map funas_term ts))"

primrec terms_form :: "('a, 'b) form ⇒ 'a term set" where
"terms_form FF = {}"
| "terms_form TT = {}"
| "terms_form (Pred b ts) = set ts"
| "terms_form (And p q) = terms_form p ∪ terms_form q"
| "terms_form (Or p q) = terms_form p ∪ terms_form q"
| "terms_form (Impl p q) = terms_form p ∪ terms_form q"
| "terms_form (Neg p) = terms_form p"
| "terms_form (Forall p) = terms_form p"
| "terms_form (Exists p) = terms_form p"

definition funas_form :: "('a, 'b) form ⇒ ('a × nat) set" where
"funas_form f ≡ ⋃(funas_term ` terms_form f)"

subsection ‹Negation Normal Form›

inductive is_nnf :: "('a, 'b) form ⇒ bool" where
"is_nnf TT"
| "is_nnf FF"
| "is_nnf (Pred p ts)"
| "is_nnf (Neg (Pred p ts))"
| "is_nnf p ⟹ is_nnf q ⟹ is_nnf (And p q)"
| "is_nnf p ⟹ is_nnf q ⟹ is_nnf (Or p q)"
| "is_nnf p ⟹ is_nnf (Forall p)"
| "is_nnf p ⟹ is_nnf (Exists p)"

primrec nnf' :: "bool ⇒ ('a, 'b) form ⇒ ('a, 'b) form" where
"nnf' b TT          = (if b then TT else FF)"
| "nnf' b FF          = (if b then FF else TT)"
| "nnf' b (Pred p ts) = (if b then id else Neg) (Pred p ts)"
| "nnf' b (And p q)   = (if b then And else Or) (nnf' b p) (nnf' b q)"
| "nnf' b (Or p q)    = (if b then Or else And) (nnf' b p) (nnf' b q)"
| "nnf' b (Impl p q)  = (if b then Or else And) (nnf' (¬ b) p) (nnf' b q)"
| "nnf' b (Neg p)     = nnf' (¬ b) p"
| "nnf' b (Forall p)  = (if b then Forall else Exists) (nnf' b p)"
| "nnf' b (Exists p)  = (if b then Exists else Forall) (nnf' b p)"

lemma eval_nnf':
"eval e f g (nnf' b p) ⟷ (eval e f g p ⟷ b)"
by (induct p arbitrary: e b) auto

lemma is_nnf_nnf':
"is_nnf (nnf' b p)"
by (induct p arbitrary: b) (auto intro: is_nnf.intros)

abbreviation nnf where
"nnf ≡ nnf' True"

lemmas nnf_simpls [simp] = eval_nnf'[where b = True, unfolded eq_True] is_nnf_nnf'[where b = True]

subsection ‹Reasoning modulo ACI01›

datatype ('a, 'b) form_aci
= TT_aci
| FF_aci
| Pred_aci bool 'b "'a term list"
| And_aci "('a, 'b) form_aci fset"
| Or_aci "('a, 'b) form_aci fset"
| Forall_aci "('a, 'b) form_aci"
| Exists_aci "('a, 'b) form_aci"

text ‹evaluation, see @{const eval}›

primrec eval_aci :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒
('b ⇒ 'c list ⇒ bool) ⇒ ('a, 'b) form_aci ⇒ bool› where
"eval_aci e f g FF_aci            ⟷ False"
| "eval_aci e f g TT_aci            ⟷ True"
| "eval_aci e f g (Pred_aci b a ts) ⟷ (g a (evalts e f ts) ⟷ b)"
| "eval_aci e f g (And_aci ps)      ⟷ fBall (fimage (eval_aci e f g) ps) id"
| "eval_aci e f g (Or_aci ps)       ⟷ fBex (fimage (eval_aci e f g) ps) id"
| "eval_aci e f g (Forall_aci p)    ⟷ (∀z. eval_aci (e⟨0:z⟩) f g p)"
| "eval_aci e f g (Exists_aci p)    ⟷ (∃z. eval_aci (e⟨0:z⟩) f g p)"

text ‹smart constructor: conjunction›

fun and_aci where
"and_aci FF_aci       _            = FF_aci"
| "and_aci _            FF_aci       = FF_aci"
| "and_aci TT_aci       q            = q"
| "and_aci p            TT_aci       = p"
| "and_aci (And_aci ps) (And_aci qs) = And_aci (ps |∪| qs)"
| "and_aci (And_aci ps) q            = And_aci (ps |∪| {|q|})"
| "and_aci p            (And_aci qs) = And_aci ({|p|} |∪| qs)"
| "and_aci p            q            = (if p = q then p else And_aci {|p,q|})"

lemma eval_and_aci [simp]:
"eval_aci e f g (and_aci p q) ⟷ eval_aci e f g p ∧ eval_aci e f g q"
by (cases "(p, q)" rule: and_aci.cases) (simp_all add: ball_Un, meson+)

declare and_aci.simps [simp del]

text ‹smart constructor: disjunction›

fun or_aci where
"or_aci TT_aci       _            = TT_aci"
| "or_aci _            TT_aci       = TT_aci"
| "or_aci FF_aci       q            = q"
| "or_aci p            FF_aci       = p"
| "or_aci (Or_aci ps)  (Or_aci qs)  = Or_aci (ps |∪| qs)"
| "or_aci (Or_aci ps)  q            = Or_aci (ps |∪| {|q|})"
| "or_aci p            (Or_aci qs)  = Or_aci ({|p|} |∪| qs)"
| "or_aci p            q            = (if p = q then p else Or_aci {|p,q|})"

lemma eval_or_aci [simp]:
"eval_aci e f g (or_aci p q) ⟷ eval_aci e f g p ∨ eval_aci e f g q"
by (cases "(p, q)" rule: or_aci.cases) (simp_all add: bex_Un, meson+)

declare or_aci.simps [simp del]

text ‹convert negation normal form to ACIU01 normal form›

fun nnf_to_aci :: "('a, 'b) form ⇒ ('a, 'b) form_aci" where
"nnf_to_aci FF                = FF_aci"
| "nnf_to_aci TT                = TT_aci"
| "nnf_to_aci (Pred b ts)       = Pred_aci True b ts"
| "nnf_to_aci (Neg (Pred b ts)) = Pred_aci False b ts"
| "nnf_to_aci (And p q)         = and_aci (nnf_to_aci p) (nnf_to_aci q)"
| "nnf_to_aci (Or p q)          = or_aci (nnf_to_aci p) (nnf_to_aci q)"
| "nnf_to_aci (Forall p)        = Forall_aci (nnf_to_aci p)"
| "nnf_to_aci (Exists p)        = Exists_aci (nnf_to_aci p)"
| "nnf_to_aci _                 = undefined" (* the remaining cases are impossible for NNFs *)

lemma eval_nnf_to_aci:
"is_nnf p ⟹ eval_aci e f g (nnf_to_aci p) ⟷ eval e f g p"
by (induct p arbitrary: e rule: is_nnf.induct) simp_all

subsection ‹A (mostly) Propositional Equivalence Check›

text ‹We reason modulo \$\forall = \neg\exists\neg\$, de Morgan, double negation, and
ACUI01 of \$\vee\$ and \$\wedge\$, by converting to negation normal form, and then collapsing
conjunctions and disjunctions taking units, absorption, commutativity, associativity, and
idempotence into account. We only need soundness for a certifier.›

lemma check_equivalence_by_nnf_aci:
"nnf_to_aci (nnf p) = nnf_to_aci (nnf q) ⟹ eval e f g p ⟷ eval e f g q"
by (metis eval_nnf_to_aci is_nnf_nnf' eval_nnf')

subsection ‹Reasoning modulo ACI01›

datatype ('a, 'b) form_list_aci
= TT_aci
| FF_aci
| Pred_aci bool 'b "'a term list"
| And_aci "('a, 'b) form_list_aci list"
| Or_aci "('a, 'b) form_list_aci list"
| Forall_aci "('a, 'b) form_list_aci"
| Exists_aci "('a, 'b) form_list_aci"

text ‹evaluation, see @{const eval}›

fun eval_list_aci :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒
('b ⇒ 'c list ⇒ bool) ⇒ ('a, 'b) form_list_aci ⇒ bool› where
"eval_list_aci e f g FF_aci            ⟷ False"
| "eval_list_aci e f g TT_aci            ⟷ True"
| "eval_list_aci e f g (Pred_aci b a ts) ⟷ (g a (evalts e f ts) ⟷ b)"
| "eval_list_aci e f g (And_aci ps)      ⟷ list_all (λ fm. eval_list_aci e f g fm) ps"
| "eval_list_aci e f g (Or_aci ps)       ⟷ list_ex (λ fm. eval_list_aci e f g fm) ps"
| "eval_list_aci e f g (Forall_aci p)    ⟷ (∀z. eval_list_aci (e⟨0:z⟩) f g p)"
| "eval_list_aci e f g (Exists_aci p)    ⟷ (∃z. eval_list_aci (e⟨0:z⟩) f g p)"

text ‹smart constructor: conjunction›

fun and_list_aci where
"and_list_aci FF_aci       _            = FF_aci"
| "and_list_aci _            FF_aci       = FF_aci"
| "and_list_aci TT_aci       q            = q"
| "and_list_aci p            TT_aci       = p"
| "and_list_aci (And_aci ps) (And_aci qs) = And_aci (remdups (ps @ qs))"
| "and_list_aci (And_aci ps) q            = And_aci (List.insert q ps)"
| "and_list_aci p            (And_aci qs) = And_aci (List.insert p qs)"
| "and_list_aci p            q            = (if p = q then p else And_aci [p,q])"

lemma eval_and_list_aci [simp]:
"eval_list_aci e f g (and_list_aci p q) ⟷ eval_list_aci e f g p ∧ eval_list_aci e f g q"
apply (cases "(p, q)" rule: and_list_aci.cases)
apply blast+
done

declare and_list_aci.simps [simp del]

text ‹smart constructor: disjunction›

fun or_list_aci where
"or_list_aci TT_aci       _            = TT_aci"
| "or_list_aci _            TT_aci       = TT_aci"
| "or_list_aci FF_aci       q            = q"
| "or_list_aci p            FF_aci       = p"
| "or_list_aci (Or_aci ps)  (Or_aci qs)  = Or_aci (remdups (ps @ qs))"
| "or_list_aci (Or_aci ps)  q            = Or_aci (List.insert q ps)"
| "or_list_aci p            (Or_aci qs)  = Or_aci (List.insert p qs)"
| "or_list_aci p            q            = (if p = q then p else Or_aci [p,q])"

lemma eval_or_list_aci [simp]:
"eval_list_aci e f g (or_list_aci p q) ⟷ eval_list_aci e f g p ∨ eval_list_aci e f g q"
by (cases "(p, q)" rule: or_list_aci.cases) (simp_all add: list.pred_set list_ex_iff, blast+)

declare or_list_aci.simps [simp del]

text ‹convert negation normal form to ACIU01 normal form›

fun nnf_to_list_aci :: "('a, 'b) form ⇒ ('a, 'b) form_list_aci" where
"nnf_to_list_aci FF                = FF_aci"
| "nnf_to_list_aci TT                = TT_aci"
| "nnf_to_list_aci (Pred b ts)       = Pred_aci True b ts"
| "nnf_to_list_aci (Neg (Pred b ts)) = Pred_aci False b ts"
| "nnf_to_list_aci (And p q)         = and_list_aci (nnf_to_list_aci p) (nnf_to_list_aci q)"
| "nnf_to_list_aci (Or p q)          = or_list_aci (nnf_to_list_aci p) (nnf_to_list_aci q)"
| "nnf_to_list_aci (Forall p)        = Forall_aci (nnf_to_list_aci p)"
| "nnf_to_list_aci (Exists p)        = Exists_aci (nnf_to_list_aci p)"
| "nnf_to_list_aci _                 = undefined" (* the remaining cases are impossible for NNFs *)

lemma eval_nnf_to_list_aci:
"is_nnf p ⟹ eval_list_aci e f g (nnf_to_list_aci p) ⟷ eval e f g p"
by (induct p arbitrary: e rule: is_nnf.induct) simp_all

subsection ‹A (mostly) Propositional Equivalence Check›

text ‹We reason modulo \$\forall = \neg\exists\neg\$, de Morgan, double negation, and
ACUI01 of \$\vee\$ and \$\wedge\$, by converting to negation normal form, and then collapsing
conjunctions and disjunctions taking units, absorption, commutativity, associativity, and
idempotence into account. We only need soundness for a certifier.›

derive linorder "term"
derive compare "term"
derive linorder form_list_aci
derive compare form_list_aci

fun ord_form_list_aci where
"ord_form_list_aci TT_aci = TT_aci"
| "ord_form_list_aci FF_aci = FF_aci"
| "ord_form_list_aci (Pred_aci bool b ts) = Pred_aci bool b ts"
| "ord_form_list_aci (And_aci fm) = (And_aci (sort (map ord_form_list_aci fm)))"
| "ord_form_list_aci (Or_aci fm) = (Or_aci (sort (map ord_form_list_aci fm)))"
| "ord_form_list_aci (Forall_aci fm) = (Forall_aci (ord_form_list_aci fm))"
| "ord_form_list_aci (Exists_aci fm) = Exists_aci (ord_form_list_aci fm)"

lemma and_list_aci_simps:
"and_list_aci TT_aci q = q"
"and_list_aci q FF_aci = FF_aci"
by (cases q, auto simp add: and_list_aci.simps)+

lemma ord_form_list_idemp:
"ord_form_list_aci (ord_form_list_aci q) = ord_form_list_aci q"
apply (induct q) apply (auto simp: list.set_map)
apply (smt imageE list.set_map map_idI set_sort sorted_sort_id sorted_sort_key)+
done

lemma eval_lsit_aci_ord_form_list_aci:
"eval_list_aci e f g (ord_form_list_aci p) ⟷ eval_list_aci e f g p"
by (induct p arbitrary: e) (auto simp: list.pred_set list_ex_iff)

lemma check_equivalence_by_nnf_sortedlist_aci:
"ord_form_list_aci (nnf_to_list_aci (nnf p)) = ord_form_list_aci (nnf_to_list_aci (nnf q)) ⟹ eval e f g p ⟷ eval e f g q"
by (metis eval_nnf_to_list_aci eval_lsit_aci_ord_form_list_aci is_nnf_nnf' eval_nnf')

hide_type (open) "term"
hide_const (open) Var
hide_type (open) ctxt

end```