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

src/Pure/Pure.thy

author | wenzelm |

Fri May 17 20:53:28 2013 +0200 (2013-05-17) | |

changeset 52060 | 179236c82c2a |

parent 52009 | 3b18ef9df768 |

child 52143 | 36ffe23b25f8 |

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

renamed 'print_configs' to 'print_options';

1 (* Title: Pure/Pure.thy

2 Author: Makarius

4 Final stage of bootstrapping Pure, based on implicit background theory.

5 *)

7 theory Pure

8 keywords

9 "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="

10 "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"

11 "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"

12 "attach" "begin" "binder" "constrains" "defines" "fixes" "for"

13 "identifier" "if" "imports" "in" "includes" "infix" "infixl"

14 "infixr" "is" "keywords" "notes" "obtains" "open" "output"

15 "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"

16 and "header" :: diag

17 and "chapter" :: thy_heading1

18 and "section" :: thy_heading2

19 and "subsection" :: thy_heading3

20 and "subsubsection" :: thy_heading4

21 and "text" "text_raw" :: thy_decl

22 and "sect" :: prf_heading2 % "proof"

23 and "subsect" :: prf_heading3 % "proof"

24 and "subsubsect" :: prf_heading4 % "proof"

25 and "txt" "txt_raw" :: prf_decl % "proof"

26 and "classes" "classrel" "default_sort" "typedecl" "type_synonym"

27 "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"

28 "translations" "no_translations" "defs" "definition"

29 "abbreviation" "type_notation" "no_type_notation" "notation"

30 "no_notation" "axiomatization" "theorems" "lemmas" "declare"

31 "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl

32 and "ML" :: thy_decl % "ML"

33 and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)

34 and "ML_val" "ML_command" :: diag % "ML"

35 and "setup" "local_setup" "attribute_setup" "method_setup"

36 "declaration" "syntax_declaration" "simproc_setup"

37 "parse_ast_translation" "parse_translation" "print_translation"

38 "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"

39 and "bundle" :: thy_decl

40 and "include" "including" :: prf_decl

41 and "print_bundles" :: diag

42 and "context" "locale" :: thy_decl

43 and "sublocale" "interpretation" :: thy_goal

44 and "interpret" :: prf_goal % "proof"

45 and "class" :: thy_decl

46 and "subclass" :: thy_goal

47 and "instantiation" :: thy_decl

48 and "instance" :: thy_goal

49 and "overloading" :: thy_decl

50 and "code_datatype" :: thy_decl

51 and "theorem" "lemma" "corollary" :: thy_goal

52 and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal

53 and "notepad" :: thy_decl

54 and "have" :: prf_goal % "proof"

55 and "hence" :: prf_goal % "proof" == "then have"

56 and "show" :: prf_asm_goal % "proof"

57 and "thus" :: prf_asm_goal % "proof" == "then show"

58 and "then" "from" "with" :: prf_chain % "proof"

59 and "note" "using" "unfolding" :: prf_decl % "proof"

60 and "fix" "assume" "presume" "def" :: prf_asm % "proof"

61 and "obtain" "guess" :: prf_asm_goal % "proof"

62 and "let" "write" :: prf_decl % "proof"

63 and "case" :: prf_asm % "proof"

64 and "{" :: prf_open % "proof"

65 and "}" :: prf_close % "proof"

66 and "next" :: prf_block % "proof"

67 and "qed" :: qed_block % "proof"

68 and "by" ".." "." "done" "sorry" :: "qed" % "proof"

69 and "oops" :: qed_global % "proof"

70 and "defer" "prefer" "apply" :: prf_script % "proof"

71 and "apply_end" :: prf_script % "proof" == ""

72 and "proof" :: prf_block % "proof"

73 and "also" "moreover" :: prf_decl % "proof"

74 and "finally" "ultimately" :: prf_chain % "proof"

75 and "back" :: prf_script % "proof"

76 and "Isabelle.command" :: control

77 and "help" "print_commands" "print_options"

78 "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"

79 "print_theorems" "print_locales" "print_classes" "print_locale"

80 "print_interps" "print_dependencies" "print_attributes"

81 "print_simpset" "print_rules" "print_trans_rules" "print_methods"

82 "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"

83 "print_binds" "print_facts" "print_cases" "print_statement" "thm"

84 "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"

85 :: diag

86 and "cd" :: control

87 and "pwd" :: diag

88 and "use_thy" "remove_thy" "kill_thy" :: control

89 and "display_drafts" "print_drafts" "pr" :: diag

90 and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control

91 and "welcome" :: diag

92 and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control

93 and "end" :: thy_end % "theory"

94 and "realizers" "realizability" "extract_type" "extract" :: thy_decl

95 and "find_theorems" "find_consts" :: diag

96 begin

98 ML_file "Isar/isar_syn.ML"

99 ML_file "Tools/find_theorems.ML"

100 ML_file "Tools/find_consts.ML"

101 ML_file "Tools/proof_general_pure.ML"

104 section {* Further content for the Pure theory *}

106 subsection {* Meta-level connectives in assumptions *}

108 lemma meta_mp:

109 assumes "PROP P ==> PROP Q" and "PROP P"

110 shows "PROP Q"

111 by (rule `PROP P ==> PROP Q` [OF `PROP P`])

113 lemmas meta_impE = meta_mp [elim_format]

115 lemma meta_spec:

116 assumes "!!x. PROP P x"

117 shows "PROP P x"

118 by (rule `!!x. PROP P x`)

120 lemmas meta_allE = meta_spec [elim_format]

122 lemma swap_params:

123 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..

126 subsection {* Meta-level conjunction *}

128 lemma all_conjunction:

129 "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"

130 proof

131 assume conj: "!!x. PROP A x &&& PROP B x"

132 show "(!!x. PROP A x) &&& (!!x. PROP B x)"

133 proof -

134 fix x

135 from conj show "PROP A x" by (rule conjunctionD1)

136 from conj show "PROP B x" by (rule conjunctionD2)

137 qed

138 next

139 assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"

140 fix x

141 show "PROP A x &&& PROP B x"

142 proof -

143 show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])

144 show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])

145 qed

146 qed

148 lemma imp_conjunction:

149 "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"

150 proof

151 assume conj: "PROP A ==> PROP B &&& PROP C"

152 show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"

153 proof -

154 assume "PROP A"

155 from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)

156 from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)

157 qed

158 next

159 assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"

160 assume "PROP A"

161 show "PROP B &&& PROP C"

162 proof -

163 from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])

164 from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])

165 qed

166 qed

168 lemma conjunction_imp:

169 "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"

170 proof

171 assume r: "PROP A &&& PROP B ==> PROP C"

172 assume ab: "PROP A" "PROP B"

173 show "PROP C"

174 proof (rule r)

175 from ab show "PROP A &&& PROP B" .

176 qed

177 next

178 assume r: "PROP A ==> PROP B ==> PROP C"

179 assume conj: "PROP A &&& PROP B"

180 show "PROP C"

181 proof (rule r)

182 from conj show "PROP A" by (rule conjunctionD1)

183 from conj show "PROP B" by (rule conjunctionD2)

184 qed

185 qed

187 end