equal
deleted
inserted
replaced
573 fun tinst (a, _) = (((a, idx), \<^sort>\<open>type\<close>), \<^ctyp>\<open>bool\<close>) |
573 fun tinst (a, _) = (((a, idx), \<^sort>\<open>type\<close>), \<^ctyp>\<open>bool\<close>) |
574 fun inst (a, t) = |
574 fun inst (a, t) = |
575 ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t) |
575 ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t) |
576 in |
576 in |
577 thm |
577 thm |
578 |> Thm.generalize (tfrees, rnames @ frees) idx |
578 |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx |
579 |> Thm.instantiate (map tinst binsts, map inst binsts) |
579 |> Thm.instantiate (map tinst binsts, map inst binsts) |
580 end |
580 end |
581 |
581 |
582 fun transfer_rule_of_lhs ctxt t = |
582 fun transfer_rule_of_lhs ctxt t = |
583 let |
583 let |
594 fun tinst (a, _) = (((a, idx), \<^sort>\<open>type\<close>), \<^ctyp>\<open>bool\<close>) |
594 fun tinst (a, _) = (((a, idx), \<^sort>\<open>type\<close>), \<^ctyp>\<open>bool\<close>) |
595 fun inst (a, t) = |
595 fun inst (a, t) = |
596 ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t) |
596 ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t) |
597 in |
597 in |
598 thm |
598 thm |
599 |> Thm.generalize (tfrees, rnames @ frees) idx |
599 |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx |
600 |> Thm.instantiate (map tinst binsts, map inst binsts) |
600 |> Thm.instantiate (map tinst binsts, map inst binsts) |
601 end |
601 end |
602 |
602 |
603 fun eq_rules_tac ctxt eq_rules = |
603 fun eq_rules_tac ctxt eq_rules = |
604 TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules) |
604 TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules) |
716 THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 |
716 THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 |
717 handle TERM (_, ts) => |
717 handle TERM (_, ts) => |
718 raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |
718 raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |
719 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
719 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
720 |> Simplifier.norm_hhf ctxt' |
720 |> Simplifier.norm_hhf ctxt' |
721 |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) |
721 |> Drule.generalize |
|
722 (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty) |
722 |> Drule.zero_var_indexes |
723 |> Drule.zero_var_indexes |
723 end |
724 end |
724 (* |
725 (* |
725 handle THM _ => thm |
726 handle THM _ => thm |
726 *) |
727 *) |
751 THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 |
752 THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 |
752 handle TERM (_, ts) => |
753 handle TERM (_, ts) => |
753 raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |
754 raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |
754 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
755 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
755 |> Simplifier.norm_hhf ctxt' |
756 |> Simplifier.norm_hhf ctxt' |
756 |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) |
757 |> Drule.generalize |
|
758 (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty) |
757 |> Drule.zero_var_indexes |
759 |> Drule.zero_var_indexes |
758 end |
760 end |
759 |
761 |
760 (** Methods and attributes **) |
762 (** Methods and attributes **) |
761 |
763 |