# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 7b5846065c1be739343b04a91a420cf15d0306db
# Parent  bd064bc710854f515e52dfe3955afe8408ea1fbf
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)

diff -r bd064bc71085 -r 7b5846065c1b src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -85,10 +85,10 @@
   val extract_isabelle_status : (string, 'a) ho_term list -> string option
   val extract_isabelle_rank : (string, 'a) ho_term list -> int
   val introN : string
-  val spec_introN : string
+  val inductiveN : string
   val elimN : string
   val simpN : string
-  val spec_eqN : string
+  val defN : string
   val rankN : string
   val minimum_rank : int
   val default_rank : int
@@ -218,10 +218,10 @@
 val isabelle_info_prefix = "isabelle_"
 
 val introN = "intro"
-val spec_introN = "spec_intro"
+val inductiveN = "inductive"
 val elimN = "elim"
 val simpN = "simp"
-val spec_eqN = "spec_eq"
+val defN = "def"
 val rankN = "rank"
 
 val minimum_rank = 0
@@ -470,7 +470,7 @@
     fun suffix_tag top_level s =
       if flavor = DFG_Sorted andalso top_level then
         case extract_isabelle_status info of
-          SOME s' => if s' = spec_eqN then s ^ ":lt"
+          SOME s' => if s' = defN then s ^ ":lt"
                      else if s' = simpN andalso gen_simp then s ^ ":lr"
                      else s
         | NONE => s
diff -r bd064bc71085 -r 7b5846065c1b src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -17,7 +17,7 @@
 
   datatype scope = Global | Local | Assum | Chained
   datatype status =
-    General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
+    General | Induction | Intro | Inductive | Elim | Simp | Def
   type stature = scope * status
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -548,7 +548,7 @@
     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
 
 datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
+datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
 type stature = scope * status
 
 datatype order = First_Order | Higher_Order
@@ -1225,8 +1225,7 @@
             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
     val lam_facts =
       map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
-                (Axiom, t)))
+               ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
@@ -1696,8 +1695,7 @@
             [t]
         end
         |> tag_list 1
-        |> map (fn (k, t) =>
-                   ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
+        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t))
       val make_facts = map_filter (make_fact ctxt format type_enc false)
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
@@ -1993,10 +1991,10 @@
    let val rank = rank j in
      case snd stature of
        Intro => isabelle_info introN rank
-     | Spec_Intro => isabelle_info spec_introN rank
+     | Inductive => isabelle_info inductiveN rank
      | Elim => isabelle_info elimN rank
      | Simp => isabelle_info simpN rank
-     | Spec_Eq => isabelle_info spec_eqN rank
+     | Def => isabelle_info defN rank
      | _ => isabelle_info "" rank
    end)
   |> Formula
@@ -2010,7 +2008,7 @@
                      type_class_formula type_enc superclass ty_arg])
              |> mk_aquant AForall
                           [(tvar_a_name, atype_of_type_vars type_enc)],
-             NONE, isabelle_info spec_introN helper_rank)
+             NONE, isabelle_info inductiveN helper_rank)
   end
 
 fun formula_from_arity_atom type_enc (class, t, args) =
@@ -2024,7 +2022,7 @@
                     (formula_from_arity_atom type_enc concl_atom)
            |> mk_aquant AForall
                   (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
-           NONE, isabelle_info spec_introN helper_rank)
+           NONE, isabelle_info inductiveN helper_rank)
 
 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
@@ -2240,7 +2238,7 @@
                                     always_guard_var_in_formula (SOME true)
            |> close_formula_universally
            |> bound_tvars type_enc true (atomic_types_of T),
-           NONE, isabelle_info spec_introN helper_rank)
+           NONE, isabelle_info inductiveN helper_rank)
 
 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
   let val x_var = ATerm (`make_bound_var "X", []) in
@@ -2249,7 +2247,7 @@
              Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
-             NONE, isabelle_info spec_eqN helper_rank)
+             NONE, isabelle_info defN helper_rank)
   end
 
 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2320,7 +2318,7 @@
              |> close_formula_universally
              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
              |> maybe_negate,
-             NONE, isabelle_info spec_introN helper_rank)
+             NONE, isabelle_info inductiveN helper_rank)
   end
 
 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
@@ -2354,7 +2352,7 @@
         in
           cons (Formula (ident_base ^ "_res", kind,
                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
-                         NONE, isabelle_info spec_eqN helper_rank))
+                         NONE, isabelle_info defN helper_rank))
         end
       else
         I
@@ -2456,7 +2454,7 @@
       in
         ([tm1, tm2],
          [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
-                   NONE, isabelle_info spec_eqN helper_rank)])
+                   NONE, isabelle_info defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
@@ -2792,9 +2790,9 @@
     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
       Graph.empty
-      |> fold (fold (add_eq_deps (has_status spec_eqN)) o snd) problem
+      |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
       |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
-      |> fold (fold (add_intro_deps (has_status spec_introN)) o snd) problem
+      |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
       |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
     fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
     fun add_weights _ [] = I
diff -r bd064bc71085 -r 7b5846065c1b src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -112,7 +112,14 @@
 val theory_const_suffix = Long_Name.separator ^ " 1"
 
 (* unfolding these can yield really huge terms *)
-val risky_spec_eqs = @{thms Bit0_def Bit1_def}
+val risky_defs = @{thms Bit0_def Bit1_def}
+
+fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
+fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
+  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
+  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
+  | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
+  | is_rec_def _ = false
 
 fun clasimpset_rule_table_of ctxt =
   let
@@ -138,22 +145,24 @@
 *)
     val simps = ctxt |> simpset_of |> dest_ss |> #simps
     val specs = ctxt |> Spec_Rules.get
-    val spec_eqs =
+    val (rec_defs, nonrec_defs) =
       specs |> filter (curry (op =) Spec_Rules.Equational o fst)
             |> maps (snd o snd)
-            |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
+            |> filter_out (member Thm.eq_thm_prop risky_defs)
+            |> List.partition (is_rec_def o prop_of)
     val spec_intros =
       specs |> filter (member (op =) [Spec_Rules.Inductive,
                                       Spec_Rules.Co_Inductive] o fst)
             |> maps (snd o snd)
   in
     Termtab.empty |> add Simp [atomize] snd simps
-                  |> add Spec_Eq [] I spec_eqs
+                  |> add Simp [] I rec_defs
+                  |> add Def [] I nonrec_defs
 (* Add once it is used:
                   |> add Elim [] I elims
 *)
                   |> add Intro [] I intros
-                  |> add Spec_Intro [] I spec_intros
+                  |> add Inductive [] I spec_intros
   end
 
 fun needs_quoting reserved s =
@@ -184,7 +193,7 @@
   (* FIXME: use structured name *)
   if String.isSubstring ".induct" name orelse
      String.isSubstring ".inducts" name then
-    Induct
+    Induction
   else case Termtab.lookup css_table (prop_of th) of
     SOME status => status
   | NONE => General
diff -r bd064bc71085 -r 7b5846065c1b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -172,7 +172,7 @@
   get_prover ctxt mode name params minimize_command problem
   |> minimize ctxt mode name params problem
 
-fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
+fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
   | is_induction_fact _ = false
 
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,