src/HOL/Tools/res_axioms.ML
changeset 27179 8f29fed3dc9a
parent 27174 c2c484480f40
child 27184 b1483d423512
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jun 12 18:54:29 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 12 18:54:31 2008 +0200
     1.3 @@ -7,13 +7,12 @@
     1.4  
     1.5  signature RES_AXIOMS =
     1.6  sig
     1.7 -  val cnf_axiom: thm -> thm list
     1.8 +  val cnf_axiom: theory -> thm -> thm list
     1.9    val pairname: thm -> string * thm
    1.10    val multi_base_blacklist: string list 
    1.11    val bad_for_atp: thm -> bool
    1.12    val type_has_empty_sort: typ -> bool
    1.13 -  val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    1.14 -  val cnf_rules_of_ths: thm list -> thm list
    1.15 +  val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
    1.16    val neg_clausify: thm list -> thm list
    1.17    val expand_defs_tac: thm -> tactic
    1.18    val combinators: thm -> thm
    1.19 @@ -187,33 +186,33 @@
    1.20          | Var _ => makeK()  (*though Var isn't expected*)
    1.21          | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
    1.22          | rator$rand =>
    1.23 -	    if loose_bvar1 (rator,0) then (*C or S*) 
    1.24 -	       if loose_bvar1 (rand,0) then (*S*)
    1.25 -	         let val crator = cterm_of thy (Abs(x,xT,rator))
    1.26 -	             val crand = cterm_of thy (Abs(x,xT,rand))
    1.27 -	             val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
    1.28 -	             val (_,rhs) = Thm.dest_equals (cprop_of abs_S') 
    1.29 -	         in
    1.30 -	           Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
    1.31 -	         end
    1.32 -	       else (*C*)
    1.33 -	         let val crator = cterm_of thy (Abs(x,xT,rator))
    1.34 -	             val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
    1.35 -	             val (_,rhs) = Thm.dest_equals (cprop_of abs_C') 
    1.36 -	         in
    1.37 -	           Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
    1.38 -	         end
    1.39 -	    else if loose_bvar1 (rand,0) then (*B or eta*) 
    1.40 -	       if rand = Bound 0 then eta_conversion ct
    1.41 -	       else (*B*)
    1.42 -	         let val crand = cterm_of thy (Abs(x,xT,rand))
    1.43 -	             val crator = cterm_of thy rator
    1.44 -	             val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B
    1.45 -	             val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 
    1.46 -	         in
    1.47 -	           Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
    1.48 -	         end
    1.49 -	    else makeK()
    1.50 +            if loose_bvar1 (rator,0) then (*C or S*) 
    1.51 +               if loose_bvar1 (rand,0) then (*S*)
    1.52 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
    1.53 +                     val crand = cterm_of thy (Abs(x,xT,rand))
    1.54 +                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
    1.55 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S') 
    1.56 +                 in
    1.57 +                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
    1.58 +                 end
    1.59 +               else (*C*)
    1.60 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
    1.61 +                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
    1.62 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C') 
    1.63 +                 in
    1.64 +                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
    1.65 +                 end
    1.66 +            else if loose_bvar1 (rand,0) then (*B or eta*) 
    1.67 +               if rand = Bound 0 then eta_conversion ct
    1.68 +               else (*B*)
    1.69 +                 let val crand = cterm_of thy (Abs(x,xT,rand))
    1.70 +                     val crator = cterm_of thy rator
    1.71 +                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B
    1.72 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 
    1.73 +                 in
    1.74 +                   Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
    1.75 +                 end
    1.76 +            else makeK()
    1.77          | _ => error "abstract: Bad term"
    1.78    end;
    1.79  
    1.80 @@ -224,26 +223,26 @@
    1.81    else
    1.82    case term_of ct of
    1.83        Abs _ =>
    1.84 -	let val (cv,cta) = Thm.dest_abs NONE ct
    1.85 -	    val (v,Tv) = (dest_Free o term_of) cv
    1.86 -	    val _ = Output.debug (fn()=>"  recursion: " ^ Display.string_of_cterm cta);
    1.87 -	    val u_th = combinators_aux cta
    1.88 -	    val _ = Output.debug (fn()=>"  returned " ^ Display.string_of_thm u_th);
    1.89 -	    val cu = Thm.rhs_of u_th
    1.90 -	    val comb_eq = abstract (Thm.cabs cv cu)
    1.91 -	in Output.debug (fn()=>"  abstraction result: " ^ Display.string_of_thm comb_eq);
    1.92 -	   (transitive (abstract_rule v cv u_th) comb_eq) end
    1.93 +        let val (cv,cta) = Thm.dest_abs NONE ct
    1.94 +            val (v,Tv) = (dest_Free o term_of) cv
    1.95 +            val _ = Output.debug (fn()=>"  recursion: " ^ Display.string_of_cterm cta);
    1.96 +            val u_th = combinators_aux cta
    1.97 +            val _ = Output.debug (fn()=>"  returned " ^ Display.string_of_thm u_th);
    1.98 +            val cu = Thm.rhs_of u_th
    1.99 +            val comb_eq = abstract (Thm.cabs cv cu)
   1.100 +        in Output.debug (fn()=>"  abstraction result: " ^ Display.string_of_thm comb_eq);
   1.101 +           (transitive (abstract_rule v cv u_th) comb_eq) end
   1.102      | t1 $ t2 =>
   1.103 -	let val (ct1,ct2) = Thm.dest_comb ct
   1.104 -	in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
   1.105 +        let val (ct1,ct2) = Thm.dest_comb ct
   1.106 +        in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
   1.107              
   1.108  fun combinators th =
   1.109    if lambda_free (prop_of th) then th 
   1.110    else
   1.111      let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
   1.112 -	val th = Drule.eta_contraction_rule th
   1.113 -	val eqth = combinators_aux (cprop_of th)
   1.114 -	val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
   1.115 +        val th = Drule.eta_contraction_rule th
   1.116 +        val eqth = combinators_aux (cprop_of th)
   1.117 +        val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
   1.118      in  equal_elim eqth th   end
   1.119      handle THM (msg,_,_) => 
   1.120        (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
   1.121 @@ -285,19 +284,9 @@
   1.122    end;
   1.123  
   1.124  
   1.125 -(*This will refer to the final version of theory ATP_Linkup.*)
   1.126 -val atp_linkup_thy_ref = @{theory_ref}
   1.127 -
   1.128 -(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
   1.129 -  inside that theory -- because it's needed for Skolemization.
   1.130 -  If called while ATP_Linkup is being created, it will transfer to the
   1.131 -  current version. If called afterward, it will transfer to the final version.*)
   1.132 -fun transfer_to_ATP_Linkup th =
   1.133 -    transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
   1.134 -
   1.135  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   1.136  fun to_nnf th ctxt0 =
   1.137 -  let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes
   1.138 +  let val th1 = th |> transform_elim |> zero_var_indexes
   1.139        val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
   1.140        val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
   1.141    in  (th3, ctxt)  end;
   1.142 @@ -369,9 +358,11 @@
   1.143  
   1.144  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   1.145    It returns a modified theory, unless skolemization fails.*)
   1.146 -fun skolem th thy =
   1.147 -  let val ctxt0 = Variable.thm_context th
   1.148 -      val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
   1.149 +fun skolem th0 thy =
   1.150 +  let
   1.151 +    val th = Thm.transfer thy th0
   1.152 +    val ctxt0 = Variable.thm_context th
   1.153 +    val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
   1.154    in
   1.155       Option.map
   1.156          (fn (nnfth,ctxt1) =>
   1.157 @@ -405,7 +396,7 @@
   1.158  fun skolem_cache_thm th thy =
   1.159    case Thmtab.lookup (ThmCache.get thy) th of
   1.160        NONE =>
   1.161 -        (case skolem (Thm.transfer thy th) thy of
   1.162 +        (case skolem th thy of
   1.163               NONE => ([th],thy)
   1.164             | SOME (cls,thy') =>
   1.165                   (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
   1.166 @@ -418,14 +409,14 @@
   1.167    if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
   1.168    else 
   1.169        let val ctxt0 = Variable.thm_context th
   1.170 -	  val (nnfth,ctxt1) = to_nnf th ctxt0
   1.171 -	  val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
   1.172 +          val (nnfth,ctxt1) = to_nnf th ctxt0
   1.173 +          val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
   1.174        in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
   1.175        handle THM _ => [];
   1.176  
   1.177  (*Exported function to convert Isabelle theorems into axiom clauses*)
   1.178 -fun cnf_axiom th =
   1.179 -  let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th)
   1.180 +fun cnf_axiom thy th0 =
   1.181 +  let val th = Thm.transfer thy th0
   1.182    in
   1.183        case Thmtab.lookup (ThmCache.get thy) th of
   1.184            NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
   1.185 @@ -466,14 +457,14 @@
   1.186  fun pair_name_cls k (n, []) = []
   1.187    | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
   1.188  
   1.189 -fun cnf_rules_pairs_aux pairs [] = pairs
   1.190 -  | cnf_rules_pairs_aux pairs ((name,th)::ths) =
   1.191 -      let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs
   1.192 +fun cnf_rules_pairs_aux _ pairs [] = pairs
   1.193 +  | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
   1.194 +      let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
   1.195                         handle THM _ => pairs | ResClause.CLAUSE _ => pairs
   1.196 -      in  cnf_rules_pairs_aux pairs' ths  end;
   1.197 +      in  cnf_rules_pairs_aux thy pairs' ths  end;
   1.198  
   1.199  (*The combination of rev and tail recursion preserves the original order*)
   1.200 -fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
   1.201 +fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
   1.202  
   1.203  
   1.204  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   1.205 @@ -505,10 +496,9 @@
   1.206     (Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy);
   1.207      Option.map skolem_cache_node (try mark_skolemized thy) );
   1.208  
   1.209 +
   1.210  (*** meson proof methods ***)
   1.211  
   1.212 -fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
   1.213 -
   1.214  (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
   1.215  fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
   1.216    | is_absko _ = false;
   1.217 @@ -537,22 +527,22 @@
   1.218  
   1.219  
   1.220  fun meson_general_tac ths i st0 =
   1.221 - let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths))
   1.222 - in  (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
   1.223 +  let
   1.224 +    val thy = Thm.theory_of_thm st0
   1.225 +    val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths))
   1.226 +  in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
   1.227  
   1.228  val meson_method_setup = Method.add_methods
   1.229    [("meson", Method.thms_args (fn ths =>
   1.230        Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
   1.231      "MESON resolution proof procedure")];
   1.232  
   1.233 +
   1.234  (** Attribute for converting a theorem into clauses **)
   1.235  
   1.236 -fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th);
   1.237 -
   1.238 -fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
   1.239 -
   1.240  val clausify = Attrib.syntax (Scan.lift Args.nat
   1.241 -  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   1.242 +  >> (fn i => Thm.rule_attribute (fn context => fn th =>
   1.243 +      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
   1.244  
   1.245  
   1.246  (*** Converting a subgoal into negated conjecture clauses. ***)
   1.247 @@ -583,6 +573,7 @@
   1.248            REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   1.249       end);
   1.250  
   1.251 +
   1.252  (** The Skolemization attribute **)
   1.253  
   1.254  fun conj2_rule (th1,th2) = conjI OF [th1,th2];