author  wenzelm 
Mon, 05 May 2014 15:17:07 +0200  
changeset 56864  0446c7ac2e32 
parent 56797  32963b43a538 
child 57415  e721124f1b1e 
permissions  rwrr 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

1 
(* Title: Pure/Pure.thy 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

2 
Author: Makarius 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

3 

05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

4 
Final stage of bootstrapping Pure, based on implicit background theory. 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

5 
*) 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48891
diff
changeset

6 

48638  7 
theory Pure 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

8 
keywords 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

9 
"!!" "!" "%" "(" ")" "+" "," "" ":" "::" ";" "<" "<=" "=" "==" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

10 
"=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" 
52143  11 
"\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

12 
"attach" "begin" "binder" "constrains" "defines" "fixes" "for" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

13 
"identifier" "if" "imports" "in" "includes" "infix" "infixl" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

14 
"infixr" "is" "keywords" "notes" "obtains" "open" "output" 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51274
diff
changeset

15 
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "" 
52449
79e7fd57acc4
recover command tags from 4cf3f6153eb8  important for document preparation;
wenzelm
parents:
52439
diff
changeset

16 
and "theory" :: thy_begin % "theory" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

17 
and "header" :: diag 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

18 
and "chapter" :: thy_heading1 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

19 
and "section" :: thy_heading2 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

20 
and "subsection" :: thy_heading3 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

21 
and "subsubsection" :: thy_heading4 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

22 
and "text" "text_raw" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

23 
and "sect" :: prf_heading2 % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

24 
and "subsect" :: prf_heading3 % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

25 
and "subsubsect" :: prf_heading4 % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

26 
and "txt" "txt_raw" :: prf_decl % "proof" 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

27 
and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment" 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

28 
"consts" "syntax" "no_syntax" "translations" "no_translations" "defs" 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55152
diff
changeset

29 
"definition" "abbreviation" "type_notation" "no_type_notation" "notation" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

30 
"no_notation" "axiomatization" "theorems" "lemmas" "declare" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

31 
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset

32 
and "SML_file" "ML_file" :: thy_load % "ML" 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset

33 
and "SML_import" "SML_export" :: thy_decl % "ML" 
51295  34 
and "ML" :: thy_decl % "ML" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

35 
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

36 
and "ML_val" "ML_command" :: diag % "ML" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

37 
and "simproc_setup" :: thy_decl % "ML" == "" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

38 
and "setup" "local_setup" "attribute_setup" "method_setup" 
55762
27a45aec67a0
suppress completion of obscure keyword, avoid confusion with plain "simp";
wenzelm
parents:
55516
diff
changeset

39 
"declaration" "syntax_declaration" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

40 
"parse_ast_translation" "parse_translation" "print_translation" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

41 
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

42 
and "bundle" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

43 
and "include" "including" :: prf_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

44 
and "print_bundles" :: diag 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

45 
and "context" "locale" :: thy_decl 
51224
c3e99efacb67
back to nonschematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset

46 
and "sublocale" "interpretation" :: thy_goal 
c3e99efacb67
back to nonschematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents:
50603
diff
changeset

47 
and "interpret" :: prf_goal % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

48 
and "class" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

49 
and "subclass" :: thy_goal 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

50 
and "instantiation" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

51 
and "instance" :: thy_goal 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

52 
and "overloading" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

53 
and "code_datatype" :: thy_decl 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

54 
and "theorem" "lemma" "corollary" :: thy_goal 
51274
cfc83ad52571
discontinued pointless command category "thy_schematic_goal"  this is checked dynamically;
wenzelm
parents:
51270
diff
changeset

55 
and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

56 
and "notepad" :: thy_decl 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

57 
and "have" :: prf_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

58 
and "hence" :: prf_goal % "proof" == "then have" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

59 
and "show" :: prf_asm_goal % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

60 
and "thus" :: prf_asm_goal % "proof" == "then show" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

61 
and "then" "from" "with" :: prf_chain % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

62 
and "note" "using" "unfolding" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

63 
and "fix" "assume" "presume" "def" :: prf_asm % "proof" 
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset

64 
and "obtain" :: prf_asm_goal % "proof" 
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52549
diff
changeset

65 
and "guess" :: prf_asm_goal_script % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

66 
and "let" "write" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

67 
and "case" :: prf_asm % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

68 
and "{" :: prf_open % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

69 
and "}" :: prf_close % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

70 
and "next" :: prf_block % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

71 
and "qed" :: qed_block % "proof" 
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset

72 
and "by" ".." "." "sorry" :: "qed" % "proof" 
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset

73 
and "done" :: "qed_script" % "proof" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

74 
and "oops" :: qed_global % "proof" 
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

