# HG changeset patch # User wenzelm # Date 1206625278 -3600 # Node ID 8ddb2e7c5a1e993c2802270c025a843e0e3a0c9d # Parent 1afbc0139b1b00aaf4fe77a36823da6b06ac5603 eliminated theory ProtoPure; implicit setup of emerging theory Pure; diff -r 1afbc0139b1b -r 8ddb2e7c5a1e src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Mar 27 14:41:17 2008 +0100 +++ b/src/Pure/pure_thy.ML Thu Mar 27 14:41:18 2008 +0100 @@ -2,23 +2,11 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Theorem storage. The ProtoPure theory. +Theorem storage. Pure theory syntax and logical content. *) -signature BASIC_PURE_THY = -sig - structure ProtoPure: - sig - val thy: theory - val prop_def: thm - val term_def: thm - val conjunction_def: thm - end -end; - signature PURE_THY = sig - include BASIC_PURE_THY val tag_rule: Markup.property -> thm -> thm val untag_rule: string -> thm -> thm val tag: Markup.property -> attribute @@ -160,6 +148,8 @@ ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2))); ); +val _ = Context.>> TheoremsData.init; + val get_theorems_ref = TheoremsData.get; val get_theorems = (fn Thms args => args) o ! o get_theorems_ref; val theorems_of = #theorems o get_theorems; @@ -431,7 +421,7 @@ -(*** the ProtoPure theory ***) +(*** Pure theory syntax and logical content ***) val typ = SimpleSyntax.read_typ; val term = SimpleSyntax.read_term; @@ -447,17 +437,14 @@ ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)), ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))]; -val proto_pure = - Context.pre_pure_thy - |> Compress.init_data - |> TheoremsData.init - |> Sign.add_types +val _ = Context.>> + (Sign.add_types [("fun", 2, NoSyn), ("prop", 0, NoSyn), ("itself", 1, NoSyn), ("dummy", 0, NoSyn)] - |> Sign.add_nonterminals Syntax.basic_nonterms - |> Sign.add_syntax_i + #> Sign.add_nonterminals Syntax.basic_nonterms + #> Sign.add_syntax_i [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), ("", typ "'a => args", Delimfix "_"), @@ -495,8 +482,8 @@ ("_struct", typ "index => logic", Mixfix ("\\_", [1000], 1000)), ("==>", typ "prop => prop => prop", Delimfix "op ==>"), (Term.dummy_patternN, typ "aprop", Delimfix "'_")] - |> Sign.add_syntax_i appl_syntax - |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) + #> Sign.add_syntax_i appl_syntax + #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [("fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), @@ -511,49 +498,37 @@ ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] - |> Sign.add_modesyntax_i ("", false) + #> Sign.add_modesyntax_i ("", false) [("prop", typ "prop => prop", Mixfix ("_", [0], 0)), - ("ProtoPure.term", typ "'a => prop", Delimfix "TERM _"), - ("ProtoPure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))] - |> Sign.add_modesyntax_i ("HTML", false) + ("Pure.term", typ "'a => prop", Delimfix "TERM _"), + ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))] + #> Sign.add_modesyntax_i ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] - |> Sign.add_consts_i + #> Sign.add_consts_i [("==", typ "'a => 'a => prop", InfixrName ("==", 2)), ("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), ("all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), ("prop", typ "prop => prop", NoSyn), ("TYPE", typ "'a itself", NoSyn), (Term.dummy_patternN, typ "'a", Delimfix "'_")] - |> Theory.add_deps "==" ("==", typ "'a => 'a => prop") [] - |> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") [] - |> Theory.add_deps "all" ("all", typ "('a => prop) => prop") [] - |> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") [] - |> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] - |> Sign.add_trfuns Syntax.pure_trfuns - |> Sign.add_trfunsT Syntax.pure_trfunsT - |> Sign.local_path - |> Sign.add_consts_i + #> Theory.add_deps "==" ("==", typ "'a => 'a => prop") [] + #> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") [] + #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") [] + #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") [] + #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] + #> Sign.add_trfuns Syntax.pure_trfuns + #> Sign.add_trfunsT Syntax.pure_trfunsT + #> Sign.local_path + #> Sign.add_consts_i [("term", typ "'a => prop", NoSyn), ("conjunction", typ "prop => prop => prop", NoSyn)] - |> (add_defs_i false o map Thm.no_attributes) + #> (add_defs_i false o map Thm.no_attributes) [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), - ("term_def", prop "(CONST ProtoPure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), - ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] |> snd - |> Sign.hide_consts false ["conjunction", "term"] - |> add_thmss [(("nothing", []), [])] |> snd - |> Theory.add_axioms_i Proofterm.equality_axms - |> Theory.end_theory; - -structure ProtoPure = -struct - val thy = proto_pure; - val prop_def = get_axiom thy "prop_def"; - val term_def = get_axiom thy "term_def"; - val conjunction_def = get_axiom thy "conjunction_def"; -end; + ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), + ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd + #> Sign.hide_consts false ["conjunction", "term"] + #> add_thmss [(("nothing", []), [])] #> snd + #> Theory.add_axioms_i Proofterm.equality_axms); end; -structure BasicPureThy: BASIC_PURE_THY = PureThy; -open BasicPureThy; -