# HG changeset patch # User wenzelm # Date 769357368 -7200 # Node ID 69f4356d915d023768156633a274e6aea3f283fe # Parent e9ba9f7e2542d4476dc7fea60007f77235942ae8 new datatype theory, supports 'draft theories' and incremental extension: add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i, add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname; added merge_thy_list for multiple merges and extend-merges; added rep_theory, subthy, eq_thy, cert_axm, read_axm; changed type of axioms_of; renamed internal merge_theories to merge_thm_sgs; various internal changes of thm and theory related code; diff -r e9ba9f7e2542 -r 69f4356d915d src/Pure/thm.ML --- a/src/Pure/thm.ML Thu May 19 16:20:52 1994 +0200 +++ b/src/Pure/thm.ML Thu May 19 16:22:48 1994 +0200 @@ -12,15 +12,15 @@ structure Envir : ENVIR structure Sequence : SEQUENCE structure Sign : SIGN + type ctyp type cterm - type ctyp + type thm + type theory type meta_simpset - type theory - type thm exception THM of string * int * thm list exception THEORY of string * theory list exception SIMPLIFIER of string * thm - (*Certified terms/types; previously in sign.ML*) + (*certified terms/types; previously in sign.ML*) val cterm_of: Sign.sg -> term -> cterm val ctyp_of: Sign.sg -> typ -> ctyp val read_ctyp: Sign.sg -> string -> ctyp @@ -30,14 +30,41 @@ val term_of: cterm -> term val typ_of: ctyp -> typ val cterm_fun: (term -> term) -> (cterm -> cterm) - (*End of cterm/ctyp functions*) + (*end of cterm/ctyp functions*) + + (* FIXME *) + local open Sign.Syntax Sign.Syntax.Mixfix in (* FIXME remove ...Mixfix *) + val add_classes: (class list * class * class list) list -> theory -> theory + val add_defsort: sort -> theory -> theory + val add_types: (string * int * mixfix) list -> theory -> theory + val add_tyabbrs: (string * string list * string * mixfix) list + -> theory -> theory + val add_tyabbrs_i: (string * string list * typ * mixfix) list + -> theory -> theory + val add_arities: (string * sort list * sort) list -> theory -> theory + val add_consts: (string * string * mixfix) list -> theory -> theory + val add_consts_i: (string * typ * mixfix) list -> theory -> theory + val add_syntax: (string * string * mixfix) list -> theory -> theory + val add_syntax_i: (string * typ * mixfix) list -> theory -> theory + val add_trfuns: + (string * (ast list -> ast)) list * + (string * (term list -> term)) list * + (string * (term list -> term)) list * + (string * (ast list -> ast)) list -> theory -> theory + val add_trrules: xrule list -> theory -> theory + val add_axioms: (string * string) list -> theory -> theory + val add_axioms_i: (string * term) list -> theory -> theory + val add_thyname: string -> theory -> theory + end + val cert_axm: Sign.sg -> string * term -> string * term + val read_axm: Sign.sg -> string * string -> string * term val abstract_rule: string -> cterm -> thm -> thm val add_congs: meta_simpset * thm list -> meta_simpset val add_prems: meta_simpset * thm list -> meta_simpset val add_simps: meta_simpset * thm list -> meta_simpset val assume: cterm -> thm val assumption: int -> thm -> thm Sequence.seq - val axioms_of: theory -> (string * thm) list + val axioms_of: theory -> (string * term) list val beta_conversion: cterm -> thm val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq @@ -72,6 +99,7 @@ -> thm -> thm val lift_rule: (thm * int) -> thm -> thm val merge_theories: theory * theory -> theory + val merge_thy_list: bool -> theory list -> theory val mk_rews_of_mss: meta_simpset -> thm -> thm list val mss_of: thm list -> meta_simpset val nprems_of: thm -> int @@ -89,6 +117,10 @@ bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option) -> cterm -> thm val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset + val rep_theory: theory -> + {sign: Sign.sg, ext_axtab: term Symtab.table, parents: theory list} + val subthy: theory * theory -> bool + val eq_thy: theory * theory -> bool val sign_of: theory -> Sign.sg val syn_of: theory -> Sign.Syntax.syntax val stamps_of_thm: thm -> string ref list @@ -102,7 +134,7 @@ end; functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN - and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) : THM = + and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)(*: THM *) (* FIXME debug *) = struct structure Sequence = Unify.Sequence; @@ -113,6 +145,8 @@ structure Symtab = Sign.Symtab; +(*** Certified terms and types ***) + (** certified types **) (*certified typs under a signature*) @@ -180,78 +214,224 @@ val ct = cterm_of sign t' handle TERM (msg, _) => error msg; in (ct, tye) end; -fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None)); +fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None); -(**** META-THEOREMS ****) +(*** Meta theorems ***) datatype thm = Thm of {sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; fun rep_thm (Thm args) = args; -(*Errors involving theorems*) +(*errors involving theorems*) exception THM of string * int * thm list; -(*maps object-rule to tpairs *) -fun tpairs_of (Thm{prop,...}) = #1 (Logic.strip_flexpairs prop); + +val sign_of_thm = #sign o rep_thm; +val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; -(*maps object-rule to premises *) -fun prems_of (Thm{prop,...}) = - Logic.strip_imp_prems (Logic.skip_flexpairs prop); +(*merge signatures of two theorems; raise exception if incompatible*) +fun merge_thm_sgs (th1, th2) = + Sign.merge (pairself sign_of_thm (th1, th2)) + handle TERM _ => raise THM ("incompatible signatures", 0, [th1, th2]); + + +(*maps object-rule to tpairs*) +fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); + +(*maps object-rule to premises*) +fun prems_of (Thm {prop, ...}) = + Logic.strip_imp_prems (Logic.skip_flexpairs prop); (*counts premises in a rule*) -fun nprems_of (Thm{prop,...}) = - Logic.count_prems (Logic.skip_flexpairs prop, 0); +fun nprems_of (Thm {prop, ...}) = + Logic.count_prems (Logic.skip_flexpairs prop, 0); -(*maps object-rule to conclusion *) -fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop; +(*maps object-rule to conclusion*) +fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; -(*The statement of any Thm is a Cterm*) -fun cprop_of (Thm{sign,maxidx,hyps,prop}) = - Cterm{sign=sign, maxidx=maxidx, T=propT, t=prop}; +(*the statement of any thm is a cterm*) +fun cprop_of (Thm {sign, maxidx, hyps, prop}) = + Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop}; -(*Stamps associated with a signature*) -val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; + -(*Theories. There is one pure theory. - A theory can be extended. Two theories can be merged.*) +(*** Theories ***) + datatype theory = - Pure of {sign: Sign.sg} - | Extend of {sign: Sign.sg, axioms: thm Symtab.table, thy: theory} - | Merge of {sign: Sign.sg, thy1: theory, thy2: theory}; + Theory of {sign: Sign.sg, ext_axtab: term Symtab.table, parents: theory list}; -(*Errors involving theories*) +fun rep_theory (Theory args) = args; + +(*errors involving theories*) exception THEORY of string * theory list; -fun sign_of (Pure {sign}) = sign - | sign_of (Extend {sign,...}) = sign - | sign_of (Merge {sign,...}) = sign; +val sign_of = #sign o rep_theory; val syn_of = #syn o Sign.rep_sg o sign_of; -(*return the axioms of a theory and its ancestors*) -fun axioms_of (Pure _) = [] - | axioms_of (Extend {axioms, thy, ...}) = - axioms_of thy @ Symtab.alist_of axioms - | axioms_of (Merge {thy1, thy2, ...}) = axioms_of thy1 @ axioms_of thy2; +(*stamps associated with a theory*) +val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; + +(*return additional axioms of this theory node*) +val axioms_of = Symtab.dest o #ext_axtab o rep_theory; + +(*return the immediate ancestors*) +val parents_of = #parents o rep_theory; + + +(*compare theories*) +val subthy = Sign.subsig o pairself sign_of; +val eq_thy = Sign.eq_sg o pairself sign_of; + + +(*look up the named axiom in the theory*) +fun get_axiom theory name = + let + fun get_ax [] = raise Match + | get_ax (Theory {sign, ext_axtab, parents} :: thys) = + (case Symtab.lookup (ext_axtab, name) of + Some t => + Thm {sign = sign, maxidx = maxidx_of_term t, hyps = [], prop = t} + | None => get_ax parents handle Match => get_ax thys); + in + get_ax [theory] handle Match + => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) + end; + + +(* the Pure theory *) + +val pure_thy = + Theory {sign = Sign.pure, ext_axtab = Symtab.null, parents = []}; + -(*return the immediate ancestors -- also distinguishes the kinds of theories*) -fun parents_of (Pure _) = [] - | parents_of (Extend{thy,...}) = [thy] - | parents_of (Merge{thy1,thy2,...}) = [thy1,thy2]; + +(** extend theory **) + +fun err_dup_axms names = + error ("Duplicate axiom name(s) " ^ commas_quote names); + +fun ext_thy (thy as Theory {sign, ext_axtab, parents}) sign1 new_axms = + let + val draft = Sign.is_draft sign; + val ext_axtab1 = + Symtab.extend_new (if draft then ext_axtab else Symtab.null, new_axms) + handle Symtab.DUPS names => err_dup_axms names; + val parents1 = if draft then parents else [thy]; + in + Theory {sign = sign1, ext_axtab = ext_axtab1, parents = parents1} + end; + + +(* extend signature of a theory *) + +fun ext_sg extfun decls (thy as Theory {sign, ...}) = + ext_thy thy (extfun decls sign) []; + +val add_classes = ext_sg Sign.add_classes; +val add_defsort = ext_sg Sign.add_defsort; +val add_types = ext_sg Sign.add_types; +val add_tyabbrs = ext_sg Sign.add_tyabbrs; +val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; +val add_arities = ext_sg Sign.add_arities; +val add_consts = ext_sg Sign.add_consts; +val add_consts_i = ext_sg Sign.add_consts_i; +val add_syntax = ext_sg Sign.add_syntax; +val add_syntax_i = ext_sg Sign.add_syntax_i; +val add_trfuns = ext_sg Sign.add_trfuns; +val add_trrules = ext_sg Sign.add_trrules; +val add_thyname = ext_sg Sign.add_name; -(*Merge theories of two theorems. Raise exception if incompatible. - Prefers (via Sign.merge) the signature of th1. *) -fun merge_theories(th1,th2) = - let val Thm{sign=sign1,...} = th1 and Thm{sign=sign2,...} = th2 - in Sign.merge (sign1,sign2) end - handle TERM _ => raise THM("incompatible signatures", 0, [th1,th2]); +(* prepare axioms *) + +fun err_in_axm name = + error ("The error(s) above occurred in axiom " ^ quote name); + +fun no_vars tm = + if null (term_vars tm) andalso null (term_tvars tm) then tm + else error "Illegal schematic variable(s) in term"; + +fun cert_axm sg (name, raw_tm) = + let + val Cterm {t, T, ...} = cterm_of sg raw_tm + handle TERM (msg, _) => error msg; + in + assert (T = propT) "Term not of type prop"; + (name, no_vars t) + end + handle ERROR => err_in_axm name; + +fun read_axm sg (name, str) = + (name, no_vars (term_of (read_cterm sg (str, propT)))) + handle ERROR => err_in_axm name; + + +(* extend axioms of a theory *) + +fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = + let + val sign1 = Sign.make_draft sign; + val new_axioms = map (apsnd Logic.varify o prep_axm sign) axms; + in + ext_thy thy sign1 new_axioms + end; + +val add_axioms = ext_axms read_axm; +val add_axioms_i = ext_axms cert_axm; + + +(* extend theory (old) *) (* FIXME remove *) -(*Stamps associated with a theory*) -val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; +(*converts Frees to Vars: axioms can be written without question marks*) +fun prepare_axiom sign sP = + Logic.varify (term_of (read_cterm sign (sP, propT))); + +(*read an axiom for a new theory*) +fun read_ax sign (a, sP) = + (a, prepare_axiom sign sP) handle ERROR => err_in_axm a; + +(*extension of a theory with given classes, types, constants and syntax; + reads the axioms from strings: axpairs have the form (axname, axiom)*) +fun extend_theory thy thyname ext axpairs = + let + val Theory {sign, ...} = thy; + + val sign1 = Sign.extend sign thyname ext; + val new_axioms = map (read_ax sign1) axpairs; + in + writeln "WARNING: called obsolete function \"extend_theory\""; + ext_thy thy sign1 new_axioms + end; + + + +(** merge theories **) + +fun merge_thy_list mk_draft thys = + let + fun is_union thy = forall (fn t => subthy (t, thy)) thys; + val is_draft = Sign.is_draft o sign_of; + + fun add_sign (sg, Theory {sign, ...}) = + Sign.merge (sg, sign) handle TERM (msg, _) => error msg; + in + (case (find_first is_union thys, exists is_draft thys) of + (Some thy, _) => thy + | (None, true) => raise THEORY ("Illegal merge of draft theories", thys) + | (None, false) => Theory { + sign = + (if mk_draft then Sign.make_draft else I) + (foldl add_sign (Sign.pure, thys)), + ext_axtab = Symtab.null, + parents = thys}) + end; + +fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; + (**** Primitive rules ****) @@ -295,7 +475,7 @@ in case prop of imp$A$B => if imp=implies andalso A aconv propA - then Thm{sign= merge_theories(thAB,thA), + then Thm{sign= merge_thm_sgs(thAB,thA), maxidx= max[maxA,maxidx], hyps= hypsA union hyps, (*dups suppressed*) prop= B} @@ -375,7 +555,7 @@ in case (prop1,prop2) of ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => if not (u aconv u') then err"middle term" else - Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, + Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, maxidx= max[max1,max2], prop= eq$t1$t2} | _ => err"premises" end; @@ -445,7 +625,7 @@ and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2 in case (prop1,prop2) of (Const("==",_) $ f $ g, Const("==",_) $ t $ u) => - Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, + Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} | _ => raise THM("combination: premises", 0, [th1,th2]) end; @@ -462,7 +642,7 @@ in case prop1 of Const("==",_) $ A $ B => if not (prop2 aconv A) then err"not equal" else - Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, + Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, maxidx= max[max1,max2], prop= B} | _ => err"major premise" end; @@ -479,7 +659,7 @@ in case (prop1,prop2) of (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => if A aconv A' andalso B aconv B' - then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, + then Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} else err"not equal" | _ => err"premises" @@ -607,7 +787,7 @@ val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); val (Thm{sign,maxidx,hyps,prop}) = orule val (tpairs,As,B) = Logic.strip_horn prop - in Thm{hyps=hyps, sign= merge_theories(state,orule), + in Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), maxidx= maxidx+smax+1, prop= Logic.rule_of(map (pairself lift_abs) tpairs, map lift_all As, lift_all B)} @@ -743,7 +923,7 @@ (eres_flg, orule, nsubgoal) = let val Thm{maxidx=smax, hyps=shyps, ...} = state and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule; - val sign = merge_theories(state,orule); + val sign = merge_thm_sgs(state,orule); (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = let val normt = Envir.norm_term env; @@ -827,51 +1007,6 @@ in Sequence.flats (res brules) end; -(**** THEORIES ****) - -val pure_thy = Pure{sign = Sign.pure}; - -(*Look up the named axiom in the theory*) -fun get_axiom thy axname = - let fun get (Pure _) = raise Match - | get (Extend{axioms,thy,...}) = - (case Symtab.lookup(axioms,axname) of - Some th => th - | None => get thy) - | get (Merge{thy1,thy2,...}) = - get thy1 handle Match => get thy2 - in get thy - handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy]) - end; - -(*Converts Frees to Vars: axioms can be written without question marks*) -fun prepare_axiom sign sP = - Logic.varify (term_of (read_cterm sign (sP,propT))); - -(*Read an axiom for a new theory*) -fun read_ax sign (a, sP) : string*thm = - let val prop = prepare_axiom sign sP - in (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop}) - end - handle ERROR => - error("extend_theory: The error above occurred in axiom " ^ a); - -fun mk_axioms sign axpairs = - Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null) - handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a); - -(*Extension of a theory with given classes, types, constants and syntax. - Reads the axioms from strings: axpairs have the form (axname, axiom). *) -fun extend_theory thy thyname ext axpairs = - let val sign = Sign.extend (sign_of thy) thyname ext; - val axioms= mk_axioms sign axpairs - in Extend{sign=sign, axioms= axioms, thy = thy} end; - -(*The union of two theories*) -fun merge_theories (thy1, thy2) = - Merge {sign = Sign.merge (sign_of thy1, sign_of thy2), - thy1 = thy1, thy2 = thy2} handle TERM (msg, _) => error msg; - (*** Meta simp sets ***)