Abduction: show error messages for unsupported problems.

Unsupported:
 - too large syntax tree.
 - the "assumes" keyword.

Other clean-up.
Especially, I put all the auxiliary lemmas in Top_Down_Util.ML
into the structure there.

The keyword "smart_induct" and "sem_ind" are now synonyms.

Abduction/Abduction.thy

@@ -10,7 +10,6 @@ theory Abduction
 begin
 
 ML_file \<open>Top_Down_Util.ML\<close>
-
 ML_file \<open>And_Node.ML\<close>
 ML_file \<open>Or_Node.ML\<close>
 ML_file \<open>Or2And_Edge.ML\<close>
@@ -19,7 +18,6 @@ ML_file \<open>Update_Abduction_Node.ML\<close>
 ML_file \<open>Abduction_Graph.ML\<close>
 ML_file \<open>Update_Abduction_Graph.ML\<close>
 ML_file \<open>Shared_State.ML\<close>
-
 ML_file \<open>Generalise_By_Renaming.ML\<close>
 ML_file \<open>Term_Table_for_Abduction.ML\<close>
 ML_file \<open>Generalise_Then_Extend.ML\<close>
@@ -98,13 +96,23 @@ val short_statement =
 
 fun theorem _ descr =
   Outer_Syntax.local_theory @{command_keyword prove} ("state " ^ descr)
-    (((long_statement || short_statement) >> (fn (_, _, _, _(*elems*), concl) =>
+    (((long_statement || short_statement) >> (fn (_, _, _, elems, concl) =>
        (fn lthy =>
           let
-            fun stmt_to_stmt_as_string (Element.Shows [((_, _), [(stmt, _)])]) = stmt: string
+            fun is_not_fix (Element.Fixes _) = false
+              | is_not_fix _                 = true
+            fun is_supported (elements:Element.context list) = exists is_not_fix elements;
+            val _ = if is_supported elems then () else error
+                     ("Currently, the \"prover\" keyword does not support the use of following keywords: \n" ^
+                      "\"constraints\", \"assumes\", \"defines\", \"notes\", and  \"lazy_notes\".\n" ^
+                      "Please present your proof goal as one single term.")
+            fun stmt_to_stmt_as_string (Element.Shows [((_, _), [(stmt, strs:strings)])]) = ( (tracing o Int.toString o length) strs; stmt: string)
               | stmt_to_stmt_as_string _ = error "stmt_to_concl_name failed in United_Reasoning";
             val start = (fn _ => Timing.start ()) lthy: Timing.start;
-            val cncl_as_trm  = Syntax.read_term lthy (stmt_to_stmt_as_string concl) |> Top_Down_Util.standardize_vnames: term;
+            val cncl_as_trm  = Syntax.read_term lthy (stmt_to_stmt_as_string concl)
+                            |> Top_Down_Util.standardize_vnames: term;
+            val _ = if Term.size_of_term cncl_as_trm < 100 then ()
+                    else error "Your problem size seems too large for Abduction Prover.\n Can you rephrase it?";
             val standardized_cncl = Top_Down_Util.standardize_vnames cncl_as_trm;
             val cxtx_wo_verbose_warnings =
                 Config.put SMT_Config.verbose false lthy
@@ -131,22 +139,11 @@ val _ = theorem \<^command_keyword>\<open>prove\<close> "prove";
 end;
 \<close>
 
-ML\<open>
-structure df = Syntax
-type tsdf = thm
-val thm = Top_Down_Util.term_to_thm @{context} (Syntax.read_term @{context} "x = x");
-\<close>
-find_theorems name: "List"
 ML\<open>
 structure TDU  = Top_Down_Util;
 structure SS   = Shared_State;
 structure SOOE = Seed_Of_Or2And_Edge;
 
-val timeout = Isabelle_Utils.timeout_apply (Time.fromSeconds 1);
-
-val d = Basic_Simplifier.asm_full_simplify @{context} thm;
-val s = simp_non_prop_term @{context} @{term "True = True"};
-
 fun simp_explicit_conjecture (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context)
   (simp as (_:string, simp_term:term)) (cnjctr as (_:string, cnjctr_term:term)): SOOE.conjectures =
   let
@@ -173,24 +170,6 @@ fun simp_explicit_conjecture (synched_term2string:SS.synched_term2string_table)
 fun simp_explicit_conjectures (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context)
   (cnjctrs:SOOE.conjectures) (simp:SOOE.conjecture): SOOE.conjectures =
   map (simp_explicit_conjecture synched_term2string ctxt simp) cnjctrs |> flat;
-
-
-
-
-val sdf = Thm.prop_of @{thm List.distinct_adj_Nil};
 \<close>
-ML\<open>
-val saf = @{thm List.distinct_adj_ConsD} |> Thm.full_prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
-\<close>
-thm List.distinct_adj_Nil
-
-lemma "False \<Longrightarrow> True"
-  apply(tactic \<open>fn thm => (
-    thm |> Thm.full_prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
-    thm |> Thm.prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
-    thm |> Thm.concl_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
-
-    Seq.single thm)\<close>)
-  oops
 
 end

Abduction/Abduction_Graph.ML

@@ -315,7 +315,7 @@ fun final_goal_proved_completely (graph:abduction_graph) =
 (* prove_term_completely *)
 fun prove_term_completely (pst:Proof.state) (lemma_term:term) =
     let
-      val pst_to_prove = mk_pst_to_prove_from_term pst lemma_term                                   : Proof.state;
+      val pst_to_prove = Top_Down_Util.mk_pst_to_prove_from_term pst lemma_term                                   : Proof.state;
       val timeouts     = {overall = 30.0, hammer = 10.0, quickcheck = 1.0, nitpick = 2.0}           : TBC_Utils.timeouts;
       val maybe_result = TBC_Utils.pst_to_proofscripts_opt timeouts "Attack_On_Or_Node" pst_to_prove: (strings * Proof.state) option;
       val maybe_script = Option.map fst maybe_result                                                : strings option;

Abduction/All_Top_Down_Conjecturing.ML

@@ -9,7 +9,10 @@
 structure All_Top_Down_Conjecturing(*: TOP_DOWN_CONJECTURING*) =
 struct
 
-fun is_composite trm = Isabelle_Utils.is_Abs trm orelse Isabelle_Utils.is_App trm: bool;
+structure IU  = Isabelle_Utils;
+structure TDU = Top_Down_Util;
+
+fun is_composite trm = IU.is_Abs trm orelse IU.is_App trm: bool;
 
 fun has_no_multiple_occ_of_composite_subtrm (ctxt:Proof.context) (trm:term) =
 let
@@ -24,7 +27,7 @@ let
       has_multi
     end;
   val duplicated_prints     = filter print_has_multiple_paths prints: strings;
-  fun checker printed_term  = Isabelle_Utils.read_term_then_check_term ctxt printed_term is_composite: bool;
+  fun checker printed_term  = IU.read_term_then_check_term ctxt printed_term is_composite: bool;
   val duplicated_composites = filter checker duplicated_prints: strings;
   val has_dupulicates       = null duplicated_composites: bool;
 in
@@ -59,8 +62,8 @@ fun template_based_conjecture_for_simplification term2name (ctxt:Proof.context)
         @ TBC.ctxt_n_consts_to_square      ctxt tm)
        |> map (apfst Template_Based_Conjecturing.property_as_string)
        |> map (fn (_,    term) => (SS.get_lemma_name term2name ctxt term, term));;
-    val result = map (ctxt_n_const_to_all_conjecture_term ctxt) (relevant_unary_funcs @ relevant_binary_funcs) |> flat
-      : (string * term) list;
+    val result = map (ctxt_n_const_to_all_conjecture_term ctxt) (relevant_unary_funcs @ relevant_binary_funcs)
+              |> flat: (string * term) list;
   in
     result
   end;
@@ -70,7 +73,7 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st
     val ctxt = Proof.context_of pst: Proof.context;
     fun tracing' mssg = ();
     val _ = tracing' "[[[[[[[[[[[top_down_conjecture starts]]]]]]]]]]": unit;
-    val standardized_trm = Top_Down_Util.standardize_vnames trm
+    val standardized_trm = TDU.standardize_vnames trm
     val results = (
       Remove_Outermost_Assumption.top_down_conjectures term2name pst standardized_trm
     @ Generalise_By_Renaming.top_down_conjectures term2name pst standardized_trm
@@ -79,18 +82,18 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st
     @ Abstract_Same_Term.top_down_conjectures term2name pst standardized_trm
     @ Replace_Imp_With_Eq.top_down_conjectures term2name pst standardized_trm
     @ template_conjectures ctxt standardized_trm)
-      |> Par_List.map (apsnd (simp_non_prop_term ctxt))
-      |> Par_List.map (apsnd Top_Down_Util.standardize_vnames)
-      |> map (fn (name, term) => (name, Syntax.check_term ctxt term))(*necessary to apply Top_Down_Util.is_prop in some cases*)
-      |> map (fn (name, term) => (name, if Top_Down_Util.is_prop term then term else HOLogic.mk_Trueprop term))
+      |> Par_List.map (apsnd (TDU.simp_non_prop_term ctxt))
+      |> Par_List.map (apsnd TDU.standardize_vnames)
+      |> map (fn (name, term) => (name, Syntax.check_term ctxt term))(*necessary to apply TDU.is_prop in some cases*)
+      |> map (fn (name, term) => (name, if TDU.is_prop term then term else HOLogic.mk_Trueprop term))
       |> distinct (fn (f, s) => snd f = snd s)
     (*|> parallel_filter_out (fn (_, trm) => eq_over_same_func ctxt trm)*)
-      |> parallel_filter_out (fn (_, cnjctr_trm) => cnjctr_trm = trm)
-      |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.has_func_with_three_occs_in_a_row)
-      |> parallel_filter     (fn (_, trm) => S4TD.run_assertion pst trm S4TD.fvars_in_prem_should_appear_in_concl)
-      |> parallel_filter     (fn (_, trm) => S4TD.run_assertion pst trm S4TD.does_not_have_trivial_equality)
-      |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.nested_eq)
-      |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.var_appears_many_times_but_always_in_the_same_subtrm)
+      |> TDU.parallel_filter_out (fn (_, cnjctr_trm) => cnjctr_trm = trm)
+      |> TDU.parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.has_func_with_three_occs_in_a_row)
+      |> TDU.parallel_filter     (fn (_, trm) => S4TD.run_assertion pst trm S4TD.fvars_in_prem_should_appear_in_concl)
+      |> TDU.parallel_filter     (fn (_, trm) => S4TD.run_assertion pst trm S4TD.does_not_have_trivial_equality)
+      |> TDU.parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.nested_eq)
+      |> TDU.parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.var_appears_many_times_but_always_in_the_same_subtrm)
       |> map (fn (_,    term) => (SS.get_lemma_name term2name ctxt term, term));
     val _ = tracing' "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit;
   in

Abduction/Generalise_By_Renaming.ML

@@ -58,7 +58,7 @@ fun replace (Const p) [] = Const p
   | replace _ _ = error "replace failed. Pattern-matching failed!";
 
 fun generalise_by_rename_free_variables' _ (trm:term) =
-  if 0 < count_fvars trm andalso count_fvars trm < 8
+  if 0 < count_fvars trm andalso count_fvars trm < 8(*TODO: magic number*)
   then
     let
       val numb_of_fvars = count_fvars trm: int;

Abduction/Generalise_Then_Extend.ML

@@ -26,7 +26,7 @@ fun extension_for_one_lhs_n_one_func (ctxt:Proof.context) (lhs:term, candidate_a
     val eqs_wo_meaningless_compound = filter_out has_fvar_appearing_only_in_the_same_compound_trm eqs_checked
     val result_as_strings           = map (Isabelle_Utils.trm_to_string ctxt) eqs_wo_meaningless_compound: strings;
     val result_as_terms             = List.mapPartial (try (Syntax.read_prop ctxt)) result_as_strings    : terms;
-    val result_wo_type_consts       = map remove_type_consts result_as_terms                             : terms;
+    val result_wo_type_consts       = map Isabelle_Utils.strip_atyp result_as_terms                      : terms;
   in
     result_wo_type_consts
   end;