149 elhs: cterm, (*the eta-contracted lhs*) |
149 elhs: cterm, (*the eta-contracted lhs*) |
150 extra: bool, (*extra variables outside of elhs*) |
150 extra: bool, (*extra variables outside of elhs*) |
151 fo: bool, (*use first-order matching*) |
151 fo: bool, (*use first-order matching*) |
152 perm: bool}; (*the rewrite rule is permutative*) |
152 perm: bool}; (*the rewrite rule is permutative*) |
153 |
153 |
|
154 fun trim_context_rrule ({thm, name, lhs, elhs, extra, fo, perm}: rrule) = |
|
155 {thm = Thm.trim_context thm, name = name, lhs = lhs, elhs = Thm.trim_context_cterm elhs, |
|
156 extra = extra, fo = fo, perm = perm}; |
|
157 |
154 (* |
158 (* |
155 Remarks: |
159 Remarks: |
156 - elhs is used for matching, |
160 - elhs is used for matching, |
157 lhs only for preservation of bound variable names; |
161 lhs only for preservation of bound variable names; |
158 - fo is set iff |
162 - fo is set iff |
468 fun insert_rrule (rrule as {thm, name, ...}) ctxt = |
472 fun insert_rrule (rrule as {thm, name, ...}) ctxt = |
469 (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm)); |
473 (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm)); |
470 ctxt |> map_simpset1 (fn (rules, prems, depth) => |
474 ctxt |> map_simpset1 (fn (rules, prems, depth) => |
471 let |
475 let |
472 val rrule2 as {elhs, ...} = mk_rrule2 rrule; |
476 val rrule2 as {elhs, ...} = mk_rrule2 rrule; |
473 val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, rrule2) rules; |
477 val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules; |
474 in (rules', prems, depth) end) |
478 in (rules', prems, depth) end) |
475 handle Net.INSERT => |
479 handle Net.INSERT => |
476 (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); |
480 (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); |
477 ctxt)); |
481 ctxt)); |
478 |
482 |
915 IMPORTANT: rewrite rules must not introduce new Vars or TVars! |
919 IMPORTANT: rewrite rules must not introduce new Vars or TVars! |
916 *) |
920 *) |
917 |
921 |
918 fun rewritec (prover, maxt) ctxt t = |
922 fun rewritec (prover, maxt) ctxt t = |
919 let |
923 let |
|
924 val thy = Proof_Context.theory_of ctxt; |
920 val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt; |
925 val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt; |
921 val eta_thm = Thm.eta_conversion t; |
926 val eta_thm = Thm.eta_conversion t; |
922 val eta_t' = Thm.rhs_of eta_thm; |
927 val eta_t' = Thm.rhs_of eta_thm; |
923 val eta_t = Thm.term_of eta_t'; |
928 val eta_t = Thm.term_of eta_t'; |
924 fun rew rrule = |
929 fun rew rrule = |
925 let |
930 let |
926 val {thm, name, lhs, elhs, extra, fo, perm} = rrule |
931 val {thm = thm0, name, lhs, elhs = elhs0, extra, fo, perm} = rrule; |
|
932 val thm = Thm.transfer thy thm0; |
|
933 val elhs = Thm.transfer_cterm thy elhs0; |
927 val prop = Thm.prop_of thm; |
934 val prop = Thm.prop_of thm; |
928 val (rthm, elhs') = |
935 val (rthm, elhs') = |
929 if maxt = ~1 orelse not extra then (thm, elhs) |
936 if maxt = ~1 orelse not extra then (thm, elhs) |
930 else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); |
937 else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); |
|
938 |
931 val insts = |
939 val insts = |
932 if fo then Thm.first_order_match (elhs', eta_t') |
940 if fo then Thm.first_order_match (elhs', eta_t') |
933 else Thm.match (elhs', eta_t'); |
941 else Thm.match (elhs', eta_t'); |
934 val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); |
942 val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); |
935 val prop' = Thm.prop_of thm'; |
943 val prop' = Thm.prop_of thm'; |