75 
and "defer" "prefer" "apply" :: prf_script % "proof" 
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49569
diff
changeset

76 
and "apply_end" :: prf_script % "proof" == "" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

77 
and "proof" :: prf_block % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

78 
and "also" "moreover" :: prf_decl % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

79 
and "finally" "ultimately" :: prf_chain % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

80 
and "back" :: prf_script % "proof" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

81 
and "Isabelle.command" :: control 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

82 
and "help" "print_commands" "print_options" "print_context" 
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

83 
"print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

84 
"print_theorems" "print_locales" "print_classes" "print_locale" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

85 
"print_interps" "print_dependencies" "print_attributes" 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

86 
"print_simpset" "print_rules" "print_trans_rules" "print_methods" 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

87 
"print_antiquotations" "print_ML_antiquotations" "thy_deps" 
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

88 
"locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts" 
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

89 
"print_cases" "print_statement" "thm" "prf" "full_prf" "prop" 
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55762
diff
changeset

90 
"term" "typ" "print_codesetup" "unused_thms" 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

91 
:: diag 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

92 
and "cd" :: control 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

93 
and "pwd" :: diag 
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

94 
and "use_thy" "remove_thy" "kill_thy" :: control 
52549  95 
and "display_drafts" "print_state" "pr" :: diag 
52438
7b5a5116f3af
back to keyword 'pr' :: diag as required for ProofGeneral command line  reject this TTY command in Isabelle/jEdit by other means;
wenzelm
parents:
52437
diff
changeset

96 
and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control 
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

97 
and "welcome" :: diag 
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

98 
and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control 
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset

99 
and "end" :: thy_end % "theory" 
56797  100 
and "realizers" :: thy_decl == "" 
101 
and "realizability" :: thy_decl == "" 

102 
and "extract_type" "extract" :: thy_decl 

48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset

103 
and "find_theorems" "find_consts" :: diag 
52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

104 
and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

105 
"ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52430
diff
changeset

106 
"ProofGeneral.inform_file_retracted" :: control 
48638  107 
begin 
15803  108 

56205  109 
ML_file "ML/ml_antiquotations.ML" 
55516  110 
ML_file "ML/ml_thms.ML" 
56864  111 
ML_file "Tools/print_operation.ML" 
48891  112 
ML_file "Isar/isar_syn.ML" 
55141  113 
ML_file "Isar/calculation.ML" 
55030  114 
ML_file "Tools/rail.ML" 
53707  115 
ML_file "Tools/rule_insts.ML"; 
48891  116 
ML_file "Tools/find_theorems.ML" 
117 
ML_file "Tools/find_consts.ML" 

52009  118 
ML_file "Tools/proof_general_pure.ML" 
54730  119 
ML_file "Tools/simplifier_trace.ML" 
48891  120 

121 

55140
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

122 
section {* Basic attributes *} 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

123 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

124 
attribute_setup tagged = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

125 
"Scan.lift (Args.name  Args.name) >> Thm.tag" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

126 
"tagged theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

127 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

128 
attribute_setup untagged = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

129 
"Scan.lift Args.name >> Thm.untag" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

130 
"untagged theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

131 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

132 
attribute_setup kind = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

133 
"Scan.lift Args.name >> Thm.kind" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

134 
"theorem kind" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

135 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

136 
attribute_setup THEN = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

137 
"Scan.lift (Scan.optional (Args.bracks Parse.nat) 1)  Attrib.thm 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

138 
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

139 
"resolution with rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

140 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

141 
attribute_setup OF = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

142 
"Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

143 
"rule resolved with facts" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

144 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

145 
attribute_setup rename_abs = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

146 
"Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

