3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 The abstract types "theory" and "thm". |
6 The abstract types "theory" and "thm". |
7 Also "cterm" / "ctyp" (certified terms / typs under a signature). |
7 Also "cterm" / "ctyp" (certified terms / typs under a signature). |
8 |
|
9 *) |
8 *) |
10 |
9 |
11 signature THM = |
10 signature THM = |
12 sig |
11 sig |
13 structure Envir : ENVIR |
12 structure Envir : ENVIR |
101 val trivial: cterm -> thm |
100 val trivial: cterm -> thm |
102 val varifyT: thm -> thm |
101 val varifyT: thm -> thm |
103 end; |
102 end; |
104 |
103 |
105 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN |
104 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN |
106 and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)(*: THM *) (* FIXME debug *) = |
105 and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) : THM = |
107 struct |
106 struct |
108 |
107 |
109 structure Sequence = Unify.Sequence; |
108 structure Sequence = Unify.Sequence; |
110 structure Envir = Unify.Envir; |
109 structure Envir = Unify.Envir; |
111 structure Sign = Unify.Sign; |
110 structure Sign = Unify.Sign; |
597 (B::rBs, C) => (tpairs, rev rBs, B, C) |
596 (B::rBs, C) => (tpairs, rev rBs, B, C) |
598 | _ => raise THM("dest_state", i, [state]) |
597 | _ => raise THM("dest_state", i, [state]) |
599 end |
598 end |
600 handle TERM _ => raise THM("dest_state", i, [state]); |
599 handle TERM _ => raise THM("dest_state", i, [state]); |
601 |
600 |
602 (*Increment variables and parameters of rule as required for |
601 (*Increment variables and parameters of orule as required for |
603 resolution with goal i of state. *) |
602 resolution with goal i of state. *) |
604 fun lift_rule (state, i) orule = |
603 fun lift_rule (state, i) orule = |
605 let val Thm{prop=sprop,maxidx=smax,...} = state; |
604 let val Thm{prop=sprop,maxidx=smax,...} = state; |
606 val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) |
605 val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) |
607 handle TERM _ => raise THM("lift_rule", i, [orule,state]); |
606 handle TERM _ => raise THM("lift_rule", i, [orule,state]); |