85 (** First-order Resolution **) |
85 (** First-order Resolution **) |
86 |
86 |
87 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty); |
87 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty); |
88 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); |
88 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); |
89 |
89 |
90 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 |
|
91 |
|
92 (*FIXME: currently does not "rename variables apart"*) |
90 (*FIXME: currently does not "rename variables apart"*) |
93 fun first_order_resolve thA thB = |
91 fun first_order_resolve thA thB = |
94 let val thy = theory_of_thm thA |
92 let val thy = theory_of_thm thA |
95 val tmA = concl_of thA |
93 val tmA = concl_of thA |
96 val Const("==>",_) $ tmB $ _ = prop_of thB |
94 val Const("==>",_) $ tmB $ _ = prop_of thB |
97 val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0) |
95 val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) |
98 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) |
96 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) |
99 in thA RS (cterm_instantiate ct_pairs thB) end |
97 in thA RS (cterm_instantiate ct_pairs thB) end |
100 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) |
98 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) |
101 |
99 |
102 fun flexflex_first_order th = |
100 fun flexflex_first_order th = |
103 case (tpairs_of th) of |
101 case (tpairs_of th) of |
104 [] => th |
102 [] => th |
105 | pairs => |
103 | pairs => |
106 let val thy = theory_of_thm th |
104 let val thy = theory_of_thm th |
107 val (tyenv,tenv) = |
105 val (tyenv, tenv) = |
108 List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs |
106 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
109 val t_pairs = map term_pair_of (Vartab.dest tenv) |
107 val t_pairs = map term_pair_of (Vartab.dest tenv) |
110 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th |
108 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th |
111 in th' end |
109 in th' end |
112 handle THM _ => th; |
110 handle THM _ => th; |
113 |
111 |