(* Title: HOL/Eisbach/Examples_FOL.thy
Author: Daniel Matichuk, NICTA/UNSW
*)
section \<open>Basic Eisbach examples (in FOL)\<close>
theory Examples_FOL
imports FOL Eisbach_Old_Appl_Syntax
begin
subsection \<open>Basic methods\<close>
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 \<open>Demo\<close>
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 \
\<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>
| match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
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 \<open>guess_all, prop_solver\<close>) \<comment> \<open>Try it without solve\<close>
done
method guess_ex =
(match conclusion in
"\x. P (x :: 'a)" for P \
\<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
\<open>rule exI[where x=x]\<close>\<close>)
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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 ist noch experimentell.
|
