--- 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<m andalso m<n
- then let val (ps,qs) = splitAt(m,asms)
- in list_all(params, Logic.list_implies(qs @ ps, concl))
- end
- else raise THM("rotate_rule", k, [state])
- in (*no fix_shyps*)
- Thm{thy_ref = thy_ref,
- der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
- maxidx = maxidx,
- shyps = shyps,
- hyps = hyps,
- tpairs = tpairs,
- prop = Logic.list_implies (Bs @ [Bi'], C)}
+ let
+ val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = 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 < m andalso m < n then
+ let val (ps, qs) = splitAt (m, asms)
+ in list_all (params, Logic.list_implies (qs @ ps, concl)) end
+ else raise THM ("rotate_rule", k, [state]);
+ in
+ Thm {thy_ref = thy_ref,
+ der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = hyps,
+ tpairs = tpairs,
+ prop = Logic.list_implies (Bs @ [Bi'], C)}
end;
@@ -1190,27 +1152,29 @@
unchanged. Does nothing if k=0 or if k equals n-j, where n is the
number of premises. Useful with etac and underlies tactic/defer_tac*)
fun permute_prems j k rl =
- let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
- val prems = Logic.strip_imp_prems prop
- and concl = Logic.strip_imp_concl prop
- val moved_prems = List.drop(prems, j)
- and fixed_prems = List.take(prems, j)
- handle Subscript => 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 (*no fix_shyps*)
- 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'}
+ let
+ val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl;
+ val prems = Logic.strip_imp_prems prop
+ and concl = Logic.strip_imp_concl prop;
+ val moved_prems = List.drop (prems, j)
+ and fixed_prems = List.take (prems, j)
+ handle Subscript => 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;