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

src/Pure/Pure.thy

author | wenzelm |

Thu Aug 02 12:36:54 2012 +0200 (2012-08-02) | |

changeset 48646 | 91281e9472d8 |

parent 48641 | 92b48b8abfe4 |

child 48891 | c0eafbd55de3 |

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

more official command specifications, including source position;

1 theory Pure

2 keywords

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

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

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

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

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

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

9 "overloaded" "pervasive" "shows" "structure" "unchecked" "uses"

10 "where" "|"

11 and "header" :: diag

12 and "chapter" :: thy_heading1

13 and "section" :: thy_heading2

14 and "subsection" :: thy_heading3

15 and "subsubsection" :: thy_heading4

16 and "text" "text_raw" :: thy_decl

17 and "sect" :: prf_heading2 % "proof"

18 and "subsect" :: prf_heading3 % "proof"

19 and "subsubsect" :: prf_heading4 % "proof"

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

21 and "classes" "classrel" "default_sort" "typedecl" "type_synonym"

22 "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"

23 "translations" "no_translations" "axioms" "defs" "definition"

24 "abbreviation" "type_notation" "no_type_notation" "notation"

25 "no_notation" "axiomatization" "theorems" "lemmas" "declare"

26 "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl

27 and "use" "ML" :: thy_decl % "ML"

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

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

30 and "setup" "local_setup" "attribute_setup" "method_setup"

31 "declaration" "syntax_declaration" "simproc_setup"

32 "parse_ast_translation" "parse_translation" "print_translation"

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

34 and "bundle" :: thy_decl

35 and "include" "including" :: prf_decl

36 and "print_bundles" :: diag

37 and "context" "locale" :: thy_decl

38 and "sublocale" "interpretation" :: thy_schematic_goal

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

40 and "class" :: thy_decl

41 and "subclass" :: thy_goal

42 and "instantiation" :: thy_decl

43 and "instance" :: thy_goal

44 and "overloading" :: thy_decl

45 and "code_datatype" :: thy_decl

46 and "theorem" "lemma" "corollary" :: thy_goal

47 and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal

48 and "notepad" :: thy_decl

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

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

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

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

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

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

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

56 and "case" :: prf_asm % "proof"

57 and "{" :: prf_open % "proof"

58 and "}" :: prf_close % "proof"

59 and "next" :: prf_block % "proof"

60 and "qed" :: qed_block % "proof"

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

62 and "oops" :: qed_global % "proof"

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

64 and "proof" :: prf_block % "proof"

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

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

67 and "back" :: prf_script % "proof"

68 and "Isabelle.command" :: control

69 and "pretty_setmargin" "help" "print_commands" "print_configs"

70 "print_context" "print_theory" "print_syntax" "print_abbrevs"

71 "print_theorems" "print_locales" "print_classes" "print_locale"

72 "print_interps" "print_dependencies" "print_attributes"

73 "print_simpset" "print_rules" "print_trans_rules" "print_methods"

74 "print_antiquotations" "thy_deps" "class_deps" "thm_deps"

75 "print_binds" "print_facts" "print_cases" "print_statement" "thm"

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

77 :: diag

78 and "cd" :: control

79 and "pwd" :: diag

80 and "use_thy" "remove_thy" "kill_thy" :: control

81 and "display_drafts" "print_drafts" "pr" :: diag

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

83 and "welcome" :: diag

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

85 and "end" :: thy_end % "theory"

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

87 and "find_theorems" "find_consts" :: diag

88 uses

89 "Isar/isar_syn.ML"

90 "Tools/find_theorems.ML"

91 "Tools/find_consts.ML"

92 begin

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

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

98 lemma meta_mp:

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

100 shows "PROP Q"

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

103 lemmas meta_impE = meta_mp [elim_format]

105 lemma meta_spec:

106 assumes "!!x. PROP P x"

107 shows "PROP P x"

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

110 lemmas meta_allE = meta_spec [elim_format]

112 lemma swap_params:

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

116 subsection {* Meta-level conjunction *}

118 lemma all_conjunction:

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

120 proof

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

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

123 proof -

124 fix x

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

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

127 qed

128 next

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

130 fix x

131 show "PROP A x &&& PROP B x"

132 proof -

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

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

135 qed

136 qed

138 lemma imp_conjunction:

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

140 proof

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

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

143 proof -

144 assume "PROP A"

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

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

147 qed

148 next

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

150 assume "PROP A"

151 show "PROP B &&& PROP C"

152 proof -

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

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

155 qed

156 qed

158 lemma conjunction_imp:

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

160 proof

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

162 assume ab: "PROP A" "PROP B"

163 show "PROP C"

164 proof (rule r)

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

166 qed

167 next

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

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

170 show "PROP C"

171 proof (rule r)

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

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

174 qed

175 qed

177 end