147 
Thm.rule_attribute (K (Drule.rename_bvars' vs)))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

148 
"rename bound variables in abstractions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

149 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

150 
attribute_setup unfolded = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

151 
"Attrib.thms >> (fn ths => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

152 
Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

153 
"unfolded definitions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

154 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

155 
attribute_setup folded = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

156 
"Attrib.thms >> (fn ths => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

157 
Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

158 
"folded definitions" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

159 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

160 
attribute_setup consumes = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

161 
"Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

162 
"number of consumed facts" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

163 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

164 
attribute_setup constraints = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

165 
"Scan.lift Parse.nat >> Rule_Cases.constraints" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

166 
"number of equality constraints" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

167 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

168 
attribute_setup case_names = {* 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

169 
Scan.lift (Scan.repeat1 (Args.name  
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

170 
Scan.optional (@{keyword "["}  Scan.repeat1 (Args.maybe Args.name)  @{keyword "]"}) [])) 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

171 
>> (fn cs => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

172 
Rule_Cases.cases_hyp_names 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

173 
(map #1 cs) 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

174 
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs)) 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

175 
*} "named rule cases" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

176 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

177 
attribute_setup case_conclusion = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

178 
"Scan.lift (Args.name  Scan.repeat Args.name) >> Rule_Cases.case_conclusion" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

179 
"named conclusion of rule cases" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

180 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

181 
attribute_setup params = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

182 
"Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

183 
"named rule parameters" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

184 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

185 
attribute_setup rule_format = {* 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

186 
Scan.lift (Args.mode "no_asm") 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

187 
>> (fn true => Object_Logic.rule_format_no_asm  false => Object_Logic.rule_format) 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

188 
*} "result put into canonical rule format" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

189 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

190 
attribute_setup elim_format = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

191 
"Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

192 
"destruct rule turned into elimination rule format" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

193 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

194 
attribute_setup no_vars = {* 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

195 
Scan.succeed (Thm.rule_attribute (fn context => fn th => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

196 
let 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

197 
val ctxt = Variable.set_body false (Context.proof_of context); 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

198 
val ((_, [th']), _) = Variable.import true [th] ctxt; 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

199 
in th' end)) 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

200 
*} "imported schematic variables" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

201 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

202 
attribute_setup eta_long = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

203 
"Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

204 
"put theorem into eta long beta normal form" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

205 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

206 
attribute_setup atomize = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

207 
"Scan.succeed Object_Logic.declare_atomize" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

208 
"declaration of atomize rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

209 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

210 
attribute_setup rulify = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

211 
"Scan.succeed Object_Logic.declare_rulify" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

212 
"declaration of rulify rule" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

213 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

214 
attribute_setup rotated = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

215 
"Scan.lift (Scan.optional Parse.int 1 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

216 
>> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

217 
"rotated theorem premises" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

218 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

219 
attribute_setup defn = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

220 
"Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

221 
"declaration of definitional transformations" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

222 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

223 
attribute_setup abs_def = 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

224 
"Scan.succeed (Thm.rule_attribute (fn context => 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

225 
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

226 
"abstract over free variables of definitional theorem" 
7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

227 

7eb0c04e4c40
define basic attributes in userspace Pure.thy  which provides better hyperlinks and may serve as example;
wenzelm
parents:
55030
diff
changeset

228 

26435  229 
section {* Further content for the Pure theory *} 
20627  230 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

231 
subsection {* Metalevel connectives in assumptions *} 
15803  232 

233 
lemma meta_mp: 

18019  234 
assumes "PROP P ==> PROP Q" and "PROP P" 
15803  235 
shows "PROP Q" 
18019  236 
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) 
15803  237 

23432  238 
lemmas meta_impE = meta_mp [elim_format] 
239 

15803  240 
lemma meta_spec: 
26958  241 
assumes "!!x. PROP P x" 
242 
shows "PROP P x" 

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

15803  244 

245 
lemmas meta_allE = meta_spec [elim_format] 

246 

26570  247 
lemma swap_params: 
26958  248 
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. 
26570  249 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

250 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

251 
subsection {* Metalevel conjunction *} 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

252 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

253 
lemma all_conjunction: 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

254 
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

255 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

256 
assume conj: "!!x. PROP A x &&& PROP B x" 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

257 
show "(!!x. PROP A x) &&& (!!x. PROP B x)" 
19121  258 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

259 
fix x 
26958  260 
from conj show "PROP A x" by (rule conjunctionD1) 
261 
from conj show "PROP B x" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

262 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

263 
next 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

264 
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

265 
fix x 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

266 
show "PROP A x &&& PROP B x" 
19121  267 
proof  
26958  268 
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) 
269 
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

270 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

271 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

272 

19121  273 
lemma imp_conjunction: 
50603  274 
"(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))" 
18836  275 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

276 
assume conj: "PROP A ==> PROP B &&& PROP C" 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

277 
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" 
19121  278 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

279 
assume "PROP A" 
19121  280 
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) 
281 
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

282 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

283 
next 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

284 
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

285 
assume "PROP A" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

286 
show "PROP B &&& PROP C" 
19121  287 
proof  
288 
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) 

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

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

290 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

291 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

292 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

293 
lemma conjunction_imp: 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

294 
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

295 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

296 
assume r: "PROP A &&& PROP B ==> PROP C" 
22933  297 
assume ab: "PROP A" "PROP B" 
298 
show "PROP C" 

299 
proof (rule r) 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

300 
from ab show "PROP A &&& PROP B" . 
22933  301 
qed 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

302 
next 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

303 
assume r: "PROP A ==> PROP B ==> PROP C" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

304 
assume conj: "PROP A &&& PROP B" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

305 
show "PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

306 
proof (rule r) 
19121  307 
from conj show "PROP A" by (rule conjunctionD1) 
308 
from conj show "PROP B" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

309 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

310 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

311 

48638  312 
end 
313 