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

src/Pure/Pure.thy

author | wenzelm |

Fri Apr 12 14:54:14 2013 +0200 (2013-04-12) | |

changeset 51700 | c8f2bad67dbb |

parent 51585 | fcd5af4aac2b |

child 52007 | 0b1183012a3c |

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

tuned signature;

tuned comments;

tuned comments;

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_configs"

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"

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

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

107 lemma meta_mp:

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

109 shows "PROP Q"

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

112 lemmas meta_impE = meta_mp [elim_format]

114 lemma meta_spec:

115 assumes "!!x. PROP P x"

116 shows "PROP P x"

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

119 lemmas meta_allE = meta_spec [elim_format]

121 lemma swap_params:

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

125 subsection {* Meta-level conjunction *}

127 lemma all_conjunction:

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

129 proof

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

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

132 proof -

133 fix x

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

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

136 qed

137 next

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

139 fix x

140 show "PROP A x &&& PROP B x"

141 proof -

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

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

144 qed

145 qed

147 lemma imp_conjunction:

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

149 proof

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

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

152 proof -

153 assume "PROP A"

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

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

156 qed

157 next

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

159 assume "PROP A"

160 show "PROP B &&& PROP C"

161 proof -

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

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

164 qed

165 qed

167 lemma conjunction_imp:

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

169 proof

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

171 assume ab: "PROP A" "PROP B"

172 show "PROP C"

173 proof (rule r)

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

175 qed

176 next

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

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

179 show "PROP C"

180 proof (rule r)

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

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

183 qed

184 qed

186 end