in der Quellcodebibliothek suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/FOLP/ex/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle Foundation.thy Sprache: Isabelle

(*  Title:      FOLP/ex/Foundation.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

section "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"

theory Foundation
imports IFOLP
begin

schematic_goal "?p : A&B --> (C-->A&C)"
apply (rule impI)
apply (rule impI)
apply (rule conjI)
prefer 2 apply assumption
apply (rule conjunct1)
apply assumption
done

text \<open>A form of conj-elimination\<close>
schematic_goal
  assumes "p : A & B"
    and "!!x y. x : A ==> y : B ==> f(x, y) : C"
  shows "?p : C"
apply (rule assms)
apply (rule conjunct1)
apply (rule assms)
apply (rule conjunct2)
apply (rule assms)
done

schematic_goal
  assumes "!!A x. x : ~ ~A ==> cla(x) : A"
  shows "?p : B | ~B"
apply (rule assms)
apply (rule notI)
apply (rule_tac P = "~B" in notE)
apply (rule_tac [2] notI)
apply (rule_tac [2] P = "B | ~B" in notE)
prefer 2 apply assumption
apply (rule_tac [2] disjI1)
prefer 2 apply assumption
apply (rule notI)
apply (rule_tac P = "B | ~B" in notE)
apply assumption
apply (rule disjI2)
apply assumption
done

schematic_goal
  assumes "!!A x. x : ~ ~A ==> cla(x) : A"
  shows "?p : B | ~B"
apply (rule assms)
apply (rule notI)
apply (rule notE)
apply (rule_tac [2] notI)
apply (erule_tac [2] notE)
apply (erule_tac [2] disjI1)
apply (rule notI)
apply (erule notE)
apply (erule disjI2)
done

schematic_goal
  assumes "p : A | ~A"
    and "q : ~ ~A"
  shows "?p : A"
apply (rule disjE)
apply (rule assms)
apply assumption
apply (rule FalseE)
apply (rule_tac P = "~A" in notE)
apply (rule assms)
apply assumption
done

subsection "Examples with quantifiers"

schematic_goal
  assumes "p : ALL z. G(z)"
  shows "?p : ALL z. G(z)|H(z)"
apply (rule allI)
apply (rule disjI1)
apply (rule assms [THEN spec])
done

schematic_goal "?p : ALL x. EX y. x=y"
apply (rule allI)
apply (rule exI)
apply (rule refl)
done

schematic_goal "?p : EX y. ALL x. x=y"
apply (rule exI)
apply (rule allI)
apply (rule refl)?
oops

text \<open>Parallel lifting example.\<close>
schematic_goal "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
apply (rule exI allI)
apply (rule exI allI)
apply (rule exI allI)
apply (rule exI allI)
apply (rule exI allI)
oops

schematic_goal
  assumes "p : (EX z. F(z)) & B"
  shows "?p : EX z. F(z) & B"
apply (rule conjE)
apply (rule assms)
apply (rule exE)
apply assumption
apply (rule exI)
apply (rule conjI)
apply assumption
apply assumption
done

text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
schematic_goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
apply (rule impI)
apply (rule allI)
apply (rule exE, assumption)
apply (rule exI)
apply (rule allE, assumption)
apply assumption
done

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.