25 |
25 |
26 infix 0 MRSL |
26 infix 0 MRSL |
27 |
27 |
28 (* Reflexivity prover *) |
28 (* Reflexivity prover *) |
29 |
29 |
30 fun refl_tac ctxt = |
30 fun mono_eq_prover ctxt prop = |
31 let |
31 let |
32 fun intro_reflp_tac (ct, i) = |
|
33 let |
|
34 val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm ge_eq_refl} |
|
35 val concl_pat = Drule.strip_imp_concl (cprop_of rule) |
|
36 val insts = Thm.first_order_match (concl_pat, ct) |
|
37 in |
|
38 rtac (Drule.instantiate_normalize insts rule) i |
|
39 end |
|
40 handle Pattern.MATCH => no_tac |
|
41 |
|
42 val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt)) |
32 val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt)) |
43 in |
33 in |
44 EVERY' [CSUBGOAL intro_reflp_tac, |
34 SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1))) |
45 REPEAT_ALL_NEW (resolve_tac rules)] |
35 handle ERROR _ => NONE |
46 end |
36 end |
47 |
37 |
48 fun try_prove_reflexivity ctxt prop = |
38 fun try_prove_reflexivity ctxt prop = |
49 SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1)) |
39 let |
50 handle ERROR _ => NONE |
40 val thy = Proof_Context.theory_of ctxt |
|
41 val cprop = cterm_of thy prop |
|
42 val rule = @{thm ge_eq_refl} |
|
43 val concl_pat = Drule.strip_imp_concl (cprop_of rule) |
|
44 val insts = Thm.first_order_match (concl_pat, cprop) |
|
45 val rule = Drule.instantiate_normalize insts rule |
|
46 val prop = hd (prems_of rule) |
|
47 in |
|
48 case mono_eq_prover ctxt prop of |
|
49 SOME thm => SOME (rule OF [thm]) |
|
50 | NONE => NONE |
|
51 end |
51 |
52 |
52 (* |
53 (* |
53 Generates a parametrized transfer rule. |
54 Generates a parametrized transfer rule. |
54 transfer_rule - of the form T t f |
55 transfer_rule - of the form T t f |
55 parametric_transfer_rule - of the form par_R t' t |
56 parametric_transfer_rule - of the form par_R t' t |