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

src/Pure/Pure.thy

author | wenzelm |

Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago) | |

changeset 50499 | f496b2b7bafb |

parent 50128 | 599c935aac82 |

child 50603 | 3e3c2af5e8a5 |

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

rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;

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" :: prf_goal % "proof"

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

57 and "show" :: prf_asm_goal % "proof"

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

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

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

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

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

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

64 and "case" :: prf_asm % "proof"

65 and "{" :: prf_open % "proof"

66 and "}" :: prf_close % "proof"

67 and "next" :: prf_block % "proof"

68 and "qed" :: qed_block % "proof"

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

70 and "oops" :: qed_global % "proof"

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

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

73 and "proof" :: prf_block % "proof"

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

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

76 and "back" :: prf_script % "proof"

77 and "Isabelle.command" :: control

78 and "pretty_setmargin" "help" "print_commands" "print_configs"

79 "print_context" "print_theory" "print_syntax" "print_abbrevs"

80 "print_theorems" "print_locales" "print_classes" "print_locale"

81 "print_interps" "print_dependencies" "print_attributes"

82 "print_simpset" "print_rules" "print_trans_rules" "print_methods"

83 "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"

84 "print_binds" "print_facts" "print_cases" "print_statement" "thm"

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

86 :: diag

87 and "cd" :: control

88 and "pwd" :: diag

89 and "use_thy" "remove_thy" "kill_thy" :: control

90 and "display_drafts" "print_drafts" "pr" :: diag

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

92 and "welcome" :: diag

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

94 and "end" :: thy_end % "theory"

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

96 and "find_theorems" "find_consts" :: diag

97 begin

99 ML_file "Isar/isar_syn.ML"

100 ML_file "Tools/find_theorems.ML"

101 ML_file "Tools/find_consts.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