author blanchet Thu Aug 19 18:16:47 2010 +0200 (2010-08-19) changeset 38606 3003ddbd46d9 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
```     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.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.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.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
```