encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
authorblanchet
Thu Aug 19 18:16:47 2010 +0200 (2010-08-19)
changeset 386063003ddbd46d9
parent 38605 970ee38495e4
child 38607 a2abe8c2a1c2
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Aug 19 14:39:31 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Aug 19 18:16:47 2010 +0200
     1.3 @@ -31,28 +31,31 @@
     1.4  [no_atp]: "skolem_id = (\<lambda>x. x)"
     1.5  
     1.6  definition COMBI :: "'a \<Rightarrow> 'a" where
     1.7 -[no_atp]: "COMBI P \<equiv> P"
     1.8 +[no_atp]: "COMBI P = P"
     1.9  
    1.10  definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    1.11 -[no_atp]: "COMBK P Q \<equiv> P"
    1.12 +[no_atp]: "COMBK P Q = P"
    1.13  
    1.14  definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    1.15 -"COMBB P Q R \<equiv> P (Q R)"
    1.16 +"COMBB P Q R = P (Q R)"
    1.17  
    1.18  definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.19 -[no_atp]: "COMBC P Q R \<equiv> P R Q"
    1.20 +[no_atp]: "COMBC P Q R = P R Q"
    1.21  
    1.22  definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.23 -[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
    1.24 +[no_atp]: "COMBS P Q R = P R (Q R)"
    1.25  
    1.26  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.27 -"fequal X Y \<equiv> (X = Y)"
    1.28 +"fequal X Y \<longleftrightarrow> (X = Y)"
    1.29 +
    1.30 +lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    1.31 +by (simp add: fequal_def)
    1.32  
    1.33 -lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
    1.34 -  by (simp add: fequal_def)
    1.35 +lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    1.36 +by (simp add: fequal_def)
    1.37  
    1.38 -lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
    1.39 -  by (simp add: fequal_def)
    1.40 +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    1.41 +by auto
    1.42  
    1.43  text{*Theorems for translation to combinators*}
    1.44  
     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 14:39:31 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 18:16:47 2010 +0200
     2.3 @@ -66,8 +66,10 @@
     2.4  (* HOL to FOL  (Isabelle to Metis)                                           *)
     2.5  (* ------------------------------------------------------------------------- *)
     2.6  
     2.7 -fun fn_isa_to_met "equal" = "="
     2.8 -  | fn_isa_to_met x       = x;
     2.9 +fun fn_isa_to_met_sublevel "equal" = "c_fequal"
    2.10 +  | fn_isa_to_met_sublevel x = x
    2.11 +fun fn_isa_to_met_toplevel "equal" = "="
    2.12 +  | fn_isa_to_met_toplevel x = x
    2.13  
    2.14  fun metis_lit b c args = (b, (c, args));
    2.15  
    2.16 @@ -89,7 +91,7 @@
    2.17      | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
    2.18  
    2.19  fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    2.20 -      Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
    2.21 +      Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
    2.22    | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    2.23    | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    2.24         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    2.25 @@ -99,7 +101,7 @@
    2.26  
    2.27  fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
    2.28    | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
    2.29 -      wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
    2.30 +      wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty)
    2.31    | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
    2.32         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
    2.33                    combtyp_of tm)
    2.34 @@ -108,7 +110,7 @@
    2.35        let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
    2.36            val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
    2.37            val lits = map hol_term_to_fol_FO tms
    2.38 -      in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
    2.39 +      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
    2.40    | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
    2.41       (case strip_combterm_comb tm of
    2.42            (CombConst(("equal", _), _, _), tms) =>
    2.43 @@ -224,13 +226,16 @@
    2.44  
    2.45  fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
    2.46  
    2.47 +fun smart_invert_const "fequal" = @{const_name "op ="}
    2.48 +  | smart_invert_const s = invert_const s
    2.49 +
    2.50  fun hol_type_from_metis_term _ (Metis.Term.Var v) =
    2.51       (case strip_prefix_and_undo_ascii tvar_prefix v of
    2.52            SOME w => make_tvar w
    2.53          | NONE   => make_tvar v)
    2.54    | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
    2.55       (case strip_prefix_and_undo_ascii type_const_prefix x of
    2.56 -          SOME tc => Term.Type (invert_const tc,
    2.57 +          SOME tc => Term.Type (smart_invert_const tc,
    2.58                                  map (hol_type_from_metis_term ctxt) tys)
    2.59          | NONE    =>
    2.60        case strip_prefix_and_undo_ascii tfree_prefix x of
    2.61 @@ -265,7 +270,7 @@
    2.62          | applic_to_tt (a,ts) =
    2.63              case strip_prefix_and_undo_ascii const_prefix a of
    2.64                  SOME b =>
    2.65 -                  let val c = invert_const b
    2.66 +                  let val c = smart_invert_const b
    2.67                        val ntypes = num_type_args thy c
    2.68                        val nterms = length ts - ntypes
    2.69                        val tts = map tm_to_tt ts
    2.70 @@ -283,7 +288,7 @@
    2.71                | NONE => (*Not a constant. Is it a type constructor?*)
    2.72              case strip_prefix_and_undo_ascii type_const_prefix a of
    2.73                  SOME b =>
    2.74 -                  Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
    2.75 +                  Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
    2.76                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
    2.77              case strip_prefix_and_undo_ascii tfree_prefix a of
    2.78                  SOME b => Type (mk_tfree ctxt b)
    2.79 @@ -311,7 +316,7 @@
    2.80              Const ("op =", HOLogic.typeT)
    2.81          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
    2.82             (case strip_prefix_and_undo_ascii const_prefix x of
    2.83 -                SOME c => Const (invert_const c, dummyT)
    2.84 +                SOME c => Const (smart_invert_const c, dummyT)
    2.85                | NONE => (*Not a constant. Is it a fixed variable??*)
    2.86              case strip_prefix_and_undo_ascii fixed_var_prefix x of
    2.87                  SOME v => Free (v, hol_type_from_metis_term ctxt ty)
    2.88 @@ -325,7 +330,7 @@
    2.89              list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
    2.90          | cvt (t as Metis.Term.Fn (x, [])) =
    2.91             (case strip_prefix_and_undo_ascii const_prefix x of
    2.92 -                SOME c => Const (invert_const c, dummyT)
    2.93 +                SOME c => Const (smart_invert_const c, dummyT)
    2.94                | NONE => (*Not a constant. Is it a fixed variable??*)
    2.95              case strip_prefix_and_undo_ascii fixed_var_prefix x of
    2.96                  SOME v => Free (v, dummyT)
    2.97 @@ -598,9 +603,6 @@
    2.98  (* Translation of HO Clauses                                                 *)
    2.99  (* ------------------------------------------------------------------------- *)
   2.100  
   2.101 -fun cnf_helper_theorem thy raw th =
   2.102 -  if raw then th else the_single (Clausifier.cnf_axiom thy th)
   2.103 -
   2.104  fun type_ext thy tms =
   2.105    let val subs = tfree_classes_of_terms tms
   2.106        val supers = tvar_classes_of_terms tms
   2.107 @@ -650,15 +652,16 @@
   2.108    | string_of_mode FT = "FT"
   2.109  
   2.110  val helpers =
   2.111 -  [("c_COMBI", (false, @{thms COMBI_def})),
   2.112 -   ("c_COMBK", (false, @{thms COMBK_def})),
   2.113 -   ("c_COMBB", (false, @{thms COMBB_def})),
   2.114 -   ("c_COMBC", (false, @{thms COMBC_def})),
   2.115 -   ("c_COMBS", (false, @{thms COMBS_def})),
   2.116 -   ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
   2.117 -   ("c_True", (true, @{thms True_or_False})),
   2.118 -   ("c_False", (true, @{thms True_or_False})),
   2.119 -   ("c_If", (true, @{thms if_True if_False True_or_False}))]
   2.120 +  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
   2.121 +   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
   2.122 +   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
   2.123 +   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
   2.124 +   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
   2.125 +   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
   2.126 +                            @{thms fequal_imp_equal equal_imp_fequal})),
   2.127 +   ("c_True", (true, map (`I) @{thms True_or_False})),
   2.128 +   ("c_False", (true, map (`I) @{thms True_or_False})),
   2.129 +   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
   2.130  
   2.131  fun is_quasi_fol_clause thy =
   2.132    Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
   2.133 @@ -673,18 +676,20 @@
   2.134          | set_mode FT = FT
   2.135        val mode = set_mode mode0
   2.136        (*transform isabelle clause to metis clause *)
   2.137 -      fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
   2.138 +      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
   2.139 +                  : logic_map =
   2.140          let
   2.141            val (mth, tfree_lits, skolems) =
   2.142 -            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
   2.143 +            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
   2.144 +                           metis_ith
   2.145          in
   2.146 -           {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   2.147 +           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
   2.148              tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
   2.149          end;
   2.150        val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
   2.151 -                 |> fold (add_thm true) cls
   2.152 +                 |> fold (add_thm true o `I) cls
   2.153                   |> add_tfrees
   2.154 -                 |> fold (add_thm false) ths
   2.155 +                 |> fold (add_thm false o `I) ths
   2.156        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   2.157        fun is_used c =
   2.158          exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   2.159 @@ -695,11 +700,12 @@
   2.160            let
   2.161              val helper_ths =
   2.162                helpers |> filter (is_used o fst)
   2.163 -                      |> maps (fn (_, (raw, thms)) =>
   2.164 -                                  if mode = FT orelse not raw then
   2.165 -                                    map (cnf_helper_theorem @{theory} raw) thms
   2.166 +                      |> maps (fn (c, (needs_full_types, thms)) =>
   2.167 +                                  if not (is_used c) orelse
   2.168 +                                     needs_full_types andalso mode <> FT then
   2.169 +                                    []
   2.170                                    else
   2.171 -                                    [])
   2.172 +                                    thms)
   2.173            in lmap |> fold (add_thm false) helper_ths end
   2.174    in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   2.175  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 19 14:39:31 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 19 18:16:47 2010 +0200
     3.3 @@ -82,9 +82,9 @@
     3.4  
     3.5  (*Pairs a constant with the list of its type instantiations (using const_typ)*)
     3.6  fun const_with_typ thy (c,typ) =
     3.7 -    let val tvars = Sign.const_typargs thy (c,typ)
     3.8 -    in (c, map const_typ_of tvars) end
     3.9 -    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)
    3.10 +  let val tvars = Sign.const_typargs thy (c,typ) in
    3.11 +    (c, map const_typ_of tvars) end
    3.12 +  handle TYPE _ => (c, [])   (*Variable (locale constant): monomorphic*)
    3.13  
    3.14  (*Add a const/type pair to the table, but a [] entry means a standard connective,
    3.15    which we ignore.*)
    3.16 @@ -95,7 +95,8 @@
    3.17  val fresh_prefix = "Sledgehammer.Fresh."
    3.18  val flip = Option.map not
    3.19  (* These are typically simplified away by "Meson.presimplify". *)
    3.20 -val boring_consts = [@{const_name If}, @{const_name Let}]
    3.21 +val boring_consts =
    3.22 +  [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
    3.23  
    3.24  fun get_consts_typs thy pos ts =
    3.25    let
    3.26 @@ -104,9 +105,8 @@
    3.27         introduce a fresh constant to simulate the effect of Skolemization. *)
    3.28      fun do_term t =
    3.29        case t of
    3.30 -        Const (@{const_name Let}, _) => I
    3.31 -      | Const x => add_const_type_to_table (const_with_typ thy x)
    3.32 -      | Free x => add_const_type_to_table (const_with_typ thy x)
    3.33 +        Const x => add_const_type_to_table (const_with_typ thy x)
    3.34 +      | Free (s, _) => add_const_type_to_table (s, [])
    3.35        | t1 $ t2 => do_term t1 #> do_term t2
    3.36        | Abs (_, _, t) =>
    3.37          (* Abstractions lead to combinators, so we add a penalty for them. *)
    3.38 @@ -198,7 +198,7 @@
    3.39  fun count_axiom_consts theory_relevant thy (_, th) =
    3.40    let
    3.41      fun do_const (a, T) =
    3.42 -      let val (c, cts) = const_with_typ thy (a,T) in
    3.43 +      let val (c, cts) = const_with_typ thy (a, T) in
    3.44          (* Two-dimensional table update. Constant maps to types maps to
    3.45             count. *)
    3.46          CTtab.map_default (cts, 0) (Integer.add 1)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 14:39:31 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 18:16:47 2010 +0200
     4.3 @@ -209,7 +209,7 @@
     4.4  val optional_typed_helpers =
     4.5    [(["c_True", "c_False"], @{thms True_or_False}),
     4.6     (["c_If"], @{thms if_True if_False True_or_False})]
     4.7 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
     4.8 +val mandatory_helpers = @{thms fequal_def}
     4.9  
    4.10  val init_counters =
    4.11    Symtab.make (maps (maps (map (rpair 0) o fst))
     5.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 19 14:39:31 2010 +0200
     5.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 19 18:16:47 2010 +0200
     5.3 @@ -527,7 +527,8 @@
     5.4    which are needed to avoid the various one-point theorems from generating junk clauses.*)
     5.5  val nnf_simps =
     5.6    @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
     5.7 -         if_eq_cancel cases_simp}
     5.8 +         if_eq_cancel cases_simp (* TODO: mem_def_raw Collect_def_raw *)}
     5.9 +(* TODO:  @ [@{lemma "{} = (%x. False)" by (rule ext) auto}] *)
    5.10  val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
    5.11  
    5.12  val nnf_ss =
    5.13 @@ -539,8 +540,7 @@
    5.14    #> simplify nnf_ss
    5.15  
    5.16  fun make_nnf ctxt th = case prems_of th of
    5.17 -    [] => th |> presimplify
    5.18 -             |> make_nnf1 ctxt
    5.19 +    [] => th |> presimplify |> make_nnf1 ctxt
    5.20    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    5.21  
    5.22  (*Pull existential quantifiers to front. This accomplishes Skolemization for