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

src/Pure/Pure.thy

author | wenzelm |

Sun Nov 11 20:31:46 2012 +0100 (2012-11-11) | |

changeset 50081 | 9b92ee8dec98 |

parent 49569 | 7b6aaf446496 |

child 50128 | 599c935aac82 |

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

tuned;

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

16 "where" "|"

17 and "header" :: diag

18 and "chapter" :: thy_heading1

19 and "section" :: thy_heading2

20 and "subsection" :: thy_heading3

21 and "subsubsection" :: thy_heading4

22 and "text" "text_raw" :: thy_decl

23 and "sect" :: prf_heading2 % "proof"

24 and "subsect" :: prf_heading3 % "proof"

25 and "subsubsect" :: prf_heading4 % "proof"

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

27 and "classes" "classrel" "default_sort" "typedecl" "type_synonym"

28 "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"

29 "translations" "no_translations" "axioms" "defs" "definition"

30 "abbreviation" "type_notation" "no_type_notation" "notation"

31 "no_notation" "axiomatization" "theorems" "lemmas" "declare"

32 "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl

33 and "use" "ML" :: thy_decl % "ML"

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

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

36 and "setup" "local_setup" "attribute_setup" "method_setup"

37 "declaration" "syntax_declaration" "simproc_setup"

38 "parse_ast_translation" "parse_translation" "print_translation"

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

40 and "bundle" :: thy_decl

41 and "include" "including" :: prf_decl

42 and "print_bundles" :: diag

43 and "context" "locale" :: thy_decl

44 and "sublocale" "interpretation" :: thy_schematic_goal

45 and "interpret" :: prf_goal % "proof" (* FIXME schematic? *)

46 and "class" :: thy_decl

47 and "subclass" :: thy_goal

48 and "instantiation" :: thy_decl

49 and "instance" :: thy_goal

50 and "overloading" :: thy_decl

51 and "code_datatype" :: thy_decl

52 and "theorem" "lemma" "corollary" :: thy_goal

53 and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal

54 and "notepad" :: thy_decl

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

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

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

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

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

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

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

62 and "case" :: prf_asm % "proof"

63 and "{" :: prf_open % "proof"

64 and "}" :: prf_close % "proof"

65 and "next" :: prf_block % "proof"

66 and "qed" :: qed_block % "proof"

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

68 and "oops" :: qed_global % "proof"

69 and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof"

70 and "proof" :: prf_block % "proof"

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

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

73 and "back" :: prf_script % "proof"

74 and "Isabelle.command" :: control

75 and "pretty_setmargin" "help" "print_commands" "print_configs"

76 "print_context" "print_theory" "print_syntax" "print_abbrevs"

77 "print_theorems" "print_locales" "print_classes" "print_locale"

78 "print_interps" "print_dependencies" "print_attributes"

79 "print_simpset" "print_rules" "print_trans_rules" "print_methods"

80 "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"

81 "print_binds" "print_facts" "print_cases" "print_statement" "thm"

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

83 :: diag

84 and "cd" :: control

85 and "pwd" :: diag

86 and "use_thy" "remove_thy" "kill_thy" :: control

87 and "display_drafts" "print_drafts" "pr" :: diag

88 and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control

89 and "welcome" :: diag

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

91 and "end" :: thy_end % "theory"

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

93 and "find_theorems" "find_consts" :: diag

94 begin

96 ML_file "Isar/isar_syn.ML"

97 ML_file "Tools/find_theorems.ML"

98 ML_file "Tools/find_consts.ML"

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

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

105 lemma meta_mp:

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

107 shows "PROP Q"

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

110 lemmas meta_impE = meta_mp [elim_format]

112 lemma meta_spec:

113 assumes "!!x. PROP P x"

114 shows "PROP P x"

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

117 lemmas meta_allE = meta_spec [elim_format]

119 lemma swap_params:

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

123 subsection {* Meta-level conjunction *}

125 lemma all_conjunction:

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

127 proof

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

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

130 proof -

131 fix x

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

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

134 qed

135 next

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

137 fix x

138 show "PROP A x &&& PROP B x"

139 proof -

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

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

142 qed

143 qed

145 lemma imp_conjunction:

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

147 proof

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

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

150 proof -

151 assume "PROP A"

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

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

154 qed

155 next

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

157 assume "PROP A"

158 show "PROP B &&& PROP C"

159 proof -

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

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

162 qed

163 qed

165 lemma conjunction_imp:

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

167 proof

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

169 assume ab: "PROP A" "PROP B"

170 show "PROP C"

171 proof (rule r)

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

173 qed

174 next

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

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

177 show "PROP C"

178 proof (rule r)

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

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

181 qed

182 qed

184 end