# Theory Foundation

theory Foundation
imports IFOL
```(*  Title:      FOL/ex/Foundation.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

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

theory Foundation
imports IFOL
begin

lemma "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 ‹A form of conj-elimination›
lemma
assumes "A ∧ B"
and "A ⟹ B ⟹ C"
shows C
apply (rule assms)
apply (rule conjunct1)
apply (rule assms)
apply (rule conjunct2)
apply (rule assms)
done

lemma
assumes "⋀A. ¬ ¬ A ⟹ A"
shows "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

lemma
assumes "⋀A. ¬ ¬ A ⟹ A"
shows "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

lemma
assumes "A ∨ ¬ A"
and "¬ ¬ A"
shows 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"

lemma
assumes "∀z. G(z)"
shows "∀z. G(z) ∨ H(z)"
apply (rule allI)
apply (rule disjI1)
apply (rule assms [THEN spec])
done

lemma "∀x. ∃y. x = y"
apply (rule allI)
apply (rule exI)
apply (rule refl)
done

lemma "∃y. ∀x. x = y"
apply (rule exI)
apply (rule allI)
apply (rule refl)?
oops

text ‹Parallel lifting example.›
lemma "∃u. ∀x. ∃v. ∀y. ∃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

lemma
assumes "(∃z. F(z)) ∧ B"
shows "∃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 ‹A bigger demonstration of quantifiers -- not in the paper.›
lemma "(∃y. ∀x. Q(x,y)) ⟶ (∀x. ∃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
```