author  wenzelm 
Wed, 15 Feb 2006 21:34:59 +0100  
changeset 19048  2b875dd5eb4c 
parent 18836  3a1e4ee72075 
child 19121  d7fd5415a781 
permissions  rwrr 
15803  1 
(* Title: Pure/Pure.thy 
2 
ID: $Id$ 

18710  3 

4 
The actual Pure theory. 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

5 
*) 
15803  6 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

7 
header {* The Pure theory *} 
15803  8 

9 
theory Pure 

10 
imports ProtoPure 

11 
begin 

12 

19048  13 
setup  {* Common setup of internal components *} 
15803  14 

18710  15 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

16 
subsection {* Metalevel connectives in assumptions *} 
15803  17 

18 
lemma meta_mp: 

18019  19 
assumes "PROP P ==> PROP Q" and "PROP P" 
15803  20 
shows "PROP Q" 
18019  21 
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) 
15803  22 

23 
lemma meta_spec: 

18019  24 
assumes "!!x. PROP P(x)" 
15803  25 
shows "PROP P(x)" 
18019  26 
by (rule `!!x. PROP P(x)`) 
15803  27 

28 
lemmas meta_allE = meta_spec [elim_format] 

29 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

30 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

31 
subsection {* Metalevel conjunction *} 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

32 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

33 
locale (open) meta_conjunction_syntax = 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

34 
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

35 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

36 
parse_translation {* 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

37 
[("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))] 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

38 
*} 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

39 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

40 
lemma all_conjunction: 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

41 
includes meta_conjunction_syntax 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

42 
shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

43 
proof 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

44 
assume conj: "!!x. PROP A(x) && PROP B(x)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

45 
fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

46 
show "PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

47 
proof (rule r) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

48 
fix x 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

49 
from conj show "PROP A(x)" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

50 
from conj show "PROP B(x)" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

51 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

52 
next 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

53 
assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

54 
fix x 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

55 
fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

56 
show "PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

57 
proof (rule r) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

58 
show "PROP A(x)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

59 
proof (rule conj) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

60 
assume "!!x. PROP A(x)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

61 
then show "PROP A(x)" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

62 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

63 
show "PROP B(x)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

64 
proof (rule conj) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

65 
assume "!!x. PROP B(x)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

66 
then show "PROP B(x)" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

67 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

68 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

69 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

70 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

71 
lemma imp_conjunction [unfolded prop_def]: 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

72 
includes meta_conjunction_syntax 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

73 
shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" 
18836  74 
unfolding prop_def 
75 
proof 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

76 
assume conj: "PROP A ==> PROP B && PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

77 
fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

78 
show "PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

79 
proof (rule r) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

80 
assume "PROP A" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

81 
from conj [OF `PROP A`] show "PROP B" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

82 
from conj [OF `PROP A`] show "PROP C" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

83 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

84 
next 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

85 
assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

86 
assume "PROP A" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

87 
fix X assume r: "PROP B ==> PROP C ==> PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

88 
show "PROP X" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

89 
proof (rule r) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

90 
show "PROP B" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

91 
proof (rule conj) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

92 
assume "PROP A ==> PROP B" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

93 
from this [OF `PROP A`] show "PROP B" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

94 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

95 
show "PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

96 
proof (rule conj) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

97 
assume "PROP A ==> PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

98 
from this [OF `PROP A`] show "PROP C" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

99 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

100 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

101 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

102 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

103 
lemma conjunction_imp: 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

104 
includes meta_conjunction_syntax 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

105 
shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

106 
proof 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

107 
assume r: "PROP A && PROP B ==> PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

108 
assume "PROP A" and "PROP B" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

109 
show "PROP C" by (rule r)  
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

110 
next 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

111 
assume r: "PROP A ==> PROP B ==> PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

112 
assume conj: "PROP A && PROP B" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

113 
show "PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

114 
proof (rule r) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

115 
from conj show "PROP A" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

116 
from conj show "PROP B" . 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

117 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

118 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

119 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

120 
lemma conjunction_assoc: 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

121 
includes meta_conjunction_syntax 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

122 
shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))" 
18836  123 
unfolding conjunction_imp . 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

124 

15803  125 
end 