1 (* ========================================================================= *)
2 (* Abstract type of theorems and primitive inference rules. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
10 (* ------------------------------------------------------------------------- *)
11 (* A few bits of general derived syntax. *)
12 (* ------------------------------------------------------------------------- *)
17 | _ -> failwith "rator: Not a combination";;
22 | _ -> failwith "rand: Not a combination";;
24 (* ------------------------------------------------------------------------- *)
25 (* Syntax operations for equations. *)
26 (* ------------------------------------------------------------------------- *)
29 let eq = mk_const("=",[]) in
31 try let ty = type_of l in
32 let eq_tm = inst [ty,aty] eq in
33 mk_comb(mk_comb(eq_tm,l),r)
34 with Failure _ -> failwith "mk_eq";;
38 Comb(Comb(Const("=",_),l),r) -> l,r
39 | _ -> failwith "dest_eq";;
43 Comb(Comb(Const("=",_),_),_) -> true
46 (* ------------------------------------------------------------------------- *)
47 (* Useful to have term union modulo alpha-conversion for assumption lists. *)
48 (* ------------------------------------------------------------------------- *)
50 let term_remove t l = filter (fun t' -> not(aconv t t')) l;;
52 let rec term_union l1 l2 =
55 | (h::t) -> let subun = term_union t l2 in
56 if exists (aconv h) subun then subun else h::subun;;
58 (* ------------------------------------------------------------------------- *)
59 (* The abstract type of theorems. *)
60 (* ------------------------------------------------------------------------- *)
62 module type Hol_thm_primitives =
64 val dest_thm : thm -> term list * term
65 val hyp : thm -> term list
66 val concl : thm -> term
67 val REFL : term -> thm
68 val TRANS : thm -> thm -> thm
69 val MK_COMB : thm * thm -> thm
70 val ABS : term -> thm -> thm
71 val BETA : term -> thm
72 val ASSUME : term -> thm
73 val EQ_MP : thm -> thm -> thm
74 val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
75 val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
76 val INST : (term * term) list -> thm -> thm
77 val axioms : unit -> thm list
78 val new_axiom : term -> thm
79 val new_basic_definition : term -> thm
80 val new_basic_type_definition : string -> string * string -> thm -> thm * thm
83 (* ------------------------------------------------------------------------- *)
84 (* This is the implementation of those primitives. *)
85 (* ------------------------------------------------------------------------- *)
87 module Hol : Hol_thm_primitives = struct
89 type thm = Sequent of (term list * term)
91 (* ------------------------------------------------------------------------- *)
92 (* Basic theorem destructors. *)
93 (* ------------------------------------------------------------------------- *)
95 let dest_thm (Sequent(asl,c)) = (asl,c)
97 let hyp (Sequent(asl,c)) = asl
99 let concl (Sequent(asl,c)) = c
101 (* ------------------------------------------------------------------------- *)
102 (* Basic equality properties; TRANS is derivable but included for efficiency *)
103 (* ------------------------------------------------------------------------- *)
106 Sequent([],mk_eq(tm,tm))
108 let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
110 Comb(Comb(Const("=",_),l),m1),Comb(Comb(Const("=",_),m2),r)
111 when aconv m1 m2 -> Sequent(term_union asl1 asl2,mk_eq(l,r))
112 | _ -> failwith "TRANS"
114 (* ------------------------------------------------------------------------- *)
115 (* Congruence properties of equality. *)
116 (* ------------------------------------------------------------------------- *)
118 let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
120 Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2)
121 -> Sequent(term_union asl1 asl2,mk_eq(mk_comb(l1,l2),mk_comb(r1,r2)))
122 | _ -> failwith "MK_COMB"
124 let ABS v (Sequent(asl,c)) =
126 Comb(Comb(Const("=",_),l),r) ->
127 if exists (vfree_in v) asl
128 then failwith "ABS: variable is free in assumptions"
129 else Sequent(asl,mk_eq(mk_abs(v,l),mk_abs(v,r)))
130 | _ -> failwith "ABS: not an equation"
132 (* ------------------------------------------------------------------------- *)
133 (* Trivial case of lambda calculus beta-conversion. *)
134 (* ------------------------------------------------------------------------- *)
138 Comb(Abs(v,bod),arg) when arg = v -> Sequent([],mk_eq(tm,bod))
139 | _ -> failwith "BETA: not a trivial beta-redex"
141 (* ------------------------------------------------------------------------- *)
142 (* Rules connected with deduction. *)
143 (* ------------------------------------------------------------------------- *)
146 if type_of tm = bool_ty then Sequent([tm],tm)
147 else failwith "ASSUME: not a proposition"
149 let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
151 Comb(Comb(Const("=",_),l),r) when aconv l c
152 -> Sequent(term_union asl1 asl2,r)
153 | _ -> failwith "EQ_MP"
155 let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
156 let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
157 Sequent(term_union asl1' asl2',mk_eq(c1,c2))
159 (* ------------------------------------------------------------------------- *)
160 (* Type and term instantiation. *)
161 (* ------------------------------------------------------------------------- *)
163 let INST_TYPE theta (Sequent(asl,c)) =
164 let inst_fn = inst theta in
165 Sequent(map inst_fn asl,inst_fn c)
167 let INST theta (Sequent(asl,c)) =
168 let inst_fun = vsubst theta in
169 Sequent(map inst_fun asl,inst_fun c)
171 (* ------------------------------------------------------------------------- *)
172 (* Handling of axioms. *)
173 (* ------------------------------------------------------------------------- *)
175 let the_axioms = ref ([]:thm list)
177 let axioms() = !the_axioms
180 if fst(dest_type(type_of tm)) = "bool" then
181 let th = Sequent([],tm) in
182 (the_axioms := th::(!the_axioms); th)
183 else failwith "new_axiom: Not a proposition"
185 (* ------------------------------------------------------------------------- *)
186 (* Handling of (term) definitions. *)
187 (* ------------------------------------------------------------------------- *)
189 let new_basic_definition tm =
190 let l,r = dest_eq tm in
191 let cname,ty = dest_var l in
192 if not(freesin [] r) then failwith "new_definition: term not closed" else
193 if not (subset (type_vars_in_term r) (tyvars ty))
194 then failwith "new_definition: Type variables not reflected in constant"
196 let c = new_constant(cname,ty); mk_const(cname,[]) in
197 Sequent([],mk_eq(c,r))
199 (* ------------------------------------------------------------------------- *)
200 (* Handling of type definitions. *)
202 (* This function now involves no logical constants beyond equality. *)
205 (* --------------------------- *)
206 (* |- abs(rep a) = a *)
207 (* |- P r = (rep(abs r) = r) *)
209 (* Where "abs" and "rep" are new constants with the nominated names. *)
210 (* ------------------------------------------------------------------------- *)
212 let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
213 if exists (can get_const_type) [absname; repname] then
214 failwith "new_basic_type_definition: Constant(s) already in use" else
215 if not (asl = []) then
216 failwith "new_basic_type_definition: Assumptions in theorem" else
217 let P,x = try dest_comb c
219 failwith "new_basic_type_definition: Not a combination" in
220 if not(freesin [] P) then
221 failwith "new_basic_type_definition: Predicate is not closed" else
222 let tyvars = sort (<=) (type_vars_in_term P) in
223 let _ = try new_type(tyname,length tyvars)
225 failwith "new_basic_type_definition: Type already defined" in
226 let aty = mk_type(tyname,tyvars)
227 and rty = type_of x in
228 let abs = new_constant(absname,mk_fun_ty rty aty); mk_const(absname,[])
229 and rep = new_constant(repname,mk_fun_ty aty rty); mk_const(repname,[]) in
230 let a = mk_var("a",aty) and r = mk_var("r",rty) in
231 Sequent([],mk_eq(mk_comb(abs,mk_comb(rep,a)),a)),
232 Sequent([],mk_eq(mk_comb(P,r),mk_eq(mk_comb(rep,mk_comb(abs,r)),r)))
238 (* ------------------------------------------------------------------------- *)
239 (* Comparison function on theorems. Currently the same as equality, but *)
240 (* it's useful to separate because in the proof-recording version it isn't. *)
241 (* ------------------------------------------------------------------------- *)
243 let equals_thm th th' = dest_thm th = dest_thm th';;