797 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
797 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
798 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
798 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
799 is_that_fact thm |
799 is_that_fact thm |
800 end) |
800 end) |
801 |
801 |
802 fun meta_equify (@{const Trueprop} |
802 val crude_zero_vars = |
803 $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) = |
803 map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t) |
804 Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2 |
|
805 | meta_equify t = t |
|
806 |
|
807 val normalize_simp_prop = |
|
808 meta_equify |
|
809 #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t) |
|
810 #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S))) |
804 #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S))) |
811 |
805 |
812 fun clasimpset_rule_table_of ctxt = |
806 fun clasimpset_rule_table_of ctxt = |
813 let |
807 let |
814 fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f) |
808 val thy = Proof_Context.theory_of ctxt |
815 val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs |
809 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy |
|
810 fun add loc g f = |
|
811 fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f) |
|
812 val {safeIs, safeEs, hazIs, hazEs, ...} = |
|
813 ctxt |> claset_of |> Classical.rep_cs |
816 val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
814 val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
817 val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs) |
815 val elims = |
|
816 Item_Net.content safeEs @ Item_Net.content hazEs |
|
817 |> map Classical.classical_rule |
818 val simps = ctxt |> simpset_of |> dest_ss |> #simps |
818 val simps = ctxt |> simpset_of |> dest_ss |> #simps |
819 in |
819 in |
820 Termtab.empty |> add Intro I I intros |
820 Termtab.empty |> add Intro I I intros |
821 |> add Elim I I elims |
821 |> add Elim I I elims |
822 |> add Simp I snd simps |
822 |> add Simp I snd simps |
823 |> add Simp normalize_simp_prop snd simps |
823 |> add Simp atomize snd simps |
824 end |
824 end |
825 |
825 |
826 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = |
826 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = |
827 let |
827 let |
828 val thy = Proof_Context.theory_of ctxt |
828 val thy = Proof_Context.theory_of ctxt |
831 val named_locals = local_facts |> Facts.dest_static [] |
831 val named_locals = local_facts |> Facts.dest_static [] |
832 val assms = Assumption.all_assms_of ctxt |
832 val assms = Assumption.all_assms_of ctxt |
833 fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms |
833 fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms |
834 val is_chained = member Thm.eq_thm_prop chained_ths |
834 val is_chained = member Thm.eq_thm_prop chained_ths |
835 val clasimpset_table = clasimpset_rule_table_of ctxt |
835 val clasimpset_table = clasimpset_rule_table_of ctxt |
836 fun locality_of_theorem global (name: string) th = |
836 fun locality_of_theorem global name th = |
837 if String.isSubstring ".induct" name orelse(*FIXME: use structured name*) |
837 if String.isSubstring ".induct" name orelse (*FIXME: use structured name*) |
838 String.isSubstring ".inducts" name then |
838 String.isSubstring ".inducts" name then |
839 Induction |
839 Induction |
840 else if is_chained th then |
840 else if is_chained th then |
841 Chained |
841 Chained |
842 else if global then |
842 else if global then |
843 case Termtab.lookup clasimpset_table (prop_of th) of |
843 case Termtab.lookup clasimpset_table (prop_of th) of |
844 SOME loc => loc |
844 SOME loc => loc |
845 | NONE => General |
845 | NONE => General |
846 else if is_assum th then Assum else Local |
846 else if is_assum th then |
|
847 Assum |
|
848 else |
|
849 Local |
847 fun is_good_unnamed_local th = |
850 fun is_good_unnamed_local th = |
848 not (Thm.has_name_hint th) andalso |
851 not (Thm.has_name_hint th) andalso |
849 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals |
852 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals |
850 val unnamed_locals = |
853 val unnamed_locals = |
851 union Thm.eq_thm_prop (Facts.props local_facts) chained_ths |
854 union Thm.eq_thm_prop (Facts.props local_facts) chained_ths |