src/HOL/Tools/res_axioms.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29579 cb520b766e00
child 30280 eb98b49ef835
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     2
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
     3
Transformation of axiom rules (elim/intro/etc) into CNF forms.
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     4
*)
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     5
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
     6
signature RES_AXIOMS =
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
     7
sig
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
     8
  val cnf_axiom: theory -> thm -> thm list
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
     9
  val pairname: thm -> string * thm
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
    10
  val multi_base_blacklist: string list
25243
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
    11
  val bad_for_atp: thm -> bool
25761
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
    12
  val type_has_empty_sort: typ -> bool
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
    13
  val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    14
  val neg_clausify: thm list -> thm list
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    15
  val expand_defs_tac: thm -> tactic
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
    16
  val combinators: thm -> thm
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
    17
  val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
    18
  val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
    19
  val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
    20
  val atpset_rules_of: Proof.context -> (string * thm) list
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
    21
  val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    22
  val setup: theory -> theory
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
    23
end;
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
    24
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    25
structure ResAxioms: RES_AXIOMS =
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    26
struct
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    27
20902
a0034e545c13 replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
wenzelm
parents: 20867
diff changeset
    28
(* FIXME legacy *)
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
    29
fun freeze_thm th = #1 (Drule.freeze_thaw th);
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
    30
25761
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
    31
fun type_has_empty_sort (TFree (_, [])) = true
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
    32
  | type_has_empty_sort (TVar (_, [])) = true
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
    33
  | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
    34
  | type_has_empty_sort _ = false;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
    35
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
    36
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    37
(**** Transformation of Elimination Rules into First-Order Formulas****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    38
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    39
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    40
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    41
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    42
(*Converts an elim-rule into an equivalent theorem that does not have the
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    43
  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    44
  conclusion variable to False.*)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    45
fun transform_elim th =
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    46
  case concl_of th of    (*conclusion variable*)
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    47
       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    48
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
    49
    | v as Var(_, Type("prop",[])) =>
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    50
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    51
    | _ => th;
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    52
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    53
(*To enforce single-threading*)
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    54
exception Clausify_failure of theory;
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    55
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
    56
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    57
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    58
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    59
fun rhs_extra_types lhsT rhs =
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    60
  let val lhs_vars = Term.add_tfreesT lhsT []
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    61
      fun add_new_TFrees (TFree v) =
24821
cc55041ca8ba skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents: 24785
diff changeset
    62
            if member (op =) lhs_vars v then I else insert (op =) (TFree v)
cc55041ca8ba skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents: 24785
diff changeset
    63
        | add_new_TFrees _ = I
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    64
      val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    65
  in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    66
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
    67
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
27174
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    68
  prefix for the Skolem constant.*)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    69
fun declare_skofuns s th =
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    70
  let
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    71
    val nref = ref 0
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    72
    fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    73
          (*Existential: declare a Skolem function, then insert into body and continue*)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    74
          let
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    75
            val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
    76
            val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
27174
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    77
            val Ts = map type_of args0
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    78
            val extraTs = rhs_extra_types (Ts ---> T) xtp
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    79
            val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    80
            val args = argsx @ args0
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    81
            val cT = extraTs ---> Ts ---> T
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    82
            val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    83
                    (*Forms a lambda-abstraction over the formal parameters*)
