SSL Examples_FOL.thy Sprache: Isabelle

(*  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

quality99%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders