# HG changeset patch # User wenzelm # Date 1120050811 -7200 # Node ID ee8eefade5684ab7c78eb8c303e5095b0514195e # Parent 55ffcee3b8f3aea72cde2101e07f19ba0f6cae50 more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML; diff -r 55ffcee3b8f3 -r ee8eefade568 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Jun 29 15:13:30 2005 +0200 +++ b/src/Pure/thm.ML Wed Jun 29 15:13:31 2005 +0200 @@ -20,8 +20,10 @@ (*certified terms*) type cterm exception CTERM of string - val rep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: typ, maxidx: int} - val crep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int} + val rep_cterm: cterm -> + {thy: theory, sign: theory, t: term, T: typ, maxidx: int, sorts: sort list} + val crep_cterm: cterm -> + {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list} val theory_of_cterm: cterm -> theory val sign_of_cterm: cterm -> theory (*obsolete*) val term_of: cterm -> term @@ -95,7 +97,6 @@ val combination: thm -> thm -> thm val equal_intr: thm -> thm -> thm val equal_elim: thm -> thm -> thm - val implies_intr_hyps: thm -> thm val flexflex_rule: thm -> thm Seq.seq val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm val trivial: cterm -> thm @@ -167,23 +168,28 @@ fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) = map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts - | dest_ctyp ct = [ct]; + | dest_ctyp cT = [cT]; (** certified terms **) -(*certified terms with checked typ and maxidx of Vars/TVars*) +(*certified terms with checked typ, maxidx, and sorts*) +datatype cterm = Cterm of + {thy_ref: theory_ref, + t: term, + T: typ, + maxidx: int, + sorts: sort list}; -datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int}; - -fun rep_cterm (Cterm {thy_ref, t, T, maxidx}) = +fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = let val thy = Theory.deref thy_ref - in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx} end; + in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; -fun crep_cterm (Cterm {thy_ref, t, T, maxidx}) = +fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = let val thy = Theory.deref thy_ref in - {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx} + {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, + maxidx = maxidx, sorts = sorts} end; fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; @@ -194,85 +200,87 @@ fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T}; fun cterm_of thy tm = - let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm - in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx} - end; - + let + val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm; + val sorts = Sorts.insert_term t []; + in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; exception CTERM of string; (*Destruct application in cterms*) -fun dest_comb (Cterm {thy_ref, T, maxidx, t = A $ B}) = +fun dest_comb (Cterm {thy_ref, T, maxidx, sorts, t = A $ B}) = let val typeA = fastype_of A; val typeB = case typeA of Type("fun",[S,T]) => S - | _ => error "Function type expected in dest_comb"; + | _ => sys_error "Function type expected in dest_comb"; in - (Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA}, - Cterm {thy_ref=thy_ref, maxidx=maxidx, t=B, T=typeB}) + (Cterm {thy_ref=thy_ref, maxidx=maxidx, sorts=sorts, t=A, T=typeA}, + Cterm {thy_ref=thy_ref, maxidx=maxidx, sorts=sorts, t=B, T=typeB}) end | dest_comb _ = raise CTERM "dest_comb"; (*Destruct abstraction in cterms*) -fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = +fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, sorts, t=Abs(x,ty,M)}) = let val (y,N) = variant_abs (if_none a x, ty, M) - in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)}, - Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, t = N}) + in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, sorts = sorts, t = Free(y,ty)}, + Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, sorts = sorts, t = N}) end | dest_abs _ _ = raise CTERM "dest_abs"; (*Makes maxidx precise: it is often too big*) -fun adjust_maxidx (ct as Cterm {thy_ref, T, t, maxidx, ...}) = +fun adjust_maxidx (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = if maxidx = ~1 then ct - else Cterm {thy_ref = thy_ref, T = T, maxidx = maxidx_of_term t, t = t}; + else Cterm {thy_ref = thy_ref, t = t, T = T, maxidx = maxidx_of_term t, sorts = sorts}; (*Form cterm out of a function and an argument*) -fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) - (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) = - if T = dty then - Cterm{t = f $ x, - thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty, - maxidx=Int.max(maxidx1, maxidx2)} +fun capply + (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1, sorts = sorts1}) + (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2, sorts = sorts2}) = + if T = dty then + Cterm{t = f $ x, + thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty, + maxidx=Int.max(maxidx1, maxidx2), + sorts = Sorts.union sorts1 sorts2} else raise CTERM "capply: types don't agree" | capply _ _ = raise CTERM "capply: first arg is not a function" -fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1}) - (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) = - Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2), - T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} - handle TERM _ => raise CTERM "cabs: first arg is not a variable"; +fun cabs + (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1, sorts = sorts1}) + (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2, sorts = sorts2}) = + let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: first arg is not a variable" in + Cterm {t = t, T = T1 --> T2, thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), + maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} + end; (*Matching of cterms*) fun gen_cterm_match mtch - (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...}, - Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, ...}) = + (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, sorts = sorts1, ...}, + Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, sorts = sorts2, ...}) = let val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2); val tsig = Sign.tsig_of (Theory.deref thy_ref); val (Tinsts, tinsts) = mtch tsig (t1, t2); val maxidx = Int.max (maxidx1, maxidx2); + val sorts = Sorts.union sorts1 sorts2; fun mk_cTinsts (ixn, (S, T)) = (Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)}, Ctyp {thy_ref = thy_ref, T = T}); fun mk_ctinsts (ixn, (T, t)) = - let val T = Envir.typ_subst_TVars Tinsts T - in - (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t}) + let val T = Envir.typ_subst_TVars Tinsts T in + (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T), sorts = sorts}, + Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t, sorts = sorts}) end; - in (map mk_cTinsts (Vartab.dest Tinsts), - map mk_ctinsts (Vartab.dest tinsts)) - end; + in (map mk_cTinsts (Vartab.dest Tinsts), map mk_ctinsts (Vartab.dest tinsts)) end; val cterm_match = gen_cterm_match Pattern.match; val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; (*Incrementing indexes*) -fun cterm_incr_indexes i (ct as Cterm {thy_ref, maxidx, t, T}) = - if i < 0 then raise CTERM "negative increment" else - if i = 0 then ct else - Cterm {thy_ref = thy_ref, maxidx = maxidx + i, - t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T}; +fun cterm_incr_indexes i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = + if i < 0 then raise CTERM "negative increment" + else if i = 0 then ct + else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, + T = Term.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; @@ -307,12 +315,13 @@ {thy_ref: theory_ref, (*dynamic reference to theory*) der: bool * Pt.proof, (*derivation*) maxidx: int, (*maximum index of any Var or TVar*) - shyps: sort list, (*sort hypotheses*) - hyps: term list, (*hypotheses*) + shyps: sort list, (*sort hypotheses as ordered list*) + hyps: term list, (*hypotheses as ordered list*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term}; (*conclusion*) fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); +val union_tpairs = gen_merge_lists (op = : (term * term) * (term * term) -> bool); fun attach_tpairs tpairs prop = Logic.list_implies (map Logic.mk_equals tpairs, prop); @@ -327,7 +336,7 @@ fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = let val thy = Theory.deref thy_ref; - fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max}; + fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps}; in {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps, hyps = map (cterm ~1) hyps, @@ -345,6 +354,16 @@ fun apply_attributes (x_th, atts) = Library.apply atts x_th; fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; + +(* shyps and hyps *) + +val remove_hyps = OrdList.remove Term.term_ord; +val union_hyps = OrdList.union Term.term_ord; +val eq_set_hyps = OrdList.eq_set Term.term_ord; + + +(* eq_thm(s) *) + fun eq_thm (th1, th2) = let val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = @@ -352,9 +371,9 @@ val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = rep_thm th2; in - (subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso - Sorts.eq_set_sort (shyps1, shyps2) andalso - aconvs (hyps1, hyps2) andalso + Context.joinable (thy1, thy2) andalso + Sorts.eq_set (shyps1, shyps2) andalso + eq_set_hyps (hyps1, hyps2) andalso aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso prop1 aconv prop2 end; @@ -366,13 +385,36 @@ fun prop_of (Thm {prop, ...}) = prop; fun proof_of (Thm {der = (_, proof), ...}) = proof; +fun tpairs_of (Thm {tpairs, ...}) = tpairs; -(*merge theories of two theorems; raise exception if incompatible*) -fun merge_thm_thys - (th1 as Thm {thy_ref = r1, ...}, th2 as Thm {thy_ref = r2, ...}) = +val concl_of = Logic.strip_imp_concl o prop_of; +val prems_of = Logic.strip_imp_prems o prop_of; +fun nprems_of th = Logic.count_prems (prop_of th, 0); +val no_prems = equal 0 o nprems_of; + +fun major_prem_of th = + (case prems_of th of + prem :: _ => Logic.strip_assums_concl prem + | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); + +(*the statement of any thm is a cterm*) +fun cprop_of (Thm {thy_ref, maxidx, shyps, prop, ...}) = + Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; + + +(* merge theories of cterms/thms; raise exception if incompatible *) + +fun merge_thys1 + (Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) = + Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th]); + +fun merge_thys2 + (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) = Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); -(*transfer thm to super theory (non-destructive)*) + +(* explicit transfer thm to super theory *) + fun transfer thy' thm = let val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; @@ -385,92 +427,21 @@ else raise THM ("transfer: not a super theory", 0, [thm]) end; -(*maps object-rule to tpairs*) -fun tpairs_of (Thm {tpairs, ...}) = tpairs; - -(*maps object-rule to premises*) -fun prems_of (Thm {prop, ...}) = - Logic.strip_imp_prems prop; - -(*counts premises in a rule*) -fun nprems_of (Thm {prop, ...}) = - Logic.count_prems (prop, 0); - -fun major_prem_of thm = - (case prems_of thm of - prem :: _ => Logic.strip_assums_concl prem - | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); - -fun no_prems thm = nprems_of thm = 0; - -(*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 {thy_ref, maxidx, prop, ...}) = - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop}; - (** sort contexts of theorems **) -(* basic utils *) - -(*accumulate sorts suppressing duplicates; these are coded low levelly - to improve efficiency a bit*) - -fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) - | add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss) - | add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss) -and add_typs_sorts ([], Ss) = Ss - | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); - -fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss) - | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss) - | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss) - | add_term_sorts (Bound _, Ss) = Ss - | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) - | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); - -fun add_terms_sorts ([], Ss) = Ss - | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); - -fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs); - -fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = - Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) - (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); +fun insert_env_sorts (env as Envir.Envir {iTs, asol, ...}) = + Vartab.fold (fn (_, (_, t)) => Sorts.insert_term t) asol o + Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) iTs; -fun add_insts_sorts ((iTs, is), Ss) = - add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); - -fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = - add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); - -fun add_thms_shyps ([], Ss) = Ss - | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) = - add_thms_shyps (ths, Sorts.union_sort (shyps, Ss)); - - -(*get 'dangling' sort constraints of a thm*) -fun extra_shyps (th as Thm {shyps, ...}) = - Sorts.rems_sort (shyps, add_thm_sorts (th, [])); +fun insert_thm_sorts (Thm {hyps, tpairs, prop, ...}) = + fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs o + Sorts.insert_terms hyps o Sorts.insert_term prop; - -(* fix_shyps *) - -val all_sorts_nonempty = is_some o Sign.universal_witness o Theory.deref; - -(*preserve sort contexts of rule premises and substituted types*) -fun fix_shyps thms Ts (thm as Thm {thy_ref, der, maxidx, hyps, tpairs, prop, ...}) = - Thm - {thy_ref = thy_ref, - der = der, (*no new derivation, as other rules call this*) - maxidx = maxidx, - shyps = - if all_sorts_nonempty thy_ref then [] - else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))), - hyps = hyps, tpairs = tpairs, prop = prop} +(*dangling sort constraints of a thm*) +fun extra_shyps (th as Thm {shyps, ...}) = + Sorts.subtract (insert_thm_sorts th []) shyps; (* strip_shyps *) @@ -480,12 +451,12 @@ | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = let val thy = Theory.deref thy_ref; - val present_sorts = add_thm_sorts (thm, []); - val extra_shyps = Sorts.rems_sort (shyps, present_sorts); + val present_sorts = insert_thm_sorts thm []; + val extra_shyps = Sorts.subtract present_sorts shyps; val witnessed_shyps = Sign.witness_sorts thy present_sorts extra_shyps; in Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, - shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps), + shyps = Sorts.subtract (map #2 witnessed_shyps) shyps, hyps = hyps, tpairs = tpairs, prop = prop} end; @@ -498,15 +469,14 @@ let fun get_ax thy = Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name) - |> Option.map (fn t => - fix_shyps [] [] - (Thm {thy_ref = Theory.self_ref thy, - der = Pt.infer_derivs' I (false, Pt.axm_proof name t), - maxidx = maxidx_of_term t, - shyps = [], - hyps = [], - tpairs = [], - prop = t})); + |> Option.map (fn prop => + Thm {thy_ref = Theory.self_ref thy, + der = Pt.infer_derivs' I (false, Pt.axm_proof name prop), + maxidx = maxidx_of_term prop, + shyps = Sorts.insert_term prop [], + hyps = [], + tpairs = [], + prop = prop}); in (case get_first get_ax (theory :: Theory.ancestors_of theory) of SOME thm => thm @@ -559,26 +529,22 @@ (*** Meta rules ***) -(** 'primitive' rules **) - -(*discharge all assumptions t from ts*) -val disch = gen_rem (op aconv); +(** primitive rules **) -(*The assumption rule A|-A in a theory*) -fun assume raw_ct : thm = - let val ct as Cterm {thy_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct - in if T<>propT then - raise THM("assume: assumptions must have type prop", 0, []) - else if maxidx <> ~1 then - raise THM("assume: assumptions may not contain scheme variables", - maxidx, []) - else Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' I (false, Pt.Hyp prop), - maxidx = ~1, - shyps = add_term_sorts(prop,[]), - hyps = [prop], - tpairs = [], - prop = prop} +(*The assumption rule A |- A in a theory*) +fun assume raw_ct = + let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx raw_ct in + if T <> propT then + raise THM ("assume: assumptions must have type prop", 0, []) + else if maxidx <> ~1 then + raise THM ("assume: assumptions may not contain schematic variables", maxidx, []) + else Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' I (false, Pt.Hyp prop), + maxidx = ~1, + shyps = sorts, + hyps = [prop], + tpairs = [], + prop = prop} end; (*Implication introduction @@ -588,21 +554,19 @@ ------- A ==> B *) -fun implies_intr cA (thB as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm = - let val Cterm {thy_ref=thy_refA, t=A, T, maxidx=maxidxA} = cA - in if T<>propT then - raise THM("implies_intr: assumptions must have type prop", 0, [thB]) - else - Thm{thy_ref = Theory.merge_refs (thy_ref,thy_refA), - der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, - maxidx = Int.max(maxidxA, maxidx), - shyps = add_term_sorts (A, shyps), - hyps = disch(hyps,A), - tpairs = tpairs, - prop = implies$A$prop} - handle TERM _ => - raise THM("implies_intr: incompatible theories", 0, [thB]) - end; +fun implies_intr + (ct as Cterm {thy_ref = thy_refA, t = A, T, maxidx = maxidxA, sorts}) + (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = + if T <> propT then + raise THM ("implies_intr: assumptions must have type prop", 0, [th]) + else + Thm {thy_ref = merge_thys1 ct th, + der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, + maxidx = Int.max (maxidxA, maxidx), + shyps = Sorts.union sorts shyps, + hyps = remove_hyps A hyps, + tpairs = tpairs, + prop = implies $ A $ prop}; (*Implication elimination @@ -610,48 +574,55 @@ ------------ B *) -fun implies_elim thAB thA : thm = - let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, tpairs=tpairsA, prop=propA, ...} = thA - and Thm{der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; - fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) - in case prop of - imp$A$B => - if imp=implies andalso A aconv propA - then - Thm{thy_ref= merge_thm_thys (thAB, thA), - der = Pt.infer_derivs (curry Pt.%%) der derA, - maxidx = Int.max(maxA,maxidx), - shyps = Sorts.union_sort (shypsA, shyps), - hyps = union_term(hypsA,hyps), (*dups suppressed*) - tpairs = tpairsA @ tpairs, - prop = B} - else err("major premise") - | _ => err("major premise") - end; +fun implies_elim thAB thA = + let + val Thm {maxidx = maxA, der = derA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA, + prop = propA, ...} = thA + and Thm {der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; + fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); + in + case prop of + imp $ A $ B => + if imp = Term.implies andalso A aconv propA then + Thm {thy_ref= merge_thys2 thAB thA, + der = Pt.infer_derivs (curry Pt.%%) der derA, + maxidx = Int.max (maxA, maxidx), + shyps = Sorts.union shypsA shyps, + hyps = union_hyps hypsA hyps, + tpairs = union_tpairs tpairsA tpairs, + prop = B} + else err () + | _ => err () + end; (*Forall introduction. The Free or Var x must not be free in the hypotheses. + [x] + : A ----- !!x.A *) -fun forall_intr cx (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) = - let val x = term_of cx; - fun result a T = fix_shyps [th] [] - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, - maxidx = maxidx, - shyps = [], - hyps = hyps, - tpairs = tpairs, - prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) - fun check_occs x ts = - if exists (apl(x, Logic.occs)) ts - then raise THM("forall_intr: variable free in assumptions", 0, [th]) - else () - in case x of - Free(a,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result a T) - | Var((a,_),T) => (check_occs x (terms_of_tpairs tpairs); result a T) - | _ => raise THM("forall_intr: not a variable", 0, [th]) +fun forall_intr + (ct as Cterm {t = x, T, sorts, ...}) + (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = + let + fun result a = + Thm {thy_ref = merge_thys1 ct th, + der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, + maxidx = maxidx, + shyps = Sorts.union sorts shyps, + hyps = hyps, + tpairs = tpairs, + prop = all T $ Abs (a, T, abstract_over (x, prop))}; + fun check_occs x ts = + if exists (apl (x, Logic.occs)) ts then + raise THM("forall_intr: variable free in assumptions", 0, [th]) + else (); + in + case x of + Free (a, _) => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result a) + | Var ((a, _), _) => (check_occs x (terms_of_tpairs tpairs); result a) + | _ => raise THM ("forall_intr: not a variable", 0, [th]) end; (*Forall elimination @@ -659,224 +630,227 @@ ------ A[t/x] *) -fun forall_elim ct (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) : thm = - let val Cterm {thy_ref=thy_reft, t, T, maxidx=maxt} = ct - in case prop of - Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => - if T<>qary then - raise THM("forall_elim: type mismatch", 0, [th]) - else fix_shyps [th] [] - (Thm{thy_ref= Theory.merge_refs(thy_ref,thy_reft), - der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, - maxidx = Int.max(maxidx, maxt), - shyps = [], - hyps = hyps, - tpairs = tpairs, - prop = betapply(A,t)}) - | _ => raise THM("forall_elim: not quantified", 0, [th]) - end - handle TERM _ => - raise THM("forall_elim: incompatible theories", 0, [th]); +fun forall_elim + (ct as Cterm {t, T, maxidx = maxt, sorts, ...}) + (th as Thm {der, maxidx, shyps, hyps, tpairs, prop, ...}) = + (case prop of + Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => + if T <> qary then + raise THM ("forall_elim: type mismatch", 0, [th]) + else + Thm {thy_ref = merge_thys1 ct th, + der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, + maxidx = Int.max (maxidx, maxt), + shyps = Sorts.union sorts shyps, + hyps = hyps, + tpairs = tpairs, + prop = Term.betapply (A, t)} + | _ => raise THM ("forall_elim: not quantified", 0, [th])); (* Equality *) -(*The reflexivity rule: maps t to the theorem t==t *) -fun reflexive ct = - let val Cterm {thy_ref, t, T, maxidx} = ct - in Thm{thy_ref= thy_ref, - der = Pt.infer_derivs' I (false, Pt.reflexive), - shyps = add_term_sorts (t, []), - hyps = [], - maxidx = maxidx, - tpairs = [], - prop = Logic.mk_equals(t,t)} - end; +(*Reflexivity + t == t +*) +fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = + Thm {thy_ref= thy_ref, + der = Pt.infer_derivs' I (false, Pt.reflexive), + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = Logic.mk_equals (t, t)}; -(*The symmetry rule - t==u - ---- - u==t +(*Symmetry + t == u + ------ + u == t *) -fun symmetric (th as Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = - case prop of - (eq as Const("==", Type (_, [T, _]))) $ t $ u => - (*no fix_shyps*) - Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' Pt.symmetric der, - maxidx = maxidx, - shyps = shyps, - hyps = hyps, - tpairs = tpairs, - prop = eq$u$t} - | _ => raise THM("symmetric", 0, [th]); +fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = + (case prop of + (eq as Const ("==", Type (_, [T, _]))) $ t $ u => + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' Pt.symmetric der, + maxidx = maxidx, + shyps = shyps, + hyps = hyps, + tpairs = tpairs, + prop = eq $ u $ t} + | _ => raise THM ("symmetric", 0, [th])); -(*The transitive rule - t1==u u==t2 - -------------- - t1==t2 +(*Transitivity + t1 == u u == t2 + ------------------ + t1 == t2 *) fun transitive th1 th2 = - let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1 - and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2; - fun err msg = raise THM("transitive: "^msg, 0, [th1,th2]) - in case (prop1,prop2) of - ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => - if not (u aconv u') then err"middle term" - else - Thm{thy_ref= merge_thm_thys (th1, th2), - der = Pt.infer_derivs (Pt.transitive u T) der1 der2, - maxidx = Int.max(max1,max2), - shyps = Sorts.union_sort (shyps1, shyps2), - hyps = union_term(hyps1,hyps2), - tpairs = tpairs1 @ tpairs2, - prop = eq$t1$t2} - | _ => err"premises" + let + val Thm {der = der1, maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1, + prop = prop1, ...} = th1 + and Thm {der = der2, maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2, + prop = prop2, ...} = th2; + fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); + in + case (prop1, prop2) of + ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) => + if not (u aconv u') then err "middle term" + else + Thm {thy_ref= merge_thys2 th1 th2, + der = Pt.infer_derivs (Pt.transitive u T) der1 der2, + maxidx = Int.max (max1, max2), + shyps = Sorts.union shyps1 shyps2, + hyps = union_hyps hyps1 hyps2, + tpairs = union_tpairs tpairs1 tpairs2, + prop = eq $ t1 $ t2} + | _ => err "premises" end; -(*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] - Fully beta-reduces the term if full=true +(*Beta-conversion + (%x.t)(u) == t[u/x] + fully beta-reduces the term if full = true *) -fun beta_conversion full ct = - let val Cterm {thy_ref, t, T, maxidx} = ct - in Thm - {thy_ref = thy_ref, - der = Pt.infer_derivs' I (false, Pt.reflexive), - maxidx = maxidx, - shyps = add_term_sorts (t, []), - hyps = [], - tpairs = [], - prop = Logic.mk_equals (t, if full then Envir.beta_norm t - else case t of - Abs(_, _, bodt) $ u => subst_bound (u, bodt) - | _ => raise THM ("beta_conversion: not a redex", 0, []))} +fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) = + let val t' = + if full then Envir.beta_norm t + else + (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) + | _ => raise THM ("beta_conversion: not a redex", 0, [])); + in + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' I (false, Pt.reflexive), + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = Logic.mk_equals (t, t')} end; -fun eta_conversion ct = - let val Cterm {thy_ref, t, T, maxidx} = ct - in Thm - {thy_ref = thy_ref, - der = Pt.infer_derivs' I (false, Pt.reflexive), - maxidx = maxidx, - shyps = add_term_sorts (t, []), - hyps = [], - tpairs = [], - prop = Logic.mk_equals (t, Pattern.eta_contract t)} - end; +fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' I (false, Pt.reflexive), + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = Logic.mk_equals (t, Pattern.eta_contract t)}; (*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) - t == u - ------------ - %x.t == %x.u + t == u + -------------- + %x. t == %x. u *) -fun abstract_rule a cx (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) = - let val x = term_of cx; - val (t,u) = Logic.dest_equals prop - handle TERM _ => - raise THM("abstract_rule: premise not an equality", 0, [th]) - fun result T = - Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.abstract_rule x a) der, - maxidx = maxidx, - shyps = add_typ_sorts (T, shyps), - hyps = hyps, - tpairs = tpairs, - prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), - Abs(a, T, abstract_over (x,u)))} - fun check_occs x ts = - if exists (apl(x, Logic.occs)) ts - then raise THM("abstract_rule: variable free in assumptions", 0, [th]) - else () - in case x of - Free(_,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result T) - | Var(_,T) => (check_occs x (terms_of_tpairs tpairs); result T) - | _ => raise THM("abstract_rule: not a variable", 0, [th]) +fun abstract_rule a + (Cterm {t = x, T, sorts, ...}) + (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = + let + val (t, u) = Logic.dest_equals prop + handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); + val result = + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.abstract_rule x a) der, + maxidx = maxidx, + shyps = Sorts.union sorts shyps, + hyps = hyps, + tpairs = tpairs, + prop = Logic.mk_equals + (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}; + fun check_occs x ts = + if exists (apl (x, Logic.occs)) ts then + raise THM ("abstract_rule: variable free in assumptions", 0, [th]) + else (); + in + case x of + Free _ => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result) + | Var _ => (check_occs x (terms_of_tpairs tpairs); result) + | _ => raise THM ("abstract_rule: not a variable", 0, [th]) end; (*The combination rule f == g t == u -------------- - f(t) == g(u) + f t == g u *) fun combination th1 th2 = - let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, - tpairs=tpairs1, prop=prop1,...} = th1 - and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, - tpairs=tpairs2, prop=prop2,...} = th2 - fun chktypes fT tT = - (case fT of - Type("fun",[T1,T2]) => - if T1 <> tT then - raise THM("combination: types", 0, [th1,th2]) - else () - | _ => raise THM("combination: not function type", 0, - [th1,th2])) - in case (prop1,prop2) of - (Const ("==", Type ("fun", [fT, _])) $ f $ g, - Const ("==", Type ("fun", [tT, _])) $ t $ u) => - (chktypes fT tT; - (*no fix_shyps*) - Thm{thy_ref = merge_thm_thys(th1,th2), - der = Pt.infer_derivs - (Pt.combination f g t u fT) der1 der2, - maxidx = Int.max(max1,max2), - shyps = Sorts.union_sort(shyps1,shyps2), - hyps = union_term(hyps1,hyps2), - tpairs = tpairs1 @ tpairs2, - prop = Logic.mk_equals(f$t, g$u)}) - | _ => raise THM("combination: premises", 0, [th1,th2]) + let + val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, + prop = prop1, ...} = th1 + and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, + prop = prop2, ...} = th2; + fun chktypes fT tT = + (case fT of + Type ("fun", [T1, T2]) => + if T1 <> tT then + raise THM ("combination: types", 0, [th1, th2]) + else () + | _ => raise THM ("combination: not function type", 0, [th1, th2])); + in + case (prop1, prop2) of + (Const ("==", Type ("fun", [fT, _])) $ f $ g, + Const ("==", Type ("fun", [tT, _])) $ t $ u) => + (chktypes fT tT; + Thm {thy_ref = merge_thys2 th1 th2, + der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2, + maxidx = Int.max (max1, max2), + shyps = Sorts.union shyps1 shyps2, + hyps = union_hyps hyps1 hyps2, + tpairs = union_tpairs tpairs1 tpairs2, + prop = Logic.mk_equals (f $ t, g $ u)}) + | _ => raise THM ("combination: premises", 0, [th1, th2]) end; - -(* Equality introduction +(*Equality introduction A ==> B B ==> A ---------------- A == B *) fun equal_intr th1 th2 = - let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, - tpairs=tpairs1, prop=prop1,...} = th1 - and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, - tpairs=tpairs2, prop=prop2,...} = th2; - fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) - in case (prop1,prop2) of - (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => - if A aconv A' andalso B aconv B' - then - (*no fix_shyps*) - Thm{thy_ref = merge_thm_thys(th1,th2), - der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, - maxidx = Int.max(max1,max2), - shyps = Sorts.union_sort(shyps1,shyps2), - hyps = union_term(hyps1,hyps2), - tpairs = tpairs1 @ tpairs2, - prop = Logic.mk_equals(A,B)} - else err"not equal" - | _ => err"premises" + let + val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, + prop = prop1, ...} = th1 + and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, + prop = prop2, ...} = th2; + fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); + in + case (prop1, prop2) of + (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => + if A aconv A' andalso B aconv B' then + Thm {thy_ref = merge_thys2 th1 th2, + der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, + maxidx = Int.max (max1, max2), + shyps = Sorts.union shyps1 shyps2, + hyps = union_hyps hyps1 hyps2, + tpairs = union_tpairs tpairs1 tpairs2, + prop = Logic.mk_equals (A, B)} + else err "not equal" + | _ => err "premises" end; - (*The equal propositions rule A == B A --------- B *) fun equal_elim th1 th2 = - let val Thm{der=der1, maxidx=max1, hyps=hyps1, tpairs=tpairs1, prop=prop1,...} = th1 - and Thm{der=der2, maxidx=max2, hyps=hyps2, tpairs=tpairs2, prop=prop2,...} = th2; - fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) - in case prop1 of - Const("==",_) $ A $ B => - if not (prop2 aconv A) then err"not equal" else - fix_shyps [th1, th2] [] - (Thm{thy_ref= merge_thm_thys(th1,th2), - der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, - maxidx = Int.max(max1,max2), - shyps = [], - hyps = union_term(hyps1,hyps2), - tpairs = tpairs1 @ tpairs2, - prop = B}) + let + val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, + tpairs = tpairs1, prop = prop1, ...} = th1 + and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, + tpairs = tpairs2, prop = prop2, ...} = th2; + fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); + in + case prop1 of + Const ("==", _) $ A $ B => + if prop2 aconv A then + Thm {thy_ref = merge_thys2 th1 th2, + der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, + maxidx = Int.max (max1, max2), + shyps = Sorts.union shyps1 shyps2, + hyps = union_hyps hyps1 hyps2, + tpairs = union_tpairs tpairs1 tpairs2, + prop = B} + else err "not equal" | _ => err"major premise" end; @@ -884,84 +858,71 @@ (**** Derived rules ****) -(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. - Repeated hypotheses are discharged only once; fold cannot do this*) -fun implies_intr_hyps (Thm{thy_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) = - implies_intr_hyps (*no fix_shyps*) - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, - maxidx = maxidx, - shyps = shyps, - hyps = disch(As,A), - tpairs = tpairs, - prop = implies$A$prop}) - | implies_intr_hyps th = th; - -(*Smash" unifies the list of term pairs leaving no flex-flex pairs. +(*Smash unifies the list of term pairs leaving no flex-flex pairs. Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex. *) -fun flexflex_rule (th as Thm{thy_ref, der, maxidx, hyps, tpairs, prop, ...}) = - let fun newthm env = - if Envir.is_empty env then th - else - let val ntpairs = map (pairself (Envir.norm_term env)) tpairs; - val newprop = Envir.norm_term env prop; - (*Remove trivial tpairs, of the form t=t*) - val distpairs = List.filter (not o op aconv) ntpairs - in fix_shyps [th] (env_codT env) - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.norm_proof' env) der, - maxidx = maxidx_of_terms (newprop :: - terms_of_tpairs distpairs), - shyps = [], - hyps = hyps, - tpairs = distpairs, - prop = newprop}) - end; - in Seq.map newthm - (Unify.smash_unifiers(Theory.deref thy_ref, Envir.empty maxidx, tpairs)) - end; +fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = + Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs) + |> Seq.map (fn env => + if Envir.is_empty env then th + else + let + val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) + (*remove trivial tpairs, of the form t==t*) + |> List.filter (not o op aconv); + val prop' = Envir.norm_term env prop; + in + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.norm_proof' env) der, + maxidx = maxidx_of_terms (prop' :: terms_of_tpairs tpairs'), + shyps = insert_env_sorts env shyps, + hyps = hyps, + tpairs = tpairs', + prop = prop'} + end); + (*Instantiation of Vars - A - ------------------- - A[t1/v1,....,tn/vn] + A + --------------------- + A[t1/v1, ...., tn/vn] *) local (*Check that all the terms are Vars and are distinct*) -fun instl_ok ts = forall is_Var ts andalso null(findrep ts); +fun instl_ok ts = forall is_Var ts andalso null (findrep ts); fun pretty_typing thy t T = Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T]; (*For instantiate: process pair of cterms, merge theories*) -fun add_ctpair ((ct,cu), (thy_ref,tpairs)) = +fun add_ctpair ((ct, cu), (thy_ref, tpairs)) = let - val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct - and Cterm {thy_ref=thy_refu, t=u, T= U, ...} = cu; + val Cterm {thy_ref = thy_reft, t = t, T = T, ...} = ct + and Cterm {thy_ref = thy_refu, t = u, T = U, ...} = cu; val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu)); val thy_merged = Theory.deref thy_ref_merged; in - if T=U then (thy_ref_merged, (t,u)::tpairs) - else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", + if T = U then (thy_ref_merged, (t, u) :: tpairs) + else raise TYPE (Pretty.string_of (Pretty.block + [Pretty.str "instantiate: type conflict", Pretty.fbrk, pretty_typing thy_merged t T, Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u]) end; -fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT}, - Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) = +fun add_ctyp + ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT}, + Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) = let val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_refT, thy_refU)); - val thy_merged = Theory.deref thy_ref_merged + val thy_merged = Theory.deref thy_ref_merged; in if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then (thy_ref_merged, (T, U) :: vTs) - else raise TYPE ("Type not of sort " ^ - Sign.string_of_sort thy_merged S, [U], []) + else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy_merged S, [U], []) end | add_ctyp ((Ctyp {T, thy_ref}, _), _) = raise TYPE (Pretty.string_of (Pretty.block @@ -970,105 +931,103 @@ in -(*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. +(*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. - No longer normalizes the new theorem! *) + Does NOT normalize the resulting theorem!*) fun instantiate ([], []) th = th - | instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = - let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs; - val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs; - fun subst t = - subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); - val newprop = subst prop; - val newdpairs = map (pairself subst) dpairs; - val newth = - (Thm{thy_ref = newthy_ref, - der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, - maxidx = maxidx_of_terms (newprop :: - terms_of_tpairs newdpairs), - shyps = add_insts_sorts ((vTs, tpairs), shyps), - hyps = hyps, - tpairs = newdpairs, - prop = newprop}) - in if not(instl_ok(map #1 tpairs)) - then raise THM("instantiate: variables not distinct", 0, [th]) - else if not(null(findrep(map #1 vTs))) - then raise THM("instantiate: type variables not distinct", 0, [th]) - else newth + | instantiate (vcTs, ctpairs) th = + let + val Thm {thy_ref, der, maxidx, hyps, shyps, tpairs = dpairs, prop} = th; + val (newthy_ref, tpairs) = foldr add_ctpair (thy_ref, []) ctpairs; + val (newthy_ref, vTs) = foldr add_ctyp (newthy_ref, []) vcTs; + fun subst t = subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); + val newprop = subst prop; + val newdpairs = map (pairself subst) dpairs; + val newth = + Thm {thy_ref = newthy_ref, + der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, + maxidx = maxidx_of_terms (newprop :: terms_of_tpairs newdpairs), + shyps = shyps + |> fold (Sorts.insert_typ o #2) vTs + |> fold (Sorts.insert_term o #2) tpairs, + hyps = hyps, + tpairs = newdpairs, + prop = newprop}; + in + if not (instl_ok (map #1 tpairs)) then + raise THM ("instantiate: variables not distinct", 0, [th]) + else if not (null (findrep (map #1 vTs))) then + raise THM ("instantiate: type variables not distinct", 0, [th]) + else newth end - handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th]) - | TYPE (msg, _, _) => raise THM (msg, 0, [th]); + handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); end; -(*The trivial implication A==>A, justified by assume and forall rules. - A can contain Vars, not so for assume! *) -fun trivial ct : thm = - let val Cterm {thy_ref, t=A, T, maxidx} = ct - in if T<>propT then - raise THM("trivial: the term must have type prop", 0, []) - else fix_shyps [] [] - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), - maxidx = maxidx, - shyps = [], - hyps = [], - tpairs = [], - prop = implies$A$A}) - end; +(*The trivial implication A ==> A, justified by assume and forall rules. + A can contain Vars, not so for assume!*) +fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) = + if T <> propT then + raise THM ("trivial: the term must have type prop", 0, []) + else + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = implies $ A $ A}; (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) fun class_triv thy c = - let val Cterm {thy_ref, t, maxidx, ...} = + let val Cterm {thy_ref, t, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); in - fix_shyps [] [] - (Thm {thy_ref = thy_ref, - der = Pt.infer_derivs' I - (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), - maxidx = maxidx, - shyps = [], - hyps = [], - tpairs = [], - prop = t}) + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = t} end; (* Replace all TFrees not fixed or in the hyps by new TVars *) -fun varifyT' fixed (Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = +fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = let val tfrees = foldr add_term_tfrees fixed hyps; val prop1 = attach_tpairs tpairs prop; val (prop2, al) = Type.varify (prop1, tfrees); - val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) - in (*no fix_shyps*) - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, - maxidx = Int.max(0,maxidx), - shyps = shyps, - hyps = hyps, - tpairs = rev (map Logic.dest_equals ts), - prop = prop3}, al) + val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); + in + (Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, + maxidx = Int.max (0, maxidx), + shyps = shyps, + hyps = hyps, + tpairs = rev (map Logic.dest_equals ts), + prop = prop3}, al) end; val varifyT = #1 o varifyT' []; (* Replace all TVars by new TFrees *) -fun freezeT(Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = +fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.freeze prop1; - val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) - in (*no fix_shyps*) - Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.freezeT prop1) der, - maxidx = maxidx_of_term prop2, - shyps = shyps, - hyps = hyps, - tpairs = rev (map Logic.dest_equals ts), - prop = prop3} + val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); + in + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.freezeT prop1) der, + maxidx = maxidx_of_term prop2, + shyps = shyps, + hyps = hyps, + tpairs = rev (map Logic.dest_equals ts), + prop = prop3} end; @@ -1084,105 +1043,108 @@ (*Increment variables and parameters of orule as required for resolution with goal i of state. *) fun lift_rule (state, i) orule = - let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state - val (Bi::_, _) = Logic.strip_prems(i, [], sprop) - handle TERM _ => raise THM("lift_rule", i, [orule,state]) - val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi} - val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) - val (Thm{thy_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule - val (As, B) = Logic.strip_horn prop - in (*no fix_shyps*) - Thm{thy_ref = merge_thm_thys(state,orule), - der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, - maxidx = maxidx+smax+1, - shyps = Sorts.union_sort(sshyps,shyps), - hyps = hyps, - tpairs = map (pairself lift_abs) tpairs, - prop = Logic.list_implies (map lift_all As, lift_all B)} + let + val Thm {shyps = sshyps, prop = sprop, maxidx = smax, thy_ref = sthy_ref,...} = state; + val (Bi :: _, _) = Logic.strip_prems (i, [], sprop) + handle TERM _ => raise THM ("lift_rule", i, [orule, state]); + val (lift_abs, lift_all) = Logic.lift_fns (Bi, smax + 1); + val (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = orule; + val (As, B) = Logic.strip_horn prop; + in + Thm {thy_ref = merge_thys2 state orule, + der = Pt.infer_derivs' (Pt.lift_proof Bi (smax + 1) prop) der, + maxidx = maxidx + smax + 1, + shyps = Sorts.union sshyps shyps, + hyps = hyps, + tpairs = map (pairself lift_abs) tpairs, + prop = Logic.list_implies (map lift_all As, lift_all B)} end; fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = - if i < 0 then raise THM ("negative increment", 0, [thm]) else - if i = 0 then thm else + if i < 0 then raise THM ("negative increment", 0, [thm]) + else if i = 0 then thm + else Thm {thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.map_proof_terms - (Logic.incr_indexes ([], i)) (incr_tvar i)) der, - maxidx = maxidx + i, - shyps = shyps, - hyps = hyps, - tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, - prop = Logic.incr_indexes ([], i) prop}; + der = Pt.infer_derivs' (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i)) der, + maxidx = maxidx + i, + shyps = shyps, + hyps = hyps, + tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, + prop = Logic.incr_indexes ([], i) prop}; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption i state = - let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; - val (tpairs, Bs, Bi, C) = dest_state(state,i) - fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = - fix_shyps [state] (env_codT env) - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' - ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o - Pt.assumption_proof Bs Bi n) der, - maxidx = maxidx, - shyps = [], - hyps = hyps, - tpairs = if Envir.is_empty env then tpairs else - map (pairself (Envir.norm_term env)) tpairs, - prop = - if Envir.is_empty env then (*avoid wasted normalizations*) - Logic.list_implies (Bs, C) - else (*normalize the new rule fully*) - Envir.norm_term env (Logic.list_implies (Bs, C))}); - fun addprfs [] _ = Seq.empty - | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull - (Seq.mapp (newth n) - (Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs)) - (addprfs apairs (n+1)))) - in addprfs (Logic.assum_pairs (~1,Bi)) 1 end; + let + val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; + val (tpairs, Bs, Bi, C) = dest_state (state, i); + fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' + ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o + Pt.assumption_proof Bs Bi n) der, + maxidx = maxidx, + shyps = insert_env_sorts env shyps, + hyps = hyps, + tpairs = + if Envir.is_empty env then tpairs + else map (pairself (Envir.norm_term env)) tpairs, + prop = + if Envir.is_empty env then (*avoid wasted normalizations*) + Logic.list_implies (Bs, C) + else (*normalize the new rule fully*) + Envir.norm_term env (Logic.list_implies (Bs, C))}; + fun addprfs [] _ = Seq.empty + | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull + (Seq.mapp (newth n) + (Unify.unifiers (Theory.deref thy_ref, Envir.empty maxidx, (t, u) :: tpairs)) + (addprfs apairs (n + 1)))) + in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) fun eq_assumption i state = - let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; - val (tpairs, Bs, Bi, C) = dest_state(state,i) - in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of - (~1) => raise THM("eq_assumption", 0, [state]) - | n => fix_shyps [state] [] - (Thm{thy_ref = thy_ref, - der = Pt.infer_derivs' - (Pt.assumption_proof Bs Bi (n+1)) der, - maxidx = maxidx, - shyps = [], - hyps = hyps, - tpairs = tpairs, - prop = Logic.list_implies (Bs, C)})) + let + val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; + val (tpairs, Bs, Bi, C) = dest_state (state, i); + in + (case find_index (op aconv) (Logic.assum_pairs (~1, Bi)) of + ~1 => raise THM ("eq_assumption", 0, [state]) + | n => + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der, + maxidx = maxidx, + shyps = shyps, + hyps = hyps, + tpairs = tpairs, + prop = Logic.list_implies (Bs, C)}) end; (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = - let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state; - val (tpairs, Bs, Bi, C) = dest_state(state,i) - val params = Term.strip_all_vars Bi - and rest = Term.strip_all_body Bi - val asms = Logic.strip_imp_prems rest - and concl = Logic.strip_imp_concl rest - val n = length asms - val m = if k<0 then n+k else k - val Bi' = if 0=m orelse m=n then Bi - else if 0 raise THM("permute_prems:j", j, [rl]) - val n_j = length moved_prems - val m = if k<0 then n_j + k else k - val prop' = if 0 = m orelse m = n_j then prop - else if 0 raise THM ("permute_prems: j", j, [rl]); + val n_j = length moved_prems; + val m = if k < 0 then n_j + k else k; + val prop' = + if 0 = m orelse m = n_j then prop + else if 0 < m andalso m < n_j then + let val (ps, qs) = splitAt (m, moved_prems) + in Logic.list_implies (fixed_prems @ qs @ ps, concl) end + else raise THM ("permute_prems:k", k, [rl]); + in + Thm {thy_ref = thy_ref, + der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, + maxidx = maxidx, + shyps = shyps, + hyps = hyps, + tpairs = tpairs, + prop = prop'} end; @@ -1221,35 +1185,36 @@ The names in cs, if distinct, are used for the innermost parameters; preceding parameters may be renamed to make all params distinct.*) fun rename_params_rule (cs, i) state = - let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state - val (tpairs, Bs, Bi, C) = dest_state(state,i) - val iparams = map #1 (Logic.strip_params Bi) - val short = length iparams - length cs - val newnames = - if short<0 then error"More names than abstractions!" - else variantlist(Library.take (short,iparams), cs) @ cs - val freenames = map (#1 o dest_Free) (term_frees Bi) - val newBi = Logic.list_rename_params (newnames, Bi) + let + val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state; + val (tpairs, Bs, Bi, C) = dest_state (state, i); + val iparams = map #1 (Logic.strip_params Bi); + val short = length iparams - length cs; + val newnames = + if short < 0 then error "More names than abstractions!" + else variantlist (Library.take (short, iparams), cs) @ cs; + val freenames = map (#1 o dest_Free) (term_frees Bi); + val newBi = Logic.list_rename_params (newnames, Bi); in - case findrep cs of - c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); - state) - | [] => (case cs inter_string freenames of - a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); - state) - | [] => Thm{thy_ref = thy_ref, - der = der, - maxidx = maxidx, - shyps = shyps, - hyps = hyps, - tpairs = tpairs, - prop = Logic.list_implies (Bs @ [newBi], C)}) + case findrep cs of + c :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ c); state) + | [] => + (case cs inter_string freenames of + a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) + | [] => + Thm {thy_ref = thy_ref, + der = der, + maxidx = maxidx, + shyps = shyps, + hyps = hyps, + tpairs = tpairs, + prop = Logic.list_implies (Bs @ [newBi], C)}) end; (*** Preservation of bound variable names ***) -fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = +fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = (case Term.rename_abs pat obj prop of NONE => thm | SOME prop' => Thm @@ -1344,7 +1309,7 @@ (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems(strip_all_body Bi, if eres_flg then ~1 else 0) - val thy_ref = merge_thm_thys(state,orule); + val thy_ref = merge_thys2 state orule; val thy = Theory.deref thy_ref; (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = @@ -1363,7 +1328,7 @@ else (*normalize the new rule fully*) (ntps, (map normt (Bs @ As), normt C)) end - val th = (*tuned fix_shyps*) + val th = Thm{thy_ref = thy_ref, der = Pt.infer_derivs ((if Envir.is_empty env then I @@ -1373,8 +1338,8 @@ curry op oo (Pt.norm_proof' env)) (Pt.bicompose_proof Bs oldAs As A n)) rder' sder, maxidx = maxidx, - shyps = add_env_sorts (env, Sorts.union_sort(rshyps,sshyps)), - hyps = union_term(rhyps,shyps), + shyps = insert_env_sorts env (Sorts.union rshyps sshyps), + hyps = union_hyps rhyps shyps, tpairs = ntpairs, prop = Logic.list_implies normp} in Seq.cons(th, thq) end handle COMPOSE => thq; @@ -1464,14 +1429,14 @@ in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) - else fix_shyps [] [] - (Thm {thy_ref = Theory.self_ref thy', + else + Thm {thy_ref = Theory.self_ref thy', der = (true, Pt.oracle_proof name prop), maxidx = maxidx, - shyps = [], + shyps = Sorts.insert_term prop [], hyps = [], tpairs = [], - prop = prop}) + prop = prop} end end;