# Theory Examples_FOL

theory Examples_FOL
imports FOL Eisbach_Old_Appl_Syntax
```(*  Title:      HOL/Eisbach/Examples_FOL.thy
Author:     Daniel Matichuk, NICTA/UNSW
*)

section ‹Basic Eisbach examples (in FOL)›

theory Examples_FOL
imports FOL Eisbach_Old_Appl_Syntax
begin

subsection ‹Basic methods›

method my_intros = (rule conjI | rule impI)

lemma "P ∧ Q ⟶ Z ∧ X"
apply my_intros+
oops

method my_intros' uses intros = (rule conjI | rule impI | rule intros)

lemma "P ∧ Q ⟶ Z ∨ X"
apply (my_intros' intros: disjI1)+
oops

method my_spec for x :: 'a = (drule spec[where x="x"])

lemma "∀x. P(x) ⟹ P(x)"
apply (my_spec x)
apply assumption
done

subsection ‹Demo›

named_theorems intros and elims and subst

method prop_solver declares intros elims subst =
(assumption |
rule intros | erule elims |
subst subst | subst (asm) subst |
(erule notE; solves prop_solver))+

lemmas [intros] =
conjI
impI
disjCI
iffI
notI
lemmas [elims] =
impCE
conjE
disjE

lemma "((A ∨ B) ∧ (A ⟶ C) ∧ (B ⟶ C)) ⟶ C"
apply prop_solver
done

method guess_all =
(match premises in U[thin]:"∀x. P (x :: 'a)" for P ⇒
‹match premises in "?H (y :: 'a)" for y ⇒
‹rule allE[where P = P and x = y, OF U]›
| match conclusion in "?H (y :: 'a)" for y ⇒
‹rule allE[where P = P and x = y, OF U]››)

lemma "(∀x. P(x) ⟶ Q(x)) ⟹ P(y) ⟹ Q(y)"
apply guess_all
apply prop_solver
done

lemma "(∀x. P(x) ⟶ Q(x)) ⟹  P(z) ⟹ P(y) ⟹ Q(y)"
apply (solves ‹guess_all, prop_solver›)  ― ‹Try it without solve›
done

method guess_ex =
(match conclusion in
"∃x. P (x :: 'a)" for P ⇒
‹match premises in "?H (x :: 'a)" for x ⇒
‹rule exI[where x=x]››)

lemma "P(x) ⟹ ∃x. P(x)"
apply guess_ex
apply prop_solver
done

method fol_solver =
((guess_ex | guess_all | prop_solver); solves fol_solver)

declare
allI [intros]
exE [elims]
ex_simps [subst]
all_simps [subst]

lemma "(∀x. P(x)) ∧ (∀x. Q(x)) ⟹ (∀x. P(x) ∧ Q(x))"
and  "∃x. P(x) ⟶ (∀x. P(x))"
and "(∃x. ∀y. R(x, y)) ⟶ (∀y. ∃x. R(x, y))"
by fol_solver+

end
```