src/Pure/Pure.thy
author wenzelm
Tue, 29 Apr 2014 22:52:15 +0200
changeset 56797 32963b43a538
parent 56618 874bdedb2313
child 56864 0446c7ac2e32
permissions -rw-r--r--
suppress slightly odd completions of "real";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 29606
diff changeset
     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
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52060
diff changeset
    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
71fc3776c453 discontinued redundant 'use' command;
wenzelm
parents: 51293
diff changeset
    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 non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
wenzelm
parents: 50603
diff changeset
    46
  and "sublocale" "interpretation" :: thy_goal
c3e99efacb67 back to non-schematic '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
802576856527 discontinued command 'print_drafts';
wenzelm
parents: 52449
diff changeset
    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
32963b43a538 suppress slightly odd completions of "real";
wenzelm
parents: 56618
diff changeset
   100
  and "realizers" :: thy_decl == ""
32963b43a538 suppress slightly odd completions of "real";
wenzelm
parents: 56618
diff changeset
   101
  and "realizability" :: thy_decl == ""
32963b43a538 suppress slightly odd completions of "real";
wenzelm
parents: 56618
diff changeset
   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
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 29606
diff changeset
   107
begin
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   108
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56069
diff changeset
   109
ML_file "ML/ml_antiquotations.ML"
55516
d0157612ebe5 prefer user-space tool within Pure.thy;
wenzelm
parents: 55385
diff changeset
   110
ML_file "ML/ml_thms.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48646
diff changeset
   111
ML_file "Isar/isar_syn.ML"
55141
863b4f9f6bd7 prefer self-contained user-space tool;
wenzelm
parents: 55140
diff changeset
   112
ML_file "Isar/calculation.ML"
55030
9a9049d12e21 prefer user-space tool within Pure.thy;
wenzelm
parents: 54730
diff changeset
   113
ML_file "Tools/rail.ML"
53707
d1c6bff9ff58 moved module into plain Isabelle/ML user space;
wenzelm
parents: 53571
diff changeset
   114
ML_file "Tools/rule_insts.ML";
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48646
diff changeset
   115
ML_file "Tools/find_theorems.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48646
diff changeset
   116
ML_file "Tools/find_consts.ML"
52009
3b18ef9df768 moved files;
wenzelm
parents: 52007
diff changeset
   117
ML_file "Tools/proof_general_pure.ML"
54730
de2d99b459b3 skeleton for Simplifier trace by Lars Hupel;
wenzelm
parents: 53707
diff changeset
   118
ML_file "Tools/simplifier_trace.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48646
diff changeset
   119
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48646
diff changeset
   120
55140
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   121
section {* Basic attributes *}
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   122
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   123
attribute_setup tagged =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   124
  "Scan.lift (Args.name -- Args.name) >> Thm.tag"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   125
  "tagged theorem"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   126
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   127
attribute_setup untagged =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   128
  "Scan.lift Args.name >> Thm.untag"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   129
  "untagged theorem"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   130
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   131
attribute_setup kind =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   132
  "Scan.lift Args.name >> Thm.kind"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   133
  "theorem kind"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   134
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   135
attribute_setup THEN =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   136
  "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   137
    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   138
  "resolution with rule"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   139
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   140
attribute_setup OF =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   141
  "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   142
  "rule resolved with facts"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   143
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   144
attribute_setup rename_abs =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   145
  "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   146
    Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   147
  "rename bound variables in abstractions"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   148
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   149
attribute_setup unfolded =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   150
  "Attrib.thms >> (fn ths =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   151
    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   152
  "unfolded definitions"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   153
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   154
attribute_setup folded =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   155
  "Attrib.thms >> (fn ths =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   156
    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   157
  "folded definitions"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   158
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   159
attribute_setup consumes =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   160
  "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   161
  "number of consumed facts"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   162
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   163
attribute_setup constraints =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   164
  "Scan.lift Parse.nat >> Rule_Cases.constraints"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   165
  "number of equality constraints"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   166
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   167
attribute_setup case_names = {*
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   168
  Scan.lift (Scan.repeat1 (Args.name --
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   169
    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   170
  >> (fn cs =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   171
      Rule_Cases.cases_hyp_names
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   172
        (map #1 cs)
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   173
        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   174
*} "named rule cases"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   175
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   176
attribute_setup case_conclusion =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   177
  "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   178
  "named conclusion of rule cases"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   179
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   180
attribute_setup params =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   181
  "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   182
  "named rule parameters"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   183
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   184
attribute_setup rule_format = {*
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   185
  Scan.lift (Args.mode "no_asm")
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   186
    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   187
*} "result put into canonical rule format"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   188
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   189
attribute_setup elim_format =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   190
  "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   191
  "destruct rule turned into elimination rule format"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   192
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   193
attribute_setup no_vars = {*
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   194
  Scan.succeed (Thm.rule_attribute (fn context => fn th =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   195
    let
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   196
      val ctxt = Variable.set_body false (Context.proof_of context);
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   197
      val ((_, [th']), _) = Variable.import true [th] ctxt;
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   198
    in th' end))
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   199
*} "imported schematic variables"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   200
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   201
attribute_setup eta_long =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   202
  "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   203
  "put theorem into eta long beta normal form"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   204
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   205
attribute_setup atomize =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   206
  "Scan.succeed Object_Logic.declare_atomize"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   207
  "declaration of atomize rule"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   208
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   209
attribute_setup rulify =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   210
  "Scan.succeed Object_Logic.declare_rulify"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   211
  "declaration of rulify rule"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   212
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   213
attribute_setup rotated =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   214
  "Scan.lift (Scan.optional Parse.int 1
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   215
    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   216
  "rotated theorem premises"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   217
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   218
attribute_setup defn =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   219
  "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   220
  "declaration of definitional transformations"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   221
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   222
attribute_setup abs_def =
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   223
  "Scan.succeed (Thm.rule_attribute (fn context =>
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   224
    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   225
  "abstract over free variables of definitional theorem"
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   226
7eb0c04e4c40 define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents: 55030
diff changeset
   227
26435
bdce320cd426 eliminated delayed theory setup
wenzelm
parents: 26426
diff changeset
   228
section {* Further content for the Pure theory *}
20627
30da2841553e revert to previous version;
wenzelm
parents: 20596
diff changeset
   229
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   230
subsection {* Meta-level connectives in assumptions *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   231
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   232
lemma meta_mp:
18019
wenzelm
parents: 15824
diff changeset
   233
  assumes "PROP P ==> PROP Q" and "PROP P"
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   234
  shows "PROP Q"
18019
wenzelm
parents: 15824
diff changeset
   235
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   236
23432
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
   237
lemmas meta_impE = meta_mp [elim_format]
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
   238
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   239
lemma meta_spec:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   240
  assumes "!!x. PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   241
  shows "PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   242
    by (rule `!!x. PROP P x`)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   243
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   244
lemmas meta_allE = meta_spec [elim_format]
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
   245
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
   246
lemma swap_params:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   247
  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
   248
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   249
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   250
subsection {* Meta-level conjunction *}
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   251
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   252
lemma all_conjunction:
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   253
  "(!!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
   254
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   255
  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
   256
  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   257
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   258
    fix x
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   259
    from conj show "PROP A x" by (rule conjunctionD1)
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   260
    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
   261
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   262
next
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   263
  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
   264
  fix x
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   265
  show "PROP A x &&& PROP B x"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   266
  proof -
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   267
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
   268
    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
   269
  qed
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
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   272
lemma imp_conjunction:
50603
3e3c2af5e8a5 removed odd associativity of ==
nipkow
parents: 50128
diff changeset
   273
  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
18836
3a1e4ee72075 tuned proofs;
wenzelm
parents: 18710
diff changeset
   274
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   275
  assume conj: "PROP A ==> PROP B &&& PROP C"
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   276
  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   277
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   278
    assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   279
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   280
    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
   281
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   282
next
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   283
  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
   284
  assume "PROP A"
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   285
  show "PROP B &&& PROP C"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   286
  proof -
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   287
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   288
    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
   289
  qed
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
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   292
lemma conjunction_imp:
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   293
  "(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
   294
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   295
  assume r: "PROP A &&& PROP B ==> PROP C"
22933
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
   296
  assume ab: "PROP A" "PROP B"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
   297
  show "PROP C"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
   298
  proof (rule r)
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
   299
    from ab show "PROP A &&& PROP B" .
22933
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
   300
  qed
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   301
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   302
  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
   303
  assume conj: "PROP A &&& PROP B"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   304
  show "PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   305
  proof (rule r)
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   306
    from conj show "PROP A" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
   307
    from conj show "PROP B" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   308
  qed
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
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 29606
diff changeset
   311
end
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 29606
diff changeset
   312