87 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct |
87 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct |
88 in if rew then SOME (t', distinct op = asms) else NONE end |
88 in if rew then SOME (t', distinct op = asms) else NONE end |
89 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *) |
89 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *) |
90 and rew_sub thy i bdv tless rls put_asm lrd r t = |
90 and rew_sub thy i bdv tless rls put_asm lrd r t = |
91 (let |
91 (let |
|
92 (** )val _ = @{print}{a = "@ rew_sub: 1 < ?n \<Longrightarrow> NTH ?n..", r = UnparseC.term r};( *TODOO*) |
92 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r |
93 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r |
|
94 (** )val _ = @{print}{a = "@ rew_sub NO: patterns..", lhs = UnparseC.term lhs, rhs = UnparseC.term rhs};( *TODOO*) |
93 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r) |
95 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r) |
94 handle Pattern.MATCH => raise NO_REWRITE |
96 handle Pattern.MATCH => raise NO_REWRITE |
|
97 (** )val _ = @{print}{a = "@ Envir.subst_term: OK gives (3 + - 1)", r' = UnparseC.term r'};( *TODOO*) |
95 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) |
98 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) |
96 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' |
99 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' |
97 val _ = trace_in2 i "eval asms" thy r'; |
100 val _ = trace_in2 i "eval asms" thy r'; |
|
101 (** )val _ = @{print}{a = "@ eval asms", r' = UnparseC.term r'};( *TODOO*) |
98 val (t'', p'') = (*conditional rewriting*) |
102 val (t'', p'') = (*conditional rewriting*) |
99 let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls |
103 let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls |
|
104 (** )val _ = @{print}{a = "@ eval__true asms", simpl_p' = UnparseC.terms simpl_p', nofalse = nofalse};( *TODOO*) |
100 in |
105 in |
101 if nofalse |
106 if nofalse |
102 then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*) |
107 then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*) |
103 else (trace_in5 i "asms false" thy p'; raise NO_REWRITE) (* don't go into subtm.of cond*) |
108 else (trace_in5 i "asms false" thy p'; raise NO_REWRITE) (* don't go into subtm.of cond*) |
104 end |
109 end |
138 if t = @{term True} then (chk (indets @ a') asms) |
143 if t = @{term True} then (chk (indets @ a') asms) |
139 else if t = @{term False} then ([], false) |
144 else if t = @{term False} then ([], false) |
140 (*asm false .. thm not applied ^^^; continue until False vvv*) |
145 (*asm false .. thm not applied ^^^; continue until False vvv*) |
141 else chk (indets @ [t] @ a') asms); |
146 else chk (indets @ [t] @ a') asms); |
142 in chk [] asms end |
147 in chk [] asms end |
143 and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*) |
148 and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*) |
144 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'") |
149 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'") |
145 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*) |
150 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*) |
146 let |
151 let |
147 val _= trace_eq1 i "rls" rrls thy t; |
152 val _= trace_eq1 i "rls" rrls thy t; |
148 val (t', asm, rew) = app_rev thy (i + 1) rrls t |
153 val (t', asm, rew) = app_rev thy (i + 1) rrls t |