6 Emulation of HOL inference rules for TFL |
6 Emulation of HOL inference rules for TFL |
7 *) |
7 *) |
8 |
8 |
9 signature RULES = |
9 signature RULES = |
10 sig |
10 sig |
11 val dest_thm : thm -> term list * term |
11 val dest_thm: thm -> term list * term |
12 |
12 |
13 (* Inference rules *) |
13 (* Inference rules *) |
14 val REFL :cterm -> thm |
14 val REFL: cterm -> thm |
15 val ASSUME :cterm -> thm |
15 val ASSUME: cterm -> thm |
16 val MP :thm -> thm -> thm |
16 val MP: thm -> thm -> thm |
17 val MATCH_MP :thm -> thm -> thm |
17 val MATCH_MP: thm -> thm -> thm |
18 val CONJUNCT1 :thm -> thm |
18 val CONJUNCT1: thm -> thm |
19 val CONJUNCT2 :thm -> thm |
19 val CONJUNCT2: thm -> thm |
20 val CONJUNCTS :thm -> thm list |
20 val CONJUNCTS: thm -> thm list |
21 val DISCH :cterm -> thm -> thm |
21 val DISCH: cterm -> thm -> thm |
22 val UNDISCH :thm -> thm |
22 val UNDISCH: thm -> thm |
23 val SPEC :cterm -> thm -> thm |
23 val SPEC: cterm -> thm -> thm |
24 val ISPEC :cterm -> thm -> thm |
24 val ISPEC: cterm -> thm -> thm |
25 val ISPECL :cterm list -> thm -> thm |
25 val ISPECL: cterm list -> thm -> thm |
26 val GEN :cterm -> thm -> thm |
26 val GEN: cterm -> thm -> thm |
27 val GENL :cterm list -> thm -> thm |
27 val GENL: cterm list -> thm -> thm |
28 val LIST_CONJ :thm list -> thm |
28 val LIST_CONJ: thm list -> thm |
29 |
29 |
30 val SYM : thm -> thm |
30 val SYM: thm -> thm |
31 val DISCH_ALL : thm -> thm |
31 val DISCH_ALL: thm -> thm |
32 val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm |
32 val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm |
33 val SPEC_ALL : thm -> thm |
33 val SPEC_ALL: thm -> thm |
34 val GEN_ALL : thm -> thm |
34 val GEN_ALL: thm -> thm |
35 val IMP_TRANS : thm -> thm -> thm |
35 val IMP_TRANS: thm -> thm -> thm |
36 val PROVE_HYP : thm -> thm -> thm |
36 val PROVE_HYP: thm -> thm -> thm |
37 |
37 |
38 val CHOOSE : cterm * thm -> thm -> thm |
38 val CHOOSE: cterm * thm -> thm -> thm |
39 val EXISTS : cterm * cterm -> thm -> thm |
39 val EXISTS: cterm * cterm -> thm -> thm |
40 val EXISTL : cterm list -> thm -> thm |
40 val EXISTL: cterm list -> thm -> thm |
41 val IT_EXISTS : (cterm*cterm) list -> thm -> thm |
41 val IT_EXISTS: (cterm*cterm) list -> thm -> thm |
42 |
42 |
43 val EVEN_ORS : thm list -> thm list |
43 val EVEN_ORS: thm list -> thm list |
44 val DISJ_CASESL : thm -> thm list -> thm |
44 val DISJ_CASESL: thm -> thm list -> thm |
45 |
45 |
46 val list_beta_conv : cterm -> cterm list -> thm |
46 val list_beta_conv: cterm -> cterm list -> thm |
47 val SUBS : thm list -> thm -> thm |
47 val SUBS: thm list -> thm -> thm |
48 val simpl_conv : simpset -> thm list -> cterm -> thm |
48 val simpl_conv: simpset -> thm list -> cterm -> thm |
49 |
49 |
50 val rbeta : thm -> thm |
50 val rbeta: thm -> thm |
51 (* For debugging my isabelle solver in the conditional rewriter *) |
51 (* For debugging my isabelle solver in the conditional rewriter *) |
52 val term_ref : term list ref |
52 val term_ref: term list ref |
53 val thm_ref : thm list ref |
53 val thm_ref: thm list ref |
54 val ss_ref : simpset list ref |
54 val ss_ref: simpset list ref |
55 val tracing : bool ref |
55 val tracing: bool ref |
56 val CONTEXT_REWRITE_RULE : term * term list * thm * thm list |
56 val CONTEXT_REWRITE_RULE: term * term list * thm * thm list |
57 -> thm -> thm * term list |
57 -> thm -> thm * term list |
58 val RIGHT_ASSOC : thm -> thm |
58 val RIGHT_ASSOC: thm -> thm |
59 |
59 |
60 val prove : bool -> cterm * tactic -> thm |
60 val prove: bool -> cterm * tactic -> thm |
61 end; |
61 end; |
62 |
62 |
63 structure Rules: RULES = |
63 structure Rules: RULES = |
64 struct |
64 struct |
65 |
65 |
306 in |
306 in |
307 fun GEN v th = |
307 fun GEN v th = |
308 let val gth = forall_intr v th |
308 let val gth = forall_intr v th |
309 val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth |
309 val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth |
310 val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) |
310 val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) |
311 val theta = Pattern.match sign (P,P') |
311 val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty); |
312 val allI2 = instantiate (certify sign theta) allI |
312 val allI2 = instantiate (certify sign theta) allI |
313 val thm = Thm.implies_elim allI2 gth |
313 val thm = Thm.implies_elim allI2 gth |
314 val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm |
314 val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm |
315 val prop' = tp $ (A $ Abs(x,ty,M)) |
315 val prop' = tp $ (A $ Abs(x,ty,M)) |
316 in ALPHA thm (cterm_of sign prop') |
316 in ALPHA thm (cterm_of sign prop') |
351 fun CHOOSE (fvar, exth) fact = |
351 fun CHOOSE (fvar, exth) fact = |
352 let |
352 let |
353 val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) |
353 val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) |
354 val redex = D.capply lam fvar |
354 val redex = D.capply lam fvar |
355 val {sign, t = t$u,...} = Thm.rep_cterm redex |
355 val {sign, t = t$u,...} = Thm.rep_cterm redex |
356 val residue = Thm.cterm_of sign (betapply (t, u)) |
356 val residue = Thm.cterm_of sign (Term.betapply (t, u)) |
357 in |
357 in |
358 GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) |
358 GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) |
359 handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg |
359 handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg |
360 end; |
360 end; |
361 |
361 |