summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Import/HOL4Setup.thy

author | wenzelm |

Thu May 27 18:10:37 2010 +0200 (2010-05-27) | |

changeset 37146 | f652333bbf8e |

parent 34208 | a7acd6c68d9b |

child 41550 | efa734d9b221 |

permissions | -rw-r--r-- |

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

1 (* Title: HOL/Import/HOL4Setup.thy

2 Author: Sebastian Skalberg (TU Muenchen)

3 *)

5 theory HOL4Setup imports MakeEqual ImportRecorder

6 uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import.ML") begin

8 section {* General Setup *}

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

11 by auto

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

14 proof -

15 assume "!! bogus. P bogus"

16 thus "ALL x. P x"

17 ..

18 qed

20 consts

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

23 defs

24 ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"

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

27 by (simp add: ONE_ONE_DEF inj_on_def)

29 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"

30 proof (rule exI,safe)

31 show "inj Suc_Rep"

32 by (rule injI) (rule Suc_Rep_inject)

33 next

34 assume "surj Suc_Rep"

35 hence "ALL y. EX x. y = Suc_Rep x"

36 by (simp add: surj_def)

37 hence "EX x. Zero_Rep = Suc_Rep x"

38 by (rule spec)

39 thus False

40 proof (rule exE)

41 fix x

42 assume "Zero_Rep = Suc_Rep x"

43 hence "Suc_Rep x = Zero_Rep"

44 ..

45 with Suc_Rep_not_Zero_Rep

46 show False

47 ..

48 qed

49 qed

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

52 proof (rule iffI)

53 assume "Ex P"

54 thus "P (Eps P)"

55 ..

56 next

57 assume "P (Eps P)"

58 thus "Ex P"

59 ..

60 qed

62 consts

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

65 defs

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

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

69 by simp

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

72 proof -

73 assume "P t"

74 hence "EX x. P x"

75 ..

76 thus ?thesis

77 by (rule ex_imp_nonempty)

78 qed

80 lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"

81 by blast

83 lemma typedef_hol2hol4:

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

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

86 proof -

87 from a

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

89 by (simp add: type_definition_def)

90 have ed: "TYPE_DEFINITION P Rep"

91 proof (auto simp add: TYPE_DEFINITION)

92 fix x y

93 assume "Rep x = Rep y"

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

95 by auto

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

97 by (simp add: prems)

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

99 by auto

100 finally show "x = y" .

101 next

102 fix x

103 assume "P x"

104 with td

105 have "Rep (Abs x) = x"

106 by auto

107 hence "x = Rep (Abs x)"

108 ..

109 thus "EX y. x = Rep y"

110 ..

111 next

112 fix y

113 from td

114 show "P (Rep y)"

115 by auto

116 qed

117 show ?thesis

118 apply (rule exI [of _ Rep])

119 apply (rule ed)

120 .

121 qed

123 lemma typedef_hol2hollight:

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

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

126 proof

127 from a

128 show "Abs (Rep a) = a"

129 by (rule type_definition.Rep_inverse)

130 next

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

132 proof

133 assume "P r"

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

135 by simp

136 with a

137 show "Rep (Abs r) = r"

138 by (rule type_definition.Abs_inverse)

139 next

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

141 from a

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

143 by (rule type_definition.Rep)

144 thus "P r"

145 by (simp add: ra)

146 qed

147 qed

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

150 apply simp

151 apply (rule someI_ex)

152 .

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

155 by simp

157 use "hol4rews.ML"

159 setup hol4_setup

160 parse_ast_translation smarter_trueprop_parsing

162 use "proof_kernel.ML"

163 use "replay.ML"

164 use "import.ML"

166 setup Import.setup

168 end