author  wenzelm 
Fri, 23 Apr 1999 11:50:17 +0200  
changeset 6493  3489490c948d 
parent 6444  2ebe9e630cab 
child 6746  cf6ad8d22793 
permissions  rwrr 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Isar_examples/Peirce.thy 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

4 

6493  5 
Peirce's law: examples of classical proof. 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

6 
*) 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

7 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

8 
theory Peirce = Main:; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

9 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

10 

6493  11 
theorem "((A > B) > A) > A"; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

12 
proof; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

13 
assume ABA: "(A > B) > A"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

14 
show A; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

15 
proof (rule classical); 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

16 
assume notA: "~ A"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

17 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

18 
have AB: "A > B"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

19 
proof; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

20 
assume A: A; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

21 
from notA A; show B; ..; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

22 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

23 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

24 
from ABA AB; show A; ..; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

25 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

26 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

27 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

28 

6493  29 
theorem "((A > B) > A) > A"; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

30 
proof; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

31 
assume ABA: "(A > B) > A"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

32 
show A; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

33 
proof (rule classical); 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

34 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

35 
assume AB: "A > B"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

36 
from ABA AB; show A; ..; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

37 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

38 
next; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

39 
assume notA: "~ A"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

40 
show "A > B"; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

41 
proof; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

42 
assume A: A; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

43 
from notA A; show B; ..; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

44 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

45 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

46 
qed; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

47 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

48 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

49 
end; 