improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
authorblanchet
Wed Dec 15 11:26:28 2010 +0100 (2010-12-15)
changeset 41145a5ee3b8e5a90
parent 41144 509e51b7509a
child 41146 be78f4053bce
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
src/HOL/Metis_Examples/HO_Reas.thy
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     1.1 --- a/src/HOL/Metis_Examples/HO_Reas.thy	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Metis_Examples/HO_Reas.thy	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -12,67 +12,98 @@
     1.4  
     1.5  lemma "id True"
     1.6  sledgehammer [expect = some] (id_apply)
     1.7 +sledgehammer [type_sys = tags, expect = some] (id_apply)
     1.8 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
     1.9  by (metis id_apply)
    1.10  
    1.11  lemma "\<not> id False"
    1.12  sledgehammer [expect = some] (id_apply)
    1.13 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.14 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.15  by (metis id_apply)
    1.16  
    1.17  lemma "x = id True \<or> x = id False"
    1.18  sledgehammer [expect = some] (id_apply)
    1.19 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.20 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.21  by (metis id_apply)
    1.22  
    1.23  lemma "id x = id True \<or> id x = id False"
    1.24  sledgehammer [expect = some] (id_apply)
    1.25 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.26 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.27  by (metis id_apply)
    1.28  
    1.29  lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
    1.30  sledgehammer [expect = none] ()
    1.31 -sledgehammer [full_types, expect = some] ()
    1.32 +sledgehammer [type_sys = tags, expect = some] ()
    1.33 +sledgehammer [full_types, type_sys = tags, expect = some] ()
    1.34  by metisFT
    1.35  
    1.36  lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
    1.37  sledgehammer [expect = some] (id_apply)
    1.38 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.39 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.40  by (metis id_apply)
    1.41  
    1.42  lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
    1.43  sledgehammer [expect = some] ()
    1.44 +sledgehammer [type_sys = tags, expect = some] ()
    1.45 +sledgehammer [full_types, type_sys = tags, expect = some] ()
    1.46  by metis
    1.47  
    1.48  lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
    1.49  sledgehammer [expect = some] (id_apply)
    1.50 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.51 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.52  by (metis id_apply)
    1.53  
    1.54  lemma "id (a \<and> b) \<Longrightarrow> id a"
    1.55  sledgehammer [expect = some] (id_apply)
    1.56 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.57 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.58  by (metis id_apply)
    1.59  
    1.60  lemma "id (a \<and> b) \<Longrightarrow> id b"
    1.61  sledgehammer [expect = some] (id_apply)
    1.62 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.63 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.64  by (metis id_apply)
    1.65  
    1.66  lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
    1.67  sledgehammer [expect = some] (id_apply)
    1.68 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.69 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.70  by (metis id_apply)
    1.71  
    1.72  lemma "id a \<Longrightarrow> id (a \<or> b)"
    1.73  sledgehammer [expect = some] (id_apply)
    1.74 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.75 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.76  by (metis id_apply)
    1.77  
    1.78  lemma "id b \<Longrightarrow> id (a \<or> b)"
    1.79  sledgehammer [expect = some] (id_apply)
    1.80 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.81 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.82  by (metis id_apply)
    1.83  
    1.84  lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
    1.85  sledgehammer [expect = some] (id_apply)
    1.86 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.87 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.88  by (metis id_apply)
    1.89  
    1.90  lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
    1.91  sledgehammer [expect = some] (id_apply)
    1.92 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.93 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
    1.94  by (metis id_apply)
    1.95  
    1.96  lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
    1.97  sledgehammer [expect = some] (id_apply)
    1.98 +sledgehammer [type_sys = tags, expect = some] (id_apply)
    1.99 +sledgehammer [full_types, type_sys = tags, expect = some] (id_apply)
   1.100  by (metis id_apply)
   1.101  
   1.102  end
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     2.3 @@ -95,6 +95,20 @@
     2.4    | mk_ahorn (phi :: phis) psi =
     2.5      AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
     2.6  
     2.7 +fun close_universally phi =
     2.8 +  let
     2.9 +    fun term_vars bounds (ATerm (name as (s, _), tms)) =
    2.10 +        (is_atp_variable s andalso not (member (op =) bounds name))
    2.11 +          ? insert (op =) name
    2.12 +        #> fold (term_vars bounds) tms
    2.13 +    fun formula_vars bounds (AQuant (_, xs, phi)) =
    2.14 +        formula_vars (xs @ bounds) phi
    2.15 +      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
    2.16 +      | formula_vars bounds (AAtom tm) = term_vars bounds tm
    2.17 +  in
    2.18 +    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
    2.19 +  end
    2.20 +
    2.21  fun combformula_for_prop thy eq_as_iff =
    2.22    let
    2.23      fun do_term bs t ts =
    2.24 @@ -264,7 +278,7 @@
    2.25    metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
    2.26    |> Symtab.make
    2.27  
    2.28 -fun get_helper_facts ctxt type_sys formulas =
    2.29 +fun get_helper_facts ctxt explicit_forall type_sys formulas =
    2.30    let
    2.31      val no_dangerous_types = types_dangerous_types type_sys
    2.32      val ct = init_counters |> fold count_formula formulas
    2.33 @@ -274,15 +288,26 @@
    2.34          false), th)
    2.35      fun make_facts eq_as_iff = map_filter (make_fact ctxt eq_as_iff false)
    2.36    in
    2.37 -    metis_helpers
    2.38 -    |> filter (is_used o fst)
    2.39 -    |> maps (fn (c, (needs_full_types, ths)) =>
    2.40 -                if needs_full_types andalso not no_dangerous_types then
    2.41 -                  []
    2.42 -                else
    2.43 -                  ths ~~ (1 upto length ths)
    2.44 -                  |> map (dub c needs_full_types)
    2.45 -                  |> make_facts (not needs_full_types))
    2.46 +    (metis_helpers
    2.47 +     |> filter (is_used o fst)
    2.48 +     |> maps (fn (c, (needs_full_types, ths)) =>
    2.49 +                 if needs_full_types andalso not no_dangerous_types then
    2.50 +                   []
    2.51 +                 else
    2.52 +                   ths ~~ (1 upto length ths)
    2.53 +                   |> map (dub c needs_full_types)
    2.54 +                   |> make_facts (not needs_full_types)),
    2.55 +     if type_sys = Tags false then
    2.56 +       let
    2.57 +         fun var s = ATerm (`I s, [])
    2.58 +         fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
    2.59 +       in
    2.60 +         [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
    2.61 +               AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
    2.62 +               |> explicit_forall ? close_universally)]
    2.63 +       end
    2.64 +     else
    2.65 +       [])
    2.66    end
    2.67  
    2.68  fun translate_atp_fact ctxt = `(make_fact ctxt true true)
    2.69 @@ -571,20 +596,6 @@
    2.70    else
    2.71      t |> not (is_predicate pred_const_tab s) ? boolify
    2.72  
    2.73 -fun close_universally phi =
    2.74 -  let
    2.75 -    fun term_vars bounds (ATerm (name as (s, _), tms)) =
    2.76 -        (is_atp_variable s andalso not (member (op =) bounds name))
    2.77 -          ? insert (op =) name
    2.78 -        #> fold (term_vars bounds) tms
    2.79 -    fun formula_vars bounds (AQuant (_, xs, phi)) =
    2.80 -        formula_vars (xs @ bounds) phi
    2.81 -      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
    2.82 -      | formula_vars bounds (AAtom tm) = term_vars bounds tm
    2.83 -  in
    2.84 -    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
    2.85 -  end
    2.86 -
    2.87  fun repair_formula thy explicit_forall type_sys const_tab =
    2.88    let
    2.89      val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab
    2.90 @@ -627,12 +638,14 @@
    2.91      val const_tab = const_table_for_problem explicit_apply problem
    2.92      val problem =
    2.93        problem |> repair_problem thy explicit_forall type_sys const_tab
    2.94 -    val helper_facts =
    2.95 -      get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
    2.96 +    val (helper_facts, raw_helper_lines) =
    2.97 +      get_helper_facts ctxt explicit_forall type_sys
    2.98 +                       (maps (map (#3 o dest_Fof) o snd) problem)
    2.99      val helper_lines =
   2.100 -      helper_facts
   2.101 -      |> map (problem_line_for_fact ctxt helper_prefix type_sys
   2.102 -              #> repair_problem_line thy explicit_forall type_sys const_tab)
   2.103 +      (helper_facts
   2.104 +       |> map (problem_line_for_fact ctxt helper_prefix type_sys
   2.105 +               #> repair_problem_line thy explicit_forall type_sys const_tab)) @
   2.106 +      raw_helper_lines
   2.107      val (problem, pool) =
   2.108        problem |> AList.update (op =) ("Helper facts", helper_lines)
   2.109                |> nice_atp_problem readable_names