1.1 --- a/src/Pure/pure_thy.ML Thu Mar 27 14:41:17 2008 +0100
1.2 +++ b/src/Pure/pure_thy.ML Thu Mar 27 14:41:18 2008 +0100
1.3 @@ -2,23 +2,11 @@
1.4 ID: $Id$
1.5 Author: Markus Wenzel, TU Muenchen
1.6
1.7 -Theorem storage. The ProtoPure theory.
1.8 +Theorem storage. Pure theory syntax and logical content.
1.9 *)
1.10
1.11 -signature BASIC_PURE_THY =
1.12 -sig
1.13 - structure ProtoPure:
1.14 - sig
1.15 - val thy: theory
1.16 - val prop_def: thm
1.17 - val term_def: thm
1.18 - val conjunction_def: thm
1.19 - end
1.20 -end;
1.21 -
1.22 signature PURE_THY =
1.23 sig
1.24 - include BASIC_PURE_THY
1.25 val tag_rule: Markup.property -> thm -> thm
1.26 val untag_rule: string -> thm -> thm
1.27 val tag: Markup.property -> attribute
1.28 @@ -160,6 +148,8 @@
1.29 ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
1.30 );
1.31
1.32 +val _ = Context.>> TheoremsData.init;
1.33 +
1.34 val get_theorems_ref = TheoremsData.get;
1.35 val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
1.36 val theorems_of = #theorems o get_theorems;
1.37 @@ -431,7 +421,7 @@
1.38
1.39
1.40
1.41 -(*** the ProtoPure theory ***)
1.42 +(*** Pure theory syntax and logical content ***)
1.43
1.44 val typ = SimpleSyntax.read_typ;
1.45 val term = SimpleSyntax.read_term;
1.46 @@ -447,17 +437,14 @@
1.47 ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
1.48 ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
1.49
1.50 -val proto_pure =
1.51 - Context.pre_pure_thy
1.52 - |> Compress.init_data
1.53 - |> TheoremsData.init
1.54 - |> Sign.add_types
1.55 +val _ = Context.>>
1.56 + (Sign.add_types
1.57 [("fun", 2, NoSyn),
1.58 ("prop", 0, NoSyn),
1.59 ("itself", 1, NoSyn),
1.60 ("dummy", 0, NoSyn)]
1.61 - |> Sign.add_nonterminals Syntax.basic_nonterms
1.62 - |> Sign.add_syntax_i
1.63 + #> Sign.add_nonterminals Syntax.basic_nonterms
1.64 + #> Sign.add_syntax_i
1.65 [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
1.66 ("_abs", typ "'a", NoSyn),
1.67 ("", typ "'a => args", Delimfix "_"),
1.68 @@ -495,8 +482,8 @@
1.69 ("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
1.70 ("==>", typ "prop => prop => prop", Delimfix "op ==>"),
1.71 (Term.dummy_patternN, typ "aprop", Delimfix "'_")]
1.72 - |> Sign.add_syntax_i appl_syntax
1.73 - |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
1.74 + #> Sign.add_syntax_i appl_syntax
1.75 + #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
1.76 [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
1.77 ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
1.78 ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
1.79 @@ -511,49 +498,37 @@
1.80 ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
1.81 ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
1.82 ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
1.83 - |> Sign.add_modesyntax_i ("", false)
1.84 + #> Sign.add_modesyntax_i ("", false)
1.85 [("prop", typ "prop => prop", Mixfix ("_", [0], 0)),
1.86 - ("ProtoPure.term", typ "'a => prop", Delimfix "TERM _"),
1.87 - ("ProtoPure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))]
1.88 - |> Sign.add_modesyntax_i ("HTML", false)
1.89 + ("Pure.term", typ "'a => prop", Delimfix "TERM _"),
1.90 + ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))]
1.91 + #> Sign.add_modesyntax_i ("HTML", false)
1.92 [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
1.93 - |> Sign.add_consts_i
1.94 + #> Sign.add_consts_i
1.95 [("==", typ "'a => 'a => prop", InfixrName ("==", 2)),
1.96 ("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
1.97 ("all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
1.98 ("prop", typ "prop => prop", NoSyn),
1.99 ("TYPE", typ "'a itself", NoSyn),
1.100 (Term.dummy_patternN, typ "'a", Delimfix "'_")]
1.101 - |> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
1.102 - |> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
1.103 - |> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
1.104 - |> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
1.105 - |> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
1.106 - |> Sign.add_trfuns Syntax.pure_trfuns
1.107 - |> Sign.add_trfunsT Syntax.pure_trfunsT
1.108 - |> Sign.local_path
1.109 - |> Sign.add_consts_i
1.110 + #> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
1.111 + #> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
1.112 + #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
1.113 + #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
1.114 + #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
1.115 + #> Sign.add_trfuns Syntax.pure_trfuns
1.116 + #> Sign.add_trfunsT Syntax.pure_trfunsT
1.117 + #> Sign.local_path
1.118 + #> Sign.add_consts_i
1.119 [("term", typ "'a => prop", NoSyn),
1.120 ("conjunction", typ "prop => prop => prop", NoSyn)]
1.121 - |> (add_defs_i false o map Thm.no_attributes)
1.122 + #> (add_defs_i false o map Thm.no_attributes)
1.123 [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
1.124 - ("term_def", prop "(CONST ProtoPure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
1.125 - ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] |> snd
1.126 - |> Sign.hide_consts false ["conjunction", "term"]
1.127 - |> add_thmss [(("nothing", []), [])] |> snd
1.128 - |> Theory.add_axioms_i Proofterm.equality_axms
1.129 - |> Theory.end_theory;
1.130 -
1.131 -structure ProtoPure =
1.132 -struct
1.133 - val thy = proto_pure;
1.134 - val prop_def = get_axiom thy "prop_def";
1.135 - val term_def = get_axiom thy "term_def";
1.136 - val conjunction_def = get_axiom thy "conjunction_def";
1.137 -end;
1.138 + ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
1.139 + ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
1.140 + #> Sign.hide_consts false ["conjunction", "term"]
1.141 + #> add_thmss [(("nothing", []), [])] #> snd
1.142 + #> Theory.add_axioms_i Proofterm.equality_axms);
1.143
1.144 end;
1.145
1.146 -structure BasicPureThy: BASIC_PURE_THY = PureThy;
1.147 -open BasicPureThy;
1.148 -