(*<*) theory FOL imports Main begin (*>*) section {* Quantifier Rules in Action *} text{* Here is one version of the first example proof from the lecture on predicate logic *} lemma "(\x. P x) \ (\y. P y)" apply (rule impI) apply (frule_tac x=a in spec) apply (rule_tac x=a in exI) by assumption text {* This proof is rather unusual in that in the second step, it is sufficient to instantiate the universally quantified hypothesis with a new variable `a' which is unconstrained by any formulas in the sequent. More commonly we instantiate formulas with terms built with free variables already present in the sequent. See the next couple of proofs. *} text{* Here is the 2nd example proof from Lecture 5, with some renaming of bound variables to make the formulas and proofs a little clearer. This shows use of left and right forall introduction rules. *} lemma "(\u. P u \ Q u) \ (\v. P v) \ (\w. Q w)" apply (rule impI) apply (erule conjE) apply (rule allI) apply (erule_tac x="w" in allE) apply (erule_tac x="w" in allE) apply (erule impE) by assumption+ text {* An example showing use of left and right exists introduction rules *} lemma " (\z. P z) \ Q \ (\y. P y \ Q)" apply (rule impI) apply (erule conjE) apply (erule exE) apply (rule_tac x="z" in exI) apply (rule conjI) apply assumption+ done text {* Here's a variation on the classical exists right introduction rule exCI in the Isabelle library. The advantage of this one is that it doesn't introduce meta-variables into the sequent. *} lemma exCIF: "((\x. \(P x)) \ False) \ \x. P x" by auto text {* An example of the use of exCIF *} lemma "\( \ P a \ \ P b) \ (\z. P z)" apply (rule impI) apply (rule exCIF) apply (erule notE) apply (rule conjI) apply (erule_tac x="a" in allE) apply assumption apply (erule_tac x="b" in allE) apply assumption done section {* Cheaters are losers *} lemma Cheaters: "\(\x. cheats x) \ (\x. loses x); (\x. cheats x \ loses x) \ loses me\ \ loses me" apply (erule mp) (* View mp rule as special left intro rule for implies*) apply (rule allI) apply (rule impI) (* From here on, is little choice in next rules *) apply (erule impE) apply (rule_tac x="x" in exI) apply assumption apply (erule_tac x="x" in allE) apply assumption done section {* Use of meta-variables in Isabelle goals *} text{* Meta-variables (also called schematic-variables in the Isabelle documentation) in goals can be considered to be existentially quantified at the sequent level. As a proof proceeds, the proof is free to substitute in more specialised terms for the meta-variables. Often, the unification that happens when rules are applied will find the needed meta-variable instantiations. This saves having to enter instantiating terms explicitly. However using meta-variables in goals and instantiating them with unification can be rather confusing when first starting out. All the Isabelle exercises and coursework can be accomplished without exploiting them. Below are some examples of proofs involving meta-variables. *} text {* Example 1 again *} lemma "(\x. P x) \ (\y. P y)" apply (rule impI) apply (rule exI) apply (drule spec) apply assumption done text {* Example II again. Here the meta-variables introduced are actually functions taking as argument a variable universally meta-quantified at the sequent level. This indicates that any instantiating term for the meta-variables can make use of the universally quantified variable. *} lemma "(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)" apply (rule impI) apply (erule conjE) apply (rule allI) apply (erule allE) apply (erule allE) apply (erule mp) by assumption text {* The example again of how existential quantification distributes over conjunction. Once you have stepped through the proof, try doing it again with the order of the exE and exI rules swapped. Why does the proof fail? *} lemma " (\z. P z) \ Q \ (\y. P y \ Q)" apply (rule impI) apply (erule conjE) apply (erule exE) apply (rule exI) apply (rule conjI) apply assumption+ done end