equal
deleted
inserted
replaced
41 |
41 |
42 fun exhaust_inst_as_projs ctxt frees thm = |
42 fun exhaust_inst_as_projs ctxt frees thm = |
43 let |
43 let |
44 val num_frees = length frees; |
44 val num_frees = length frees; |
45 val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd); |
45 val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd); |
46 fun find s = find_index (curry (op =) s) frees; |
46 fun find x = find_index (curry (op =) x) frees; |
47 fun mk_cfp (f as ((s, _), T)) = |
47 fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x))); |
48 (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s))); |
48 in infer_instantiate ctxt (map mk_inst fs) thm end; |
49 val cfps = map mk_cfp fs; |
|
50 in |
|
51 Drule.cterm_instantiate cfps thm |
|
52 end; |
|
53 |
49 |
54 val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs; |
50 val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs; |
55 |
51 |
56 fun distinct_in_prems_tac ctxt distincts = |
52 fun distinct_in_prems_tac ctxt distincts = |
57 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' |
53 eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' |