header {* Beispielbeweise für VSPred *}
theory VSPredEx
imports VSPred
begin

section{* Ohne Existenzquantor *}

consts
  f :: "[i, i] => o"

text{* Erstes Beispiel, Rückwärtsbewies mit expliziter Instantiierung. *}
lemma bsp1: "(ALL x. ALL y. f x y) --> (ALL b. ALL a. f a b)"
 apply (rule impI)
 apply (rule allI) --{* [where x="b"]) *}
 apply (rule allI [where x="a"])
 apply (rule allE [where t="b"])
 apply (rule allE [where t="a"])
 apply (assumption)
 done

text{* Erstes Beispiel, Rückwärtsbeweis ohne explizite Instantiierung. *}
lemma bsp1a: "(ALL x. ALL y. p x y) --> (ALL y. ALL x. p x y)"
 apply (rule impI)
 apply (rule allI)
 apply (rule allI)
 apply (drule allE)
 apply (drule allE)
 apply (assumption)
 done


consts
  r :: "i => o"
  s :: "i => o"

text{* Zweites Beispiel. *}
lemma bsp2: "(ALL x. r x & s x) --> (ALL x. r x) & (ALL x. s x)"
 apply (rule impI)
 apply (rule conjI)
 apply (rule allI)
 apply (drule allE)
 apply (drule conjE1)
 apply (assumption)
 apply (rule allI) 
 apply (drule allE)
 apply (drule conjE2)
 apply (assumption) 
 done


section {* Mit Existenzquantor *}

consts
  u :: "i => o"
  v :: o

lemma ex3: "(ALL x. u x --> v) --> ((EX x. u x) --> v)"
  apply (rule impI)
  apply (rule impI)
  apply (rule exE [where P="%x. u x"])
  apply (assumption)
  apply (rule impE [where P="u x"])
  apply (rule allE [where P="%x. u x --> v"])
  apply (assumption)
  apply (assumption)
  done
end