119 fun steps ctxt rew_ord erls rules fo ifo = |
119 fun steps ctxt rew_ord erls rules fo ifo = |
120 let |
120 let |
121 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty |
121 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty |
122 | derivat dt = (#1 o #3 o last_elem) dt |
122 | derivat dt = (#1 o #3 o last_elem) dt |
123 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2 |
123 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2 |
124 val fod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE fo |
124 val fod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE fo |
125 val ifod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE ifo |
125 val ifod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE ifo |
126 in |
126 in |
127 case (fod, ifod) of |
127 case (fod, ifod) of |
128 ([], []) => if fo = ifo then (true, []) else (false, []) |
128 ([], []) => if fo = ifo then (true, []) else (false, []) |
129 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) |
129 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) |
130 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) |
130 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) |