be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
authorblanchet
Tue Mar 27 16:59:13 2012 +0300 (2012-03-27)
changeset 471487b5846065c1b
parent 47147 bd064bc71085
child 47149 97f8c6c88134
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -85,10 +85,10 @@
     1.4    val extract_isabelle_status : (string, 'a) ho_term list -> string option
     1.5    val extract_isabelle_rank : (string, 'a) ho_term list -> int
     1.6    val introN : string
     1.7 -  val spec_introN : string
     1.8 +  val inductiveN : string
     1.9    val elimN : string
    1.10    val simpN : string
    1.11 -  val spec_eqN : string
    1.12 +  val defN : string
    1.13    val rankN : string
    1.14    val minimum_rank : int
    1.15    val default_rank : int
    1.16 @@ -218,10 +218,10 @@
    1.17  val isabelle_info_prefix = "isabelle_"
    1.18  
    1.19  val introN = "intro"
    1.20 -val spec_introN = "spec_intro"
    1.21 +val inductiveN = "inductive"
    1.22  val elimN = "elim"
    1.23  val simpN = "simp"
    1.24 -val spec_eqN = "spec_eq"
    1.25 +val defN = "def"
    1.26  val rankN = "rank"
    1.27  
    1.28  val minimum_rank = 0
    1.29 @@ -470,7 +470,7 @@
    1.30      fun suffix_tag top_level s =
    1.31        if flavor = DFG_Sorted andalso top_level then
    1.32          case extract_isabelle_status info of
    1.33 -          SOME s' => if s' = spec_eqN then s ^ ":lt"
    1.34 +          SOME s' => if s' = defN then s ^ ":lt"
    1.35                       else if s' = simpN andalso gen_simp then s ^ ":lr"
    1.36                       else s
    1.37          | NONE => s
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5    datatype scope = Global | Local | Assum | Chained
     2.6    datatype status =
     2.7 -    General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
     2.8 +    General | Induction | Intro | Inductive | Elim | Simp | Def
     2.9    type stature = scope * status
    2.10  
    2.11    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    2.12 @@ -548,7 +548,7 @@
    2.13      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
    2.14  
    2.15  datatype scope = Global | Local | Assum | Chained
    2.16 -datatype status = General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
    2.17 +datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
    2.18  type stature = scope * status
    2.19  
    2.20  datatype order = First_Order | Higher_Order
    2.21 @@ -1225,8 +1225,7 @@
    2.22              |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    2.23      val lam_facts =
    2.24        map2 (fn t => fn j =>
    2.25 -               ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
    2.26 -                (Axiom, t)))
    2.27 +               ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
    2.28             lambda_ts (1 upto length lambda_ts)
    2.29    in (facts, lam_facts) end
    2.30  
    2.31 @@ -1696,8 +1695,7 @@
    2.32              [t]
    2.33          end
    2.34          |> tag_list 1
    2.35 -        |> map (fn (k, t) =>
    2.36 -                   ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
    2.37 +        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t))
    2.38        val make_facts = map_filter (make_fact ctxt format type_enc false)
    2.39        val fairly_sound = is_type_enc_fairly_sound type_enc
    2.40      in
    2.41 @@ -1993,10 +1991,10 @@
    2.42     let val rank = rank j in
    2.43       case snd stature of
    2.44         Intro => isabelle_info introN rank
    2.45 -     | Spec_Intro => isabelle_info spec_introN rank
    2.46 +     | Inductive => isabelle_info inductiveN rank
    2.47       | Elim => isabelle_info elimN rank
    2.48       | Simp => isabelle_info simpN rank
    2.49 -     | Spec_Eq => isabelle_info spec_eqN rank
    2.50 +     | Def => isabelle_info defN rank
    2.51       | _ => isabelle_info "" rank
    2.52     end)
    2.53    |> Formula
    2.54 @@ -2010,7 +2008,7 @@
    2.55                       type_class_formula type_enc superclass ty_arg])
    2.56               |> mk_aquant AForall
    2.57                            [(tvar_a_name, atype_of_type_vars type_enc)],
    2.58 -             NONE, isabelle_info spec_introN helper_rank)
    2.59 +             NONE, isabelle_info inductiveN helper_rank)
    2.60    end
    2.61  
    2.62  fun formula_from_arity_atom type_enc (class, t, args) =
    2.63 @@ -2024,7 +2022,7 @@
    2.64                      (formula_from_arity_atom type_enc concl_atom)
    2.65             |> mk_aquant AForall
    2.66                    (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
    2.67 -           NONE, isabelle_info spec_introN helper_rank)
    2.68 +           NONE, isabelle_info inductiveN helper_rank)
    2.69  
    2.70  fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
    2.71          ({name, kind, iformula, atomic_types, ...} : translated_formula) =
    2.72 @@ -2240,7 +2238,7 @@
    2.73                                      always_guard_var_in_formula (SOME true)
    2.74             |> close_formula_universally
    2.75             |> bound_tvars type_enc true (atomic_types_of T),
    2.76 -           NONE, isabelle_info spec_introN helper_rank)
    2.77 +           NONE, isabelle_info inductiveN helper_rank)
    2.78  
    2.79  fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
    2.80    let val x_var = ATerm (`make_bound_var "X", []) in
    2.81 @@ -2249,7 +2247,7 @@
    2.82               Axiom,
    2.83               eq_formula type_enc (atomic_types_of T) [] false
    2.84                    (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
    2.85 -             NONE, isabelle_info spec_eqN helper_rank)
    2.86 +             NONE, isabelle_info defN helper_rank)
    2.87    end
    2.88  
    2.89  fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
    2.90 @@ -2320,7 +2318,7 @@
    2.91               |> close_formula_universally
    2.92               |> bound_tvars type_enc (n > 1) (atomic_types_of T)
    2.93               |> maybe_negate,
    2.94 -             NONE, isabelle_info spec_introN helper_rank)
    2.95 +             NONE, isabelle_info inductiveN helper_rank)
    2.96    end
    2.97  
    2.98  fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
    2.99 @@ -2354,7 +2352,7 @@
   2.100          in
   2.101            cons (Formula (ident_base ^ "_res", kind,
   2.102                           eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
   2.103 -                         NONE, isabelle_info spec_eqN helper_rank))
   2.104 +                         NONE, isabelle_info defN helper_rank))
   2.105          end
   2.106        else
   2.107          I
   2.108 @@ -2456,7 +2454,7 @@
   2.109        in
   2.110          ([tm1, tm2],
   2.111           [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
   2.112 -                   NONE, isabelle_info spec_eqN helper_rank)])
   2.113 +                   NONE, isabelle_info defN helper_rank)])
   2.114          |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
   2.115              else pair_append (do_alias (ary - 1)))
   2.116        end
   2.117 @@ -2792,9 +2790,9 @@
   2.118      fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
   2.119      val graph =
   2.120        Graph.empty
   2.121 -      |> fold (fold (add_eq_deps (has_status spec_eqN)) o snd) problem
   2.122 +      |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
   2.123        |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
   2.124 -      |> fold (fold (add_intro_deps (has_status spec_introN)) o snd) problem
   2.125 +      |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
   2.126        |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
   2.127      fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
   2.128      fun add_weights _ [] = I
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
     3.3 @@ -112,7 +112,14 @@
     3.4  val theory_const_suffix = Long_Name.separator ^ " 1"
     3.5  
     3.6  (* unfolding these can yield really huge terms *)
     3.7 -val risky_spec_eqs = @{thms Bit0_def Bit1_def}
     3.8 +val risky_defs = @{thms Bit0_def Bit1_def}
     3.9 +
    3.10 +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    3.11 +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    3.12 +  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    3.13 +  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    3.14 +  | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    3.15 +  | is_rec_def _ = false
    3.16  
    3.17  fun clasimpset_rule_table_of ctxt =
    3.18    let
    3.19 @@ -138,22 +145,24 @@
    3.20  *)
    3.21      val simps = ctxt |> simpset_of |> dest_ss |> #simps
    3.22      val specs = ctxt |> Spec_Rules.get
    3.23 -    val spec_eqs =
    3.24 +    val (rec_defs, nonrec_defs) =
    3.25        specs |> filter (curry (op =) Spec_Rules.Equational o fst)
    3.26              |> maps (snd o snd)
    3.27 -            |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
    3.28 +            |> filter_out (member Thm.eq_thm_prop risky_defs)
    3.29 +            |> List.partition (is_rec_def o prop_of)
    3.30      val spec_intros =
    3.31        specs |> filter (member (op =) [Spec_Rules.Inductive,
    3.32                                        Spec_Rules.Co_Inductive] o fst)
    3.33              |> maps (snd o snd)
    3.34    in
    3.35      Termtab.empty |> add Simp [atomize] snd simps
    3.36 -                  |> add Spec_Eq [] I spec_eqs
    3.37 +                  |> add Simp [] I rec_defs
    3.38 +                  |> add Def [] I nonrec_defs
    3.39  (* Add once it is used:
    3.40                    |> add Elim [] I elims
    3.41  *)
    3.42                    |> add Intro [] I intros
    3.43 -                  |> add Spec_Intro [] I spec_intros
    3.44 +                  |> add Inductive [] I spec_intros
    3.45    end
    3.46  
    3.47  fun needs_quoting reserved s =
    3.48 @@ -184,7 +193,7 @@
    3.49    (* FIXME: use structured name *)
    3.50    if String.isSubstring ".induct" name orelse
    3.51       String.isSubstring ".inducts" name then
    3.52 -    Induct
    3.53 +    Induction
    3.54    else case Termtab.lookup css_table (prop_of th) of
    3.55      SOME status => status
    3.56    | NONE => General
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
     4.3 @@ -172,7 +172,7 @@
     4.4    get_prover ctxt mode name params minimize_command problem
     4.5    |> minimize ctxt mode name params problem
     4.6  
     4.7 -fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
     4.8 +fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
     4.9    | is_induction_fact _ = false
    4.10  
    4.11  fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,