abstraction of lambda-expressions
authorpaulson
Fri Aug 25 18:48:58 2006 +0200 (2006-08-25 ago)
changeset 20419df257a9cf0e9
parent 20418 7c1aa7872266
child 20420 56ef2dfc41d6
abstraction of lambda-expressions
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 25 18:48:09 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 25 18:48:58 2006 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  (*** background linkup ***)
     1.5  val call_atp = ref false; 
     1.6  val hook_count = ref 0;
     1.7 -val time_limit = ref 30;
     1.8 +val time_limit = ref 80;
     1.9  val prover = ref "E";   (* use E as the default prover *)
    1.10  val custom_spass =   (*specialized options for SPASS*)
    1.11        ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    1.12 @@ -735,7 +735,7 @@
    1.13  	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
    1.14  	                                   skolemize_tac] n th)
    1.15  		  val negs = Option.valOf (metahyps_thms n st)
    1.16 -		  val negs_clauses = make_clauses negs
    1.17 +		  val negs_clauses = ResAxioms.assume_abstract (make_clauses negs)
    1.18  	      in
    1.19  		  negs_clauses :: get_neg_subgoals (n-1)
    1.20  	      end
    1.21 @@ -809,7 +809,7 @@
    1.22  		  Pretty.string_of (ProofContext.pretty_term ctxt
    1.23  		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.24      Output.debug ("current theory: " ^ Context.theory_name thy);
    1.25 -    hook_count := !hook_count +1;
    1.26 +    inc hook_count;
    1.27      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.28      ResClause.init thy;
    1.29      ResHolClause.init thy;
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Aug 25 18:48:09 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Aug 25 18:48:58 2006 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
     2.5    val pairname : thm -> (string * thm)
     2.6    val skolem_thm : thm -> thm list
     2.7 +  val to_nnf : thm -> thm
     2.8    val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
     2.9    val meson_method_setup : theory -> theory
    2.10    val setup : theory -> theory
    2.11 @@ -25,17 +26,22 @@
    2.12    val atpset_rules_of_thy : theory -> (string * thm) list
    2.13    val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
    2.14    end;
    2.15 -
    2.16 -structure ResAxioms : RES_AXIOMS =
    2.17 + 
    2.18 +structure ResAxioms =
    2.19   
    2.20  struct
    2.21  
    2.22 +(*FIXME DELETE: For running the comparison between combinators and abstractions.
    2.23 +  CANNOT be a ref, as the setting is used while Isabelle is built.*)
    2.24 +val abstract_lambdas = true;
    2.25 +
    2.26 +val trace_abs = ref false;
    2.27  
    2.28  (**** Transformation of Elimination Rules into First-Order Formulas****)
    2.29  
    2.30  (* a tactic used to prove an elim-rule. *)
    2.31  fun elimRule_tac th =
    2.32 -    (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(blast_tac HOL_cs 1);
    2.33 +    (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
    2.34  
    2.35  fun add_EX tm [] = tm
    2.36    | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
    2.37 @@ -97,10 +103,8 @@
    2.38                              " for theorem " ^ string_of_thm th); th) 
    2.39  
    2.40  
    2.41 -
    2.42  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    2.43  
    2.44 -
    2.45  (*Transfer a theorem into theory Reconstruction.thy if it is not already
    2.46    inside that theory -- because it's needed for Skolemization *)
    2.47  
    2.48 @@ -126,43 +130,41 @@
    2.49  (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
    2.50    prefix for the Skolem constant. Result is a new theory*)
    2.51  fun declare_skofuns s th thy =
    2.52 -  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) =
    2.53 +  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
    2.54  	    (*Existential: declare a Skolem function, then insert into body and continue*)
    2.55 -	    let val cname = s ^ "_" ^ Int.toString n
    2.56 +	    let val cname = gensym ("sko_" ^ s ^ "_")
    2.57  		val args = term_frees xtp  (*get the formal parameter list*)
    2.58  		val Ts = map type_of args
    2.59  		val cT = Ts ---> T
    2.60  		val c = Const (Sign.full_name thy cname, cT)
    2.61  		val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
    2.62  		        (*Forms a lambda-abstraction over the formal parameters*)
    2.63 -		val def = equals cT $ c $ rhs
    2.64  		val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
    2.65  		           (*Theory is augmented with the constant, then its def*)
    2.66  		val cdef = cname ^ "_def"
    2.67 -		val thy'' = Theory.add_defs_i false false [(cdef, def)] thy'
    2.68 +		val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
    2.69  	    in dec_sko (subst_bound (list_comb(c,args), p)) 
    2.70 -	               (n+1, (thy'', get_axiom thy'' cdef :: axs)) 
    2.71 +	               (thy'', get_axiom thy'' cdef :: axs)
    2.72  	    end
    2.73 -	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
    2.74 +	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
    2.75  	    (*Universal quant: insert a free variable into body and continue*)
    2.76  	    let val fname = Name.variant (add_term_names (p,[])) a
    2.77 -	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
    2.78 -	| dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
    2.79 -	| dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
    2.80 -	| dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy
    2.81 -	| dec_sko t nthx = nthx (*Do nothing otherwise*)
    2.82 -  in  #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[])))  end;
    2.83 +	    in dec_sko (subst_bound (Free(fname,T), p)) thx end
    2.84 +	| dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.85 +	| dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.86 +	| dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
    2.87 +	| dec_sko t thx = thx (*Do nothing otherwise*)
    2.88 +  in  dec_sko (prop_of th) (thy,[])  end;
    2.89  
    2.90  (*Traverse a theorem, accumulating Skolem function definitions.*)
    2.91  fun assume_skofuns th =
    2.92    let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
    2.93  	    (*Existential: declare a Skolem function, then insert into body and continue*)
    2.94 -	    let val name = Name.variant (add_term_names (p,[])) (gensym "sko_")
    2.95 -                val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
    2.96 +	    let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
    2.97  		val args = term_frees xtp \\ skos  (*the formal parameters*)
    2.98  		val Ts = map type_of args
    2.99  		val cT = Ts ---> T
   2.100 -		val c = Free (name, cT)
   2.101 +		val c = Free (gensym "sko_", cT)
   2.102  		val rhs = list_abs_free (map dest_Free args,        
   2.103  		                         HOLogic.choice_const T $ xtp)
   2.104  		      (*Forms a lambda-abstraction over the formal parameters*)
   2.105 @@ -178,7 +180,145 @@
   2.106  	| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   2.107  	| dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
   2.108  	| dec_sko t defs = defs (*Do nothing otherwise*)
   2.109 -  in  dec_sko (#prop (rep_thm th)) []  end;
   2.110 +  in  dec_sko (prop_of th) []  end;
   2.111 +
   2.112 +
   2.113 +(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
   2.114 +
   2.115 +(*Returns the vars of a theorem*)
   2.116 +fun vars_of_thm th =
   2.117 +  map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
   2.118 +
   2.119 +(*Make a version of fun_cong with a given variable name*)
   2.120 +local
   2.121 +    val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
   2.122 +    val cx = hd (vars_of_thm fun_cong');
   2.123 +    val ty = typ_of (ctyp_of_term cx);
   2.124 +    val thy = Thm.theory_of_thm fun_cong;
   2.125 +    fun mkvar a = cterm_of thy (Var((a,0),ty));
   2.126 +in
   2.127 +fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
   2.128 +end;
   2.129 +
   2.130 +(*Removes the lambdas from an equation of the form t = (%x. u)*)
   2.131 +fun strip_lambdas th = 
   2.132 +  case prop_of th of
   2.133 +      _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
   2.134 +          strip_lambdas (#1 (Drule.freeze_thaw (th RS xfun_cong x)))
   2.135 +    | _ => th;
   2.136 +
   2.137 +(*Convert meta- to object-equality. Fails for theorems like split_comp_eq, 
   2.138 +  where some types have the empty sort.*)
   2.139 +fun object_eq th = th RS def_imp_eq 
   2.140 +    handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
   2.141 +  
   2.142 +fun valid_name vs (Free(x,T)) = x mem_string vs
   2.143 +  | valid_name vs _ = false;
   2.144 +
   2.145 +(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
   2.146 +fun eta_conversion_rule th =
   2.147 +  equal_elim (eta_conversion (cprop_of th)) th;
   2.148 +  
   2.149 +fun crhs th =
   2.150 +  case Drule.strip_comb (cprop_of th) of
   2.151 +      (f, [_, rhs]) => 
   2.152 +          (case term_of f of
   2.153 +               Const ("==", _) => rhs
   2.154 +             | _ => raise THM ("crhs", 0, [th]))
   2.155 +    | _ => raise THM ("crhs", 1, [th]);
   2.156 +
   2.157 +(*Apply a function definition to an argument, beta-reducing the result.*)
   2.158 +fun beta_comb cf x =
   2.159 +  let val th1 = combination cf (reflexive x)
   2.160 +      val th2 = beta_conversion false (crhs th1)
   2.161 +  in  transitive th1 th2  end;
   2.162 +
   2.163 +(*Apply a function definition to arguments, beta-reducing along the way.*)
   2.164 +fun list_combination cf [] = cf
   2.165 +  | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
   2.166 +
   2.167 +fun list_cabs ([] ,     t) = t
   2.168 +  | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
   2.169 +
   2.170 +(*FIXME DELETE*)
   2.171 +fun check_eta ct = 
   2.172 +  let val t = term_of ct 
   2.173 +  in if (t aconv Envir.eta_contract t) then ()  
   2.174 +     else error ("Eta redex in term: " ^ string_of_cterm ct)
   2.175 +  end;
   2.176 +
   2.177 +(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   2.178 +  prefix for the constants. Resulting theory is returned in the first theorem. *)
   2.179 +fun declare_absfuns th =
   2.180 +  let fun abstract thy ct = case term_of ct of
   2.181 +          Abs (_,T,u) =>
   2.182 +	    let val cname = gensym "abs_"
   2.183 +	        val _ = check_eta ct;
   2.184 +		val (cv,cta) = Thm.dest_abs NONE ct
   2.185 +		val v = (#1 o dest_Free o term_of) cv
   2.186 +		val (u'_th,defs) = abstract thy cta
   2.187 +                val cu' = crhs u'_th
   2.188 +		val abs_v_u = lambda (term_of cv) (term_of cu')
   2.189 +		(*get the formal parameters: ALL variables free in the term*)
   2.190 +		val args = term_frees abs_v_u
   2.191 +		val Ts = map type_of args
   2.192 +		val cT = Ts ---> (T --> typ_of (ctyp_of_term cu'))
   2.193 +		val thy = theory_of_thm u'_th
   2.194 +		val c = Const (Sign.full_name thy cname, cT)
   2.195 +		val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy
   2.196 +		           (*Theory is augmented with the constant, then its def*)
   2.197 +		val rhs = list_abs_free (map dest_Free args, abs_v_u)
   2.198 +		      (*Forms a lambda-abstraction over the formal parameters*)
   2.199 +		val cdef = cname ^ "_def"
   2.200 +		val thy = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy		      
   2.201 +		val def = #1 (Drule.freeze_thaw (get_axiom thy cdef))
   2.202 +		val def_args = list_combination def (map (cterm_of thy) args)
   2.203 +	    in (transitive (abstract_rule v cv u'_th) (symmetric def_args), 
   2.204 +	        def :: defs) end
   2.205 +	| (t1$t2) =>
   2.206 +	    let val (ct1,ct2) = Thm.dest_comb ct
   2.207 +	        val (th1,defs1) = abstract thy ct1
   2.208 +		val (th2,defs2) = abstract (theory_of_thm th1) ct2
   2.209 +	    in  (combination th1 th2, defs1@defs2)  end
   2.210 +	| _ => (transfer thy (reflexive ct), [])
   2.211 +      val _ = if !trace_abs then warning (string_of_thm th) else ();
   2.212 +      val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
   2.213 +      val ths = equal_elim eqth th ::
   2.214 +                map (forall_intr_vars o strip_lambdas o object_eq) defs
   2.215 +  in  (theory_of_thm eqth, ths)  end;
   2.216 +
   2.217 +fun assume_absfuns th =
   2.218 +  let val cterm = cterm_of (Thm.theory_of_thm th)
   2.219 +      fun abstract vs ct = case term_of ct of
   2.220 +          Abs (_,T,u) =>
   2.221 +	    let val (cv,cta) = Thm.dest_abs NONE ct
   2.222 +	        val _ = check_eta ct;
   2.223 +		val v = (#1 o dest_Free o term_of) cv
   2.224 +		val (u'_th,defs) = abstract (v::vs) cta
   2.225 +                val cu' = crhs u'_th
   2.226 +		val abs_v_u = Thm.cabs cv cu'
   2.227 +		(*get the formal parameters: bound variables also present in the term*)
   2.228 +		val args = filter (valid_name vs) (term_frees (term_of abs_v_u))
   2.229 +		val Ts = map type_of args
   2.230 +		val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu'))
   2.231 +		val c = Free (gensym "abs_", const_ty)
   2.232 +		val rhs = list_cabs (map cterm args, abs_v_u)
   2.233 +		      (*Forms a lambda-abstraction over the formal parameters*)
   2.234 +		val def = assume (Thm.capply (cterm (equals const_ty $ c)) rhs)
   2.235 +		val def_args = list_combination def (map cterm args)
   2.236 +	    in (transitive (abstract_rule v cv u'_th) (symmetric def_args), 
   2.237 +	        def :: defs) end
   2.238 +	| (t1$t2) =>
   2.239 +	    let val (ct1,ct2) = Thm.dest_comb ct
   2.240 +	        val (t1',defs1) = abstract vs ct1
   2.241 +		val (t2',defs2) = abstract vs ct2
   2.242 +	    in  (combination t1' t2', defs1@defs2)  end
   2.243 +	| _ => (reflexive ct, [])
   2.244 +      val (eqth,defs) = abstract [] (cprop_of th)
   2.245 +  in  equal_elim eqth th ::
   2.246 +      map (forall_intr_vars o strip_lambdas o object_eq) defs
   2.247 +  end;
   2.248 +
   2.249  
   2.250  (*cterms are used throughout for efficiency*)
   2.251  val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
   2.252 @@ -217,7 +357,7 @@
   2.253  (*It now works for HOL too. *)
   2.254  fun to_nnf th = 
   2.255      th |> transfer_to_Reconstruction
   2.256 -       |> transform_elim |> Drule.freeze_thaw |> #1
   2.257 +       |> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1
   2.258         |> ObjectLogic.atomize_thm |> make_nnf;
   2.259  
   2.260  (*The cache prevents repeated clausification of a theorem, 
   2.261 @@ -230,23 +370,46 @@
   2.262  fun skolem_of_nnf th =
   2.263    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
   2.264  
   2.265 +(*Replace lambdas by assumed function definitions in the theorems*)
   2.266 +fun assume_abstract ths =
   2.267 +  if abstract_lambdas then List.concat (map (assume_absfuns o eta_conversion_rule) ths)
   2.268 +  else map eta_conversion_rule ths;
   2.269 +
   2.270 +(*Replace lambdas by declared function definitions in the theorems*)
   2.271 +fun declare_abstract' (thy, []) = (thy, [])
   2.272 +  | declare_abstract' (thy, th::ths) =
   2.273 +      let val (thy', th_defs) = 
   2.274 +            th |> zero_var_indexes |> Drule.freeze_thaw |> #1
   2.275 +               |> eta_conversion_rule |> transfer thy |> declare_absfuns
   2.276 +	  val (thy'', ths') = declare_abstract' (thy', ths)
   2.277 +      in  (thy'', th_defs @ ths')  end;
   2.278 +
   2.279 +(*FIXME DELETE*)
   2.280 +fun declare_abstract (thy, ths) =
   2.281 +  if abstract_lambdas then declare_abstract' (thy, ths)
   2.282 +  else (thy, map eta_conversion_rule ths);
   2.283 +
   2.284  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   2.285  (*also works for HOL*) 
   2.286  fun skolem_thm th = 
   2.287    let val nnfth = to_nnf th
   2.288 -  in  rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
   2.289 +  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
   2.290 +      |> assume_abstract |> Meson.finish_cnf |> rm_redundant_cls
   2.291    end
   2.292    handle THM _ => [];
   2.293  
   2.294  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   2.295    It returns a modified theory, unless skolemization fails.*)
   2.296  fun skolem thy (name,th) =
   2.297 -  let val cname = (case name of "" => gensym "sko_" | s => Sign.base_name s)
   2.298 +  let val cname = (case name of "" => gensym "" | s => Sign.base_name s)
   2.299 +      val _ = Output.debug ("skolemizing " ^ name ^ ": ")
   2.300    in Option.map 
   2.301          (fn nnfth => 
   2.302            let val (thy',defs) = declare_skofuns cname nnfth thy
   2.303 -              val skoths = map skolem_of_def defs
   2.304 -          in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)
   2.305 +              val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   2.306 +              val (thy'',cnfs') = declare_abstract (thy',cnfs)
   2.307 +          in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs'))
   2.308 +          end)
   2.309        (SOME (to_nnf th)  handle THM _ => NONE) 
   2.310    end;
   2.311  
   2.312 @@ -347,14 +510,8 @@
   2.313  
   2.314  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   2.315  
   2.316 -(*Setup function: takes a theory and installs ALL simprules and claset rules 
   2.317 -  into the clause cache*)
   2.318 -fun clause_cache_setup thy =
   2.319 -  let val simps = simpset_rules_of_thy thy
   2.320 -      and clas  = claset_rules_of_thy thy
   2.321 -      val thy1  = List.foldl skolem_cache thy clas
   2.322 -  in List.foldl skolem_cache thy1 simps end;
   2.323 -(*Could be duplicate theorem names, due to multiple attributes*)
   2.324 +(*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
   2.325 +fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy);
   2.326    
   2.327  
   2.328  (*** meson proof methods ***)
   2.329 @@ -379,15 +536,14 @@
   2.330  (*Conjoin a list of clauses to recreate a single theorem*)
   2.331  val conj_rule = foldr1 conj2_rule;
   2.332  
   2.333 -fun skolem (Context.Theory thy, th) =
   2.334 -      let
   2.335 -        val name = Thm.name_of_thm th
   2.336 -        val (cls, thy') = skolem_cache_thm ((name, th), thy)
   2.337 +fun skolem_attr (Context.Theory thy, th) =
   2.338 +      let val name = Thm.name_of_thm th
   2.339 +          val (cls, thy') = skolem_cache_thm ((name, th), thy)
   2.340        in (Context.Theory thy', conj_rule cls) end
   2.341 -  | skolem (context, th) = (context, conj_rule (skolem_thm th));
   2.342 +  | skolem_attr (context, th) = (context, conj_rule (skolem_thm th));
   2.343  
   2.344  val setup_attrs = Attrib.add_attributes
   2.345 -  [("skolem", Attrib.no_args skolem, "skolemization of a theorem")];
   2.346 +  [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];
   2.347  
   2.348  val setup = clause_cache_setup #> setup_attrs;
   2.349