Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ATP.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/ATP.thy
    Author:     Fabian Immler, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Martin Desharnais, UniBw Muenchen
*)

section \<open>Automatic Theorem Provers (ATPs)\<close>

theory ATP
  imports Meson
begin

subsection \<open>ATP problems and proofs\<close>

ML_file \<open>Tools/ATP/atp_util.ML\<close>
ML_file \<open>Tools/ATP/atp_problem.ML\<close>
ML_file \<open>Tools/ATP/atp_proof.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>

subsection \<open>Higher-order reasoning helpers\<close>

definition fFalse :: bool where
"fFalse \ False"

definition fTrue :: bool where
"fTrue \ True"

definition fNot :: "bool \ bool" where
"fNot P \ \ P"

definition fComp :: "('a \ bool) \ 'a \ bool" where
"fComp P = (\x. \ P x)"

definition fconj :: "bool \ bool \ bool" where
"fconj P Q \ P \ Q"

definition fdisj :: "bool \ bool \ bool" where
"fdisj P Q \ P \ Q"

definition fimplies :: "bool \ bool \ bool" where
"fimplies P Q \ (P \ Q)"

definition fAll :: "('a \ bool) \ bool" where
"fAll P \ All P"

definition fEx :: "('a \ bool) \ bool" where
"fEx P \ Ex P"

definition fequal :: "'a \ 'a \ bool" where
"fequal x y \ (x = y)"

lemma fTrue_ne_fFalse: "fFalse \ fTrue"
unfolding fFalse_def fTrue_def by simp

lemma fNot_table:
"fNot fFalse = fTrue"
"fNot fTrue = fFalse"
unfolding fFalse_def fTrue_def fNot_def by auto

lemma fconj_table:
"fconj fFalse P = fFalse"
"fconj P fFalse = fFalse"
"fconj fTrue fTrue = fTrue"
unfolding fFalse_def fTrue_def fconj_def by auto

lemma fdisj_table:
"fdisj fTrue P = fTrue"
"fdisj P fTrue = fTrue"
"fdisj fFalse fFalse = fFalse"
unfolding fFalse_def fTrue_def fdisj_def by auto

lemma fimplies_table:
"fimplies P fTrue = fTrue"
"fimplies fFalse P = fTrue"
"fimplies fTrue fFalse = fFalse"
unfolding fFalse_def fTrue_def fimplies_def by auto

lemma fAll_table:
"Ex (fComp P) \ fAll P = fTrue"
"All P \ fAll P = fFalse"
unfolding fFalse_def fTrue_def fComp_def fAll_def by auto

lemma fEx_table:
"All (fComp P) \ fEx P = fTrue"
"Ex P \ fEx P = fFalse"
unfolding fFalse_def fTrue_def fComp_def fEx_def by auto

lemma fequal_table:
"fequal x x = fTrue"
"x = y \ fequal x y = fFalse"
unfolding fFalse_def fTrue_def fequal_def by auto

lemma fNot_law:
"fNot P \ P"
unfolding fNot_def by auto

lemma fComp_law:
"fComp P x \ \ P x"
unfolding fComp_def ..

lemma fconj_laws:
"fconj P P \ P"
"fconj P Q \ fconj Q P"
"fNot (fconj P Q) \ fdisj (fNot P) (fNot Q)"
unfolding fNot_def fconj_def fdisj_def by auto

lemma fdisj_laws:
"fdisj P P \ P"
"fdisj P Q \ fdisj Q P"
"fNot (fdisj P Q) \ fconj (fNot P) (fNot Q)"
unfolding fNot_def fconj_def fdisj_def by auto

lemma fimplies_laws:
"fimplies P Q \ fdisj (\ P) Q"
"fNot (fimplies P Q) \ fconj P (fNot Q)"
unfolding fNot_def fconj_def fdisj_def fimplies_def by auto

lemma fAll_law:
"fNot (fAll R) \ fEx (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto

lemma fEx_law:
"fNot (fEx R) \ fAll (fComp R)"
unfolding fNot_def fComp_def fAll_def fEx_def by auto

lemma fequal_laws:
"fequal x y = fequal y x"
"fequal x y = fFalse \ fequal y z = fFalse \ fequal x z = fTrue"
"fequal x y = fFalse \ fequal (f x) (f y) = fTrue"
unfolding fFalse_def fTrue_def fequal_def by auto

subsection \<open>Basic connection between ATPs and HOL\<close>

ML_file \<open>Tools/lambda_lifting.ML\<close>
ML_file \<open>Tools/monomorph.ML\<close>
ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>

end

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.