equal
deleted
inserted
replaced
474 |
474 |
475 fun init_state thy eval_rls ro t = |
475 fun init_state thy eval_rls ro t = |
476 let |
476 let |
477 val SOME (t', _) = factout_p_ thy t; |
477 val SOME (t', _) = factout_p_ thy t; |
478 val SOME (t'', asm) = cancel_p_ thy t; |
478 val SOME (t'', asm) = cancel_p_ thy t; |
479 val der = Derive.reverse_deriv thy eval_rls rules ro NONE t'; |
479 val der = Derive.steps_reverse thy eval_rls rules ro NONE t'; |
480 val der = der @ |
480 val der = der @ |
481 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))] |
481 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))] |
482 val rs = (Rtools.distinct_Thm o (map #1)) der |
482 val rs = (Rtools.distinct_Thm o (map #1)) der |
483 val rs = filter_out (Rtools.eq_Thms |
483 val rs = filter_out (Rtools.eq_Thms |
484 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs |
484 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs |
496 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) []) |
496 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) []) |
497 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate"; |
497 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate"; |
498 |
498 |
499 fun next_rule thy eval_rls ro [rs] t = |
499 fun next_rule thy eval_rls ro [rs] t = |
500 let |
500 let |
501 val der = Derive.make_deriv thy eval_rls rs ro NONE t; |
501 val der = Derive.do_one thy eval_rls rs ro NONE t; |
502 in case der of (_, r, _) :: _ => SOME r | _ => NONE end |
502 in case der of (_, r, _) :: _ => SOME r | _ => NONE end |
503 | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate"); |
503 | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate"); |
504 |
504 |
505 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = |
505 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = |
506 [(*TODO*)]: ( Rule.rule * (term * term list)) list; |
506 [(*TODO*)]: ( Rule.rule * (term * term list)) list; |
535 |
535 |
536 fun init_state thy eval_rls ro t = |
536 fun init_state thy eval_rls ro t = |
537 let |
537 let |
538 val SOME (t',_) = common_nominator_p_ thy t; |
538 val SOME (t',_) = common_nominator_p_ thy t; |
539 val SOME (t'', asm) = add_fraction_p_ thy t; |
539 val SOME (t'', asm) = add_fraction_p_ thy t; |
540 val der = Derive.reverse_deriv thy eval_rls rules ro NONE t'; |
540 val der = Derive.steps_reverse thy eval_rls rules ro NONE t'; |
541 val der = der @ |
541 val der = der @ |
542 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))] |
542 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))] |
543 val rs = (Rtools.distinct_Thm o (map #1)) der; |
543 val rs = (Rtools.distinct_Thm o (map #1)) der; |
544 val rs = filter_out (Rtools.eq_Thms |
544 val rs = filter_out (Rtools.eq_Thms |
545 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs; |
545 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs; |
557 []) end |
557 []) end |
558 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) []) |
558 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) []) |
559 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate"; |
559 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate"; |
560 |
560 |
561 fun next_rule thy eval_rls ro [rs] t = |
561 fun next_rule thy eval_rls ro [rs] t = |
562 let val der = Derive.make_deriv thy eval_rls rs ro NONE t; |
562 let val der = Derive.do_one thy eval_rls rs ro NONE t; |
563 in |
563 in |
564 case der of |
564 case der of |
565 (_,r,_)::_ => SOME r |
565 (_,r,_)::_ => SOME r |
566 | _ => NONE |
566 | _ => NONE |
567 end |
567 end |