28110
9d121b171a0a Sign.declare_const: Name.binding;
wenzelm
parents: 27865
diff changeset
    84
            val (c, thy') =
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28674
diff changeset
    85
              Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
27174
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    86
            val cdef = cname ^ "_def"
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29368
diff changeset
    87
            val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28674
diff changeset
    88
            val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
27174
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    89
          in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    90
      | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    91
          (*Universal quant: insert a free variable into body and continue*)
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
    92
          let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
27174
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    93
          in dec_sko (subst_bound (Free (fname, T), p)) thx end
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    94
      | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    95
      | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    96
      | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    97
      | dec_sko t thx = thx (*Do nothing otherwise*)
c2c484480f40 declare_skofuns/skolem: canonical argument order;
wenzelm
parents: 26939
diff changeset
    98
  in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
    99
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   100
(*Traverse a theorem, accumulating Skolem function definitions.*)
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   101
fun assume_skofuns s th =
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   102
  let val sko_count = ref 0
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   103
      fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   104
            (*Existential: declare a Skolem function, then insert into body and continue*)
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   105
            let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   106
                val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   107
                val Ts = map type_of args
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   108
                val cT = Ts ---> T
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   109
                val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   110
                val c = Free (id, cT)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   111
                val rhs = list_abs_free (map dest_Free args,
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   112
                                         HOLogic.choice_const T $ xtp)
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   113
                      (*Forms a lambda-abstraction over the formal parameters*)
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27194
diff changeset
   114
                val def = Logic.mk_equals (c, rhs)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   115
            in dec_sko (subst_bound (list_comb(c,args), p))
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   116
                       (def :: defs)
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   117
            end
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   118
        | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   119
            (*Universal quant: insert a free variable into body and continue*)
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   120
            let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   121
            in dec_sko (subst_bound (Free(fname,T), p)) defs end
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   122
        | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   123
        | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   124
        | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   125
        | dec_sko t defs = defs (*Do nothing otherwise*)
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   126
  in  dec_sko (prop_of th) []  end;
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   127
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   128
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   129
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   130
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   131
(*Returns the vars of a theorem*)
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   132
fun vars_of_thm th =
22691
290454649b8c Thm.fold_terms;
wenzelm
parents: 22644
diff changeset
   133
  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   134
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   135
(*Make a version of fun_cong with a given variable name*)
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   136
local
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   137
    val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   138
    val cx = hd (vars_of_thm fun_cong');
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   139
    val ty = typ_of (ctyp_of_term cx);
20445
b222d9939e00 improvements to abstraction generation
paulson
parents: 20421
diff changeset
   140
    val thy = theory_of_thm fun_cong;
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   141
    fun mkvar a = cterm_of thy (Var((a,0),ty));
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   142
in
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   143
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   144
end;
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   145
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   146
(*Removes the lambdas from an equation of the form t = (%x. u).  A non-negative n,
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   147
  serves as an upper bound on how many to remove.*)
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   148
fun strip_lambdas 0 th = th
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   149
  | strip_lambdas n th =
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   150
      case prop_of th of
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   151
          _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   152
              strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   153
        | _ => th;
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   154
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   155
val lambda_free = not o Term.has_abs;
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   156
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   157
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   158
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   159
val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   160
val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   161
val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   162
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   163
(*FIXME: requires more use of cterm constructors*)
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   164
fun abstract ct =
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   165
  let
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   166
      val thy = theory_of_cterm ct
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   167
      val Abs(x,_,body) = term_of ct
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   168
      val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   169
      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   170
      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   171
  in
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   172
      case body of
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   173
          Const _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   174
        | Free _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   175
        | Var _ => makeK()  (*though Var isn't expected*)
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   176
        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   177
        | rator$rand =>
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   178
            if loose_bvar1 (rator,0) then (*C or S*)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   179
               if loose_bvar1 (rand,0) then (*S*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   180
                 let val crator = cterm_of thy (Abs(x,xT,rator))
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   181
                     val crand = cterm_of thy (Abs(x,xT,rand))
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   182
                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   183
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   184
                 in
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   185
                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   186
                 end
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   187
               else (*C*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   188
                 let val crator = cterm_of thy (Abs(x,xT,rator))
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   189
                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   190
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   191
                 in
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   192
                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   193
                 end
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   194
            else if loose_bvar1 (rand,0) then (*B or eta*)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   195
               if rand = Bound 0 then eta_conversion ct
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   196
               else (*B*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   197
                 let val crand = cterm_of thy (Abs(x,xT,rand))
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   198
                     val crator = cterm_of thy rator
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   199
                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   200
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   201
                 in
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   202
                   Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   203
                 end
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   204
            else makeK()
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   205
        | _ => error "abstract: Bad term"
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   206
  end;
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   207
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
   208
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   209
  prefix for the constants.*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   210
fun combinators_aux ct =
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   211
  if lambda_free (term_of ct) then reflexive ct
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   212
  else
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   213
  case term_of ct of
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   214
      Abs _ =>
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   215
        let val (cv,cta) = Thm.dest_abs NONE ct
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   216
            val (v,Tv) = (dest_Free o term_of) cv
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   217
            val u_th = combinators_aux cta
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   218
            val cu = Thm.rhs_of u_th
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   219
            val comb_eq = abstract (Thm.cabs cv cu)
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   220
        in transitive (abstract_rule v cv u_th) comb_eq end
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   221
    | t1 $ t2 =>
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   222
        let val (ct1,ct2) = Thm.dest_comb ct
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   223
        in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   224
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   225
fun combinators th =
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   226
  if lambda_free (prop_of th) then th
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   227
  else
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   228
    let val th = Drule.eta_contraction_rule th
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   229
        val eqth = combinators_aux (cprop_of th)
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   230
    in  equal_elim eqth th   end
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   231
    handle THM (msg,_,_) =>
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26653
diff changeset
   232
      (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   233
       warning ("  Exception message: " ^ msg);
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   234
       TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   235
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   236
(*cterms are used throughout for efficiency*)
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
   237
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   238
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   239
(*cterm version of mk_cTrueprop*)
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   240
fun c_mkTrueprop A = Thm.capply cTrueprop A;
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   241
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   242
(*Given an abstraction over n variables, replace the bound variables by free
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   243
  ones. Return the body, along with the list of free variables.*)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   244
fun c_variant_abs_multi (ct0, vars) =
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   245
      let val (cv,ct) = Thm.dest_abs NONE ct0
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   246
      in  c_variant_abs_multi (ct, cv::vars)  end
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   247
      handle CTERM _ => (ct0, rev vars);
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   248
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   249
(*Given the definition of a Skolem function, return a theorem to replace
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   250
  an existential formula by a use of that function.
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   251
   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   252
fun skolem_of_def def =
22902
ac833b4bb7ee moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents: 22846
diff changeset
   253
  let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   254
      val (ch, frees) = c_variant_abs_multi (rhs, [])
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   255
      val (chilbert,cabs) = Thm.dest_comb ch
26627
dac6d56b7c8d rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 26618
diff changeset
   256
      val thy = Thm.theory_of_cterm chilbert
dac6d56b7c8d rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 26618
diff changeset
   257
      val t = Thm.term_of chilbert
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   258
      val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   259
                      | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
22596
d0d2af4db18f rep_thm/cterm/ctyp: removed obsolete sign field;
wenzelm
parents: 22516
diff changeset
   260
      val cex = Thm.cterm_of thy (HOLogic.exists_const T)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   261
      val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   262
      and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   263
      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
23352
356edb5eb1c4 renamed Goal.prove_raw to Goal.prove_internal;
wenzelm
parents: 22902
diff changeset
   264
  in  Goal.prove_internal [ex_tm] conc tacf
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   265
       |> forall_intr_list frees
26653
60e0cf6bef89 Thm.forall_elim_var(s);
wenzelm
parents: 26627
diff changeset
   266
       |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   267
       |> Thm.varifyT
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   268
  end;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   269
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   270
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   271
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   272
fun to_nnf th ctxt0 =
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   273
  let val th1 = th |> transform_elim |> zero_var_indexes
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   274
      val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   275
      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   276
  in  (th3, ctxt)  end;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   277
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   278
(*Generate Skolem functions for a theorem supplied in nnf*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   279
fun assume_skolem_of_def s th =
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   280
  map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   281
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   282
fun assert_lambda_free ths msg =
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   283
  case filter (not o lambda_free o prop_of) ths of
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   284
      [] => ()
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26653
diff changeset
   285
    | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20445
diff changeset
   286
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   287
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   288
(*** Blacklisting (duplicated in ResAtp?) ***)
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   289
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   290
val max_lambda_nesting = 3;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   291
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   292
fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   293
  | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   294
  | excessive_lambdas _ = false;
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   295
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   296
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   297
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   298
(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   299
fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   300
  | excessive_lambdas_fm Ts t =
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   301
      if is_formula_type (fastype_of1 (Ts, t))
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   302
      then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   303
      else excessive_lambdas (t, max_lambda_nesting);
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   304
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   305
(*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*)
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   306
val max_apply_depth = 15;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   307
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   308
fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1)
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   309
  | apply_depth (Abs(_,_,t)) = apply_depth t
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   310
  | apply_depth _ = 0;
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   311
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   312
fun too_complex t =
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   313
  apply_depth t > max_apply_depth orelse
26562
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 25761
diff changeset
   314
  Meson.too_many_clauses NONE t orelse
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   315
  excessive_lambdas_fm [] t;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   316
25243
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   317
fun is_strange_thm th =
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   318
  case head_of (concl_of th) of
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   319
      Const (a,_) => (a <> "Trueprop" andalso a <> "==")
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   320
    | _ => false;
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   321
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   322
fun bad_for_atp th =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27809
diff changeset
   323
  Thm.is_internal th
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   324
  orelse too_complex (prop_of th)
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   325
  orelse exists_type type_has_empty_sort (prop_of th)
25761
466e714de2fc testing for empty sort
paulson
parents: 25256
diff changeset
   326
  orelse is_strange_thm th;
25243
78f8aaa27493 bugfixes concerning strange theorems
paulson
parents: 25007
diff changeset
   327
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   328
val multi_base_blacklist =
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   329
  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   330
   "cases","ext_cases"];  (*FIXME: put other record thms here, or use the "Internal" marker*)
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   331
21071
8d0245c5ed9e Fixed the "exception Empty" bug in elim2Fol
paulson
parents: 20996
diff changeset
   332
(*Keep the full complexity of the original name*)
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21646
diff changeset
   333
fun flatten_name s = space_implode "_X" (NameSpace.explode s);
21071
8d0245c5ed9e Fixed the "exception Empty" bug in elim2Fol
paulson
parents: 20996
diff changeset
   334
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   335
fun fake_name th =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27809
diff changeset
   336
  if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   337
  else gensym "unknown_thm_";
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   338
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   339
fun name_or_string th =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27809
diff changeset
   340
  if Thm.has_name_hint th then Thm.get_name_hint th
26928
ca87aff1ad2d structure Display: less pervasive operations;
wenzelm
parents: 26653
diff changeset
   341
  else Display.string_of_thm th;
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   342
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   343
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   344
fun skolem_thm (s, th) =
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   345
  if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then []
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   346
  else
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   347
    let
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   348
      val ctxt0 = Variable.thm_context th
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   349
      val (nnfth, ctxt1) = to_nnf th ctxt0
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   350
      val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   351
    in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   352
    handle THM _ => [];
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   353
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   354
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   355
  Skolem functions.*)
22516
c986140356b8 Clause cache is now in theory data.
paulson
parents: 22471
diff changeset
   356
structure ThmCache = TheoryDataFun
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22731
diff changeset
   357
(
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   358
  type T = thm list Thmtab.table * unit Symtab.table;
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   359
  val empty = (Thmtab.empty, Symtab.empty);
26618
wenzelm
parents: 26562
diff changeset
   360
  val copy = I;
wenzelm
parents: 26562
diff changeset
   361
  val extend = I;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   362
  fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   363
    (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22731
diff changeset
   364
);
22516
c986140356b8 Clause cache is now in theory data.
paulson
parents: 22471
diff changeset
   365
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   366
val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   367
val already_seen = Symtab.defined o #2 o ThmCache.get;
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   368
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   369
val update_cache = ThmCache.map o apfst o Thmtab.update;
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   370
fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
25007
cd497f6fe8d1 trying to make it run faster
paulson
parents: 24959
diff changeset
   371
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   372
(*Exported function to convert Isabelle theorems into axiom clauses*)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   373
fun cnf_axiom thy th0 =
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   374
  let val th = Thm.transfer thy th0 in
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   375
    case lookup_cache thy th of
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   376
      NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   377
    | SOME cls => cls
22516
c986140356b8 Clause cache is now in theory data.
paulson
parents: 22471
diff changeset
   378
  end;
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   379
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   380
15872
8336ff711d80 fixed treatment of higher-order simprules
paulson
parents: 15736
diff changeset
   381
(**** Extract and Clausify theorems from a theory's claset and simpset ****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   382
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27809
diff changeset
   383
fun pairname th = (Thm.get_name_hint th, th);
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   384
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   385
fun rules_of_claset cs =
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   386
  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
19175
c6e4b073f6a5 subset_refl now included using the atp attribute
paulson
parents: 19113
diff changeset
   387
      val intros = safeIs @ hazIs
18532
0347c1bba406 elim rules: Classical.classical_rule;
wenzelm
parents: 18510
diff changeset
   388
      val elims  = map Classical.classical_rule (safeEs @ hazEs)
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   389
  in map pairname (intros @ elims) end;
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   390
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   391
fun rules_of_simpset ss =
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   392
  let val ({rules,...}, _) = rep_ss ss
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   393
      val simps = Net.entries rules
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   394
  in map (fn r => (#name r, #thm r)) simps end;
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17412
diff changeset
   395
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
   396
fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
   397
fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
   398
24042
968f42fe6836 simplified ResAtpset via NamedThmsFun;
wenzelm
parents: 23592
diff changeset
   399
fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
20774
8f947ffb5eb8 ResAtpset.get_atpset;
wenzelm
parents: 20710
diff changeset
   400
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   401
22471
7c51f1a799f3 Removal of axiom names from the theorem cache
paulson
parents: 22360
diff changeset
   402
(**** Translate a set of theorems into CNF ****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   403
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19630
diff changeset
   404
fun pair_name_cls k (n, []) = []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19630
diff changeset
   405
  | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   406
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   407
fun cnf_rules_pairs_aux _ pairs [] = pairs
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   408
  | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   409
      let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   410
                       handle THM _ => pairs | ResClause.CLAUSE _ => pairs
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   411
      in  cnf_rules_pairs_aux thy pairs' ths  end;
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   412
21290
33b6bb5d6ab8 Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents: 21254
diff changeset
   413
(*The combination of rev and tail recursion preserves the original order*)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   414
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
19353
36b6b15ee670 added another function for CNF.
mengj
parents: 19232
diff changeset
   415
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
   416
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   417
(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   418
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   419
local
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   420
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   421
fun skolem_def (name, th) thy =
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   422
  let val ctxt0 = Variable.thm_context th in
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   423
    (case try (to_nnf th) ctxt0 of
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   424
      NONE => (NONE, thy)
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   425
    | SOME (nnfth, ctxt1) =>
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   426
        let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   427
        in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end)
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   428
  end;
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   429
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   430
fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) =
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   431
  let
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   432
    val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1;
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   433
    val cnfs' = cnfs
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   434
      |> map combinators
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   435
      |> Variable.export ctxt2 ctxt0
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   436
      |> Meson.finish_cnf
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   437
      |> map Thm.close_derivation;
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   438
    in (th, cnfs') end;
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   439
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   440
in
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   441
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   442
fun saturate_skolem_cache thy =
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   443
  let
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   444
    val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   445
      if already_seen thy name then I else cons (name, ths));
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   446
    val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   447
      if member (op =) multi_base_blacklist (Sign.base_name name) then I
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   448
      else fold_index (fn (i, th) =>
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   449
        if bad_for_atp th orelse is_some (lookup_cache thy th) then I
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   450
        else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   451
  in
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   452
    if null new_facts then NONE
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   453
    else
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   454
      let
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   455
        val (defs, thy') = thy
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   456
          |> fold (mark_seen o #1) new_facts
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   457
          |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   458
          |>> map_filter I;
29368
503ce3f8f092 renamed structure ParList to Par_List;
wenzelm
parents: 29270
diff changeset
   459
        val cache_entries = Par_List.map skolem_cnfs defs;
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   460
      in SOME (fold update_cache cache_entries thy') end
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   461
  end;
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   462
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   463
end;
24854
0ebcd575d3c6 filtering out some package theorems
paulson
parents: 24827
diff changeset
   464
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   465
val suppress_endtheory = ref false;
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   466
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   467
fun clause_cache_endtheory thy =
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   468
  if ! suppress_endtheory then NONE
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   469
  else saturate_skolem_cache thy;
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   470
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20445
diff changeset
   471
22516
c986140356b8 Clause cache is now in theory data.
paulson
parents: 22471
diff changeset
   472
(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
c986140356b8 Clause cache is now in theory data.
paulson
parents: 22471
diff changeset
   473
  lambda_free, but then the individual theory caches become much bigger.*)
21071
8d0245c5ed9e Fixed the "exception Empty" bug in elim2Fol
paulson
parents: 20996
diff changeset
   474
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   475
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   476
(*** meson proof methods ***)
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   477
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   478
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   479
fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   480
  | is_absko _ = false;
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   481
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   482
fun is_okdef xs (Const ("==", _) $ t $ u) =   (*Definition of Free, not in certain terms*)
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   483
      is_Free t andalso not (member (op aconv) xs t)
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   484
  | is_okdef _ _ = false
22724
3002683a6e0f Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents: 22691
diff changeset
   485
24215
5458fbf18276 removal of some refs
paulson
parents: 24137
diff changeset
   486
(*This function tries to cope with open locales, which introduce hypotheses of the form
5458fbf18276 removal of some refs
paulson
parents: 24137
diff changeset
   487
  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   488
  of sko_ functions. *)
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   489
fun expand_defs_tac st0 st =
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   490
  let val hyps0 = #hyps (rep_thm st0)
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   491
      val hyps = #hyps (crep_thm st)
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   492
      val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   493
      val defs = filter (is_absko o Thm.term_of) newhyps
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   494
      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   495
                                      (map Thm.term_of hyps)
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   496
      val fixed = OldTerm.term_frees (concl_of st) @
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29579
diff changeset
   497
                  List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   498
  in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
22724
3002683a6e0f Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents: 22691
diff changeset
   499
22731
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   500
abfdccaed085 trying to make single-step proofs work better, especially if they contain
paulson
parents: 22724
diff changeset
   501
fun meson_general_tac ths i st0 =
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   502
  let
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   503
    val thy = Thm.theory_of_thm st0
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   504
  in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
22724
3002683a6e0f Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents: 22691
diff changeset
   505
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21505
diff changeset
   506
val meson_method_setup = Method.add_methods
cd0dc678a205 simplified method setup;
wenzelm
parents: 21505
diff changeset
   507
  [("meson", Method.thms_args (fn ths =>
22724
3002683a6e0f Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents: 22691
diff changeset
   508
      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21505
diff changeset
   509
    "MESON resolution proof procedure")];
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   510
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   511
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   512
(*** Converting a subgoal into negated conjecture clauses. ***)
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   513
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24215
diff changeset
   514
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
22471
7c51f1a799f3 Removal of axiom names from the theorem cache
paulson
parents: 22360
diff changeset
   515
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   516
fun neg_clausify sts =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   517
  sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   518
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   519
fun neg_conjecture_clauses st0 n =
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   520
  let val st = Seq.hd (neg_skolemize_tac n st0)
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   521
      val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
27187
17b63e145986 use regular error function;
wenzelm
parents: 27184
diff changeset
   522
  in (neg_clausify (the (metahyps_thms n st)), params) end
17b63e145986 use regular error function;
wenzelm
parents: 27184
diff changeset
   523
  handle Option => error "unable to Skolemize subgoal";
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   524
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   525
(*Conversion of a subgoal to conjecture clauses. Each clause has
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   526
  leading !!-bound universal variables, to express generality. *)
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   527
val neg_clausify_tac =
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   528
  neg_skolemize_tac THEN'
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   529
  SUBGOAL
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   530
    (fn (prop,_) =>
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   531
     let val ts = Logic.strip_assums_hyp prop
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   532
     in EVERY1
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   533
         [METAHYPS
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   534
            (fn hyps =>
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   535
              (Method.insert_tac
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   536
                (map forall_intr_vars (neg_clausify hyps)) 1)),
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   537
          REPEAT_DETERM_N (length ts) o (etac thin_rl)]
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   538
     end);
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   539
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   540
val setup_methods = Method.add_methods
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   541
  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   542
    "conversion of goal to conjecture clauses")];
24669
4579eac2c997 proper signature constraint;
wenzelm
parents: 24632
diff changeset
   543
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   544
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   545
(** Attribute for converting a theorem into clauses **)
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   546
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27330
diff changeset
   547
val clausify = Attrib.syntax (Scan.lift OuterParse.nat
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   548
  >> (fn i => Thm.rule_attribute (fn context => fn th =>
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   549
      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   550
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   551
val setup_attrs = Attrib.add_attributes
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   552
  [("clausify", clausify, "conversion of theorem to clauses")];
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   553
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   554
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   555
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   556
(** setup **)
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   557
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   558
val setup =
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   559
  meson_method_setup #>
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   560
  setup_methods #>
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   561
  setup_attrs #>
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   562
  perhaps saturate_skolem_cache #>
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   563
  Theory.at_end clause_cache_endtheory;
18510
0a6c24f549c3 the "skolem" attribute and better initialization of the clause database
paulson
parents: 18404
diff changeset
   564
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   565
end;