author  wenzelm 
Sat, 08 Oct 2005 22:39:39 +0200  
changeset 17801  30cbd2685e73 
parent 17322  781abf7011e6 
child 19064  bf19cc5a7899 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

1 
(* Title: HOL/Import/HOL4Setup.thy 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

2 
ID: $Id$ 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

3 
Author: Sebastian Skalberg (TU Muenchen) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

4 
*) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

5 

16417  6 
theory HOL4Setup imports MakeEqual 
17801  7 
uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML" 
8 
("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin 

14516  9 

10 
section {* General Setup *} 

11 

12 
lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q" 

13 
by auto 

14 

15 
lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)" 

16 
proof  

17 
assume "!! bogus. P bogus" 

18 
thus "ALL x. P x" 

19 
.. 

20 
qed 

21 

22 
consts 

23 
ONE_ONE :: "('a => 'b) => bool" 

24 
ONTO :: "('a => 'b) => bool" 

25 

26 
defs 

27 
ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y > x = y" 

28 

29 
lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" 

30 
by (simp add: ONE_ONE_DEF inj_on_def) 

31 

17322  32 
lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))" 
14516  33 
proof (rule exI,safe) 
34 
show "inj Suc_Rep" 

35 
by (rule inj_Suc_Rep) 

36 
next 

17322  37 
assume "surj Suc_Rep" 
14516  38 
hence "ALL y. EX x. y = Suc_Rep x" 
17322  39 
by (simp add: surj_def) 
14516  40 
hence "EX x. Zero_Rep = Suc_Rep x" 
41 
by (rule spec) 

42 
thus False 

43 
proof (rule exE) 

44 
fix x 

45 
assume "Zero_Rep = Suc_Rep x" 

46 
hence "Suc_Rep x = Zero_Rep" 

47 
.. 

48 
with Suc_Rep_not_Zero_Rep 

49 
show False 

50 
.. 

51 
qed 

52 
qed 

53 

54 
lemma EXISTS_DEF: "Ex P = P (Eps P)" 

55 
proof (rule iffI) 

56 
assume "Ex P" 

57 
thus "P (Eps P)" 

58 
.. 

59 
next 

60 
assume "P (Eps P)" 

61 
thus "Ex P" 

62 
.. 

63 
qed 

64 

65 
consts 

66 
TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool" 

67 

68 
defs 

69 
TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) > (x = y)) & (ALL x. (p x = (EX y. x = rep y))))" 

70 

71 
lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)" 

72 
by simp 

73 

74 
lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)" 

75 
proof  

76 
assume "P t" 

77 
hence "EX x. P x" 

78 
.. 

79 
thus ?thesis 

80 
by (rule ex_imp_nonempty) 

81 
qed 

82 

83 
lemma light_imp_as: "[ Q > P; P > Q ] ==> P = Q" 

84 
by blast 

85 

86 
lemma typedef_hol2hol4: 

87 
assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" 

88 
shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)" 

89 
proof  

90 
from a 

91 
have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)" 

92 
by (simp add: type_definition_def) 

93 
have ed: "TYPE_DEFINITION P Rep" 

94 
proof (auto simp add: TYPE_DEFINITION) 

95 
fix x y 

96 
assume "Rep x = Rep y" 

97 
from td have "x = Abs (Rep x)" 

98 
by auto 

99 
also have "Abs (Rep x) = Abs (Rep y)" 

100 
by (simp add: prems) 

101 
also from td have "Abs (Rep y) = y" 

102 
by auto 

103 
finally show "x = y" . 

104 
next 

105 
fix x 

106 
assume "P x" 

107 
with td 

108 
have "Rep (Abs x) = x" 

109 
by auto 

110 
hence "x = Rep (Abs x)" 

111 
.. 

112 
thus "EX y. x = Rep y" 

113 
.. 

114 
next 

115 
fix y 

116 
from td 

117 
show "P (Rep y)" 

118 
by auto 

119 
qed 

120 
show ?thesis 

121 
apply (rule exI [of _ Rep]) 

122 
apply (rule ed) 

123 
. 

124 
qed 

125 

126 
lemma typedef_hol2hollight: 

127 
assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" 

128 
shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))" 

129 
proof 

130 
from a 

131 
show "Abs (Rep a) = a" 

132 
by (rule type_definition.Rep_inverse) 

133 
next 

134 
show "P r = (Rep (Abs r) = r)" 

135 
proof 

136 
assume "P r" 

137 
hence "r \<in> (Collect P)" 

138 
by simp 

139 
with a 

140 
show "Rep (Abs r) = r" 

141 
by (rule type_definition.Abs_inverse) 

142 
next 

143 
assume ra: "Rep (Abs r) = r" 

144 
from a 

145 
have "Rep (Abs r) \<in> (Collect P)" 

146 
by (rule type_definition.Rep) 

147 
thus "P r" 

148 
by (simp add: ra) 

149 
qed 

150 
qed 

151 

152 
lemma termspec_help: "[ Ex P ; c == Eps P ] ==> P c" 

153 
apply simp 

154 
apply (rule someI_ex) 

155 
. 

156 

157 
lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)" 

158 
by simp 

159 

160 
use "hol4rews.ML" 

161 

162 
setup hol4_setup 

163 
parse_ast_translation smarter_trueprop_parsing 

164 

165 
use "proof_kernel.ML" 

166 
use "replay.ML" 

167 
use "import_package.ML" 

168 

169 
setup ImportPackage.setup 

170 

171 
end 