574 in |
574 in |
575 |
575 |
576 fun add_eqcong thm ss = ss |> |
576 fun add_eqcong thm ss = ss |> |
577 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
577 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
578 let |
578 let |
579 val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) |
579 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) |
580 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
580 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
581 (*val lhs = Envir.eta_contract lhs;*) |
581 (*val lhs = Envir.eta_contract lhs;*) |
582 val a = the (cong_name (head_of (term_of lhs))) handle Option.Option => |
582 val a = the (cong_name (head_of lhs)) handle Option.Option => |
583 raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); |
583 raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); |
584 val (xs, weak) = congs; |
584 val (xs, weak) = congs; |
585 val _ = |
585 val _ = |
586 if AList.defined (op =) xs a |
586 if AList.defined (op =) xs a |
587 then if_visible ss warning ("Overwriting congruence rule for " ^ quote a) |
587 then if_visible ss warning ("Overwriting congruence rule for " ^ quote a) |
591 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
591 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
592 |
592 |
593 fun del_eqcong thm ss = ss |> |
593 fun del_eqcong thm ss = ss |> |
594 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
594 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
595 let |
595 let |
596 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => |
596 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) |
597 raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
597 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
598 (*val lhs = Envir.eta_contract lhs;*) |
598 (*val lhs = Envir.eta_contract lhs;*) |
599 val a = the (cong_name (head_of lhs)) handle Option.Option => |
599 val a = the (cong_name (head_of lhs)) handle Option.Option => |
600 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
600 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
601 val (xs, _) = congs; |
601 val (xs, _) = congs; |
602 val xs' = filter_out (fn (x : string, _) => x = a) xs; |
602 val xs' = filter_out (fn (x : string, _) => x = a) xs; |