src/HOL/Tools/res_axioms.ML
changeset 24215 5458fbf18276
parent 24137 8d7896398147
child 24300 e170cee91c66
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Aug 10 14:49:01 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Aug 10 15:13:18 2007 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature RES_AXIOMS =
     1.6  sig
     1.7 -  val trace_abs: bool ref
     1.8    val cnf_axiom : string * thm -> thm list
     1.9    val cnf_name : string -> thm list
    1.10    val meta_cnf_axiom : thm -> thm list
    1.11 @@ -32,8 +31,6 @@
    1.12    because it is not performed by inference!!*)
    1.13  val abstract_lambdas = true;
    1.14  
    1.15 -val trace_abs = ref false;
    1.16 -
    1.17  (* FIXME legacy *)
    1.18  fun freeze_thm th = #1 (Drule.freeze_thaw th);
    1.19  
    1.20 @@ -230,8 +227,8 @@
    1.21  (*Does an existing abstraction definition have an RHS that matches the one we need now?
    1.22    thy is the current theory, which must extend that of theorem th.*)
    1.23  fun match_rhs thy t th =
    1.24 -  let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
    1.25 -                                          " against\n" ^ string_of_thm th) else ();
    1.26 +  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
    1.27 +                                   " against\n" ^ string_of_thm th);
    1.28        val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
    1.29        val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
    1.30        val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
    1.31 @@ -256,27 +253,27 @@
    1.32                  val _ = assert_eta_free ct;
    1.33                  val (cvs,cta) = dest_abs_list ct
    1.34                  val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
    1.35 -                val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
    1.36 +                val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
    1.37                  val (u'_th,defs) = abstract thy cta
    1.38 -                val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
    1.39 +                val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
    1.40                  val cu' = Thm.rhs_of u'_th
    1.41                  val u' = term_of cu'
    1.42                  val abs_v_u = lambda_list (map term_of cvs) u'
    1.43                  (*get the formal parameters: ALL variables free in the term*)
    1.44                  val args = term_frees abs_v_u
    1.45 -                val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
    1.46 +                val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
    1.47                  val rhs = list_abs_free (map dest_Free args, abs_v_u)
    1.48                        (*Forms a lambda-abstraction over the formal parameters*)
    1.49 -                val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
    1.50 +                val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
    1.51                  val thy = theory_of_thm u'_th
    1.52                  val (ax,ax',thy) =
    1.53                   case List.mapPartial (match_rhs thy abs_v_u) 
    1.54                           (Net.match_term (!abstraction_cache) u') of
    1.55                       (ax,ax')::_ => 
    1.56 -                       (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
    1.57 +                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
    1.58                          (ax,ax',thy))
    1.59                     | [] =>
    1.60 -                      let val _ = if !trace_abs then warning "Lookup was empty" else ();
    1.61 +                      let val _ = Output.debug (fn()=>"Lookup was empty");
    1.62                            val Ts = map type_of args
    1.63                            val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
    1.64                            val c = Const (Sign.full_name thy cname, cT)
    1.65 @@ -286,33 +283,29 @@
    1.66                            val cdef = cname ^ "_def"
    1.67                            val thy = Theory.add_defs_i false false
    1.68                                         [(cdef, equals cT $ c $ rhs)] thy
    1.69 -                          val _ = if !trace_abs then (warning ("Definition is " ^ 
    1.70 -                                                      string_of_thm (get_axiom thy cdef))) 
    1.71 -                                  else ();
    1.72 +                          val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
    1.73                            val ax = get_axiom thy cdef |> freeze_thm
    1.74                                       |> mk_object_eq |> strip_lambdas (length args)
    1.75                                       |> mk_meta_eq |> Meson.generalize
    1.76                            val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
    1.77 -                          val _ = if !trace_abs then 
    1.78 -                                    (warning ("Declaring: " ^ string_of_thm ax);
    1.79 -                                     warning ("Instance: " ^ string_of_thm ax')) 
    1.80 -                                  else ();
    1.81 +                          val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
    1.82 +                                                       "Instance: " ^ string_of_thm ax');
    1.83                            val _ = abstraction_cache := Net.insert_term eq_absdef 
    1.84                                              ((Logic.varify u'), ax) (!abstraction_cache)
    1.85                              handle Net.INSERT =>
    1.86                                raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
    1.87                         in  (ax,ax',thy)  end
    1.88 -            in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
    1.89 +            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
    1.90                 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
    1.91          | (t1$t2) =>
    1.92              let val (ct1,ct2) = Thm.dest_comb ct
    1.93                  val (th1,defs1) = abstract thy ct1
    1.94                  val (th2,defs2) = abstract (theory_of_thm th1) ct2
    1.95              in  (combination th1 th2, defs1@defs2)  end
    1.96 -      val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
    1.97 +      val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
    1.98        val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
    1.99        val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   1.100 -      val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   1.101 +      val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
   1.102    in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
   1.103  
   1.104  fun name_of def = try (#1 o dest_Free o lhs_of) def;
   1.105 @@ -349,7 +342,7 @@
   1.106                   case List.mapPartial (match_rhs thy abs_v_u) 
   1.107                          (Net.match_term (!abstraction_cache) u') of
   1.108                       (ax,ax')::_ => 
   1.109 -                       (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
   1.110 +                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   1.111                          (ax,ax'))
   1.112                     | [] =>
   1.113                        let val Ts = map type_of args
   1.114 @@ -365,17 +358,17 @@
   1.115                              handle Net.INSERT =>
   1.116                                raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   1.117                        in (ax,ax') end
   1.118 -            in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
   1.119 +            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   1.120                 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   1.121          | (t1$t2) =>
   1.122              let val (ct1,ct2) = Thm.dest_comb ct
   1.123                  val (t1',defs1) = abstract ct1
   1.124                  val (t2',defs2) = abstract ct2
   1.125              in  (combination t1' t2', defs1@defs2)  end
   1.126 -      val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
   1.127 +      val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
   1.128        val (eqth,defs) = abstract (cprop_of th)
   1.129        val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   1.130 -      val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   1.131 +      val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
   1.132    in  map Drule.eta_contraction_rule ths  end;
   1.133  
   1.134  
   1.135 @@ -603,6 +596,9 @@
   1.136        is_Free t andalso not (member (op aconv) xs t)
   1.137    | is_okdef _ _ = false
   1.138  
   1.139 +(*This function tries to cope with open locales, which introduce hypotheses of the form
   1.140 +  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   1.141 +  of llabs_ and sko_ functions. *)
   1.142  fun expand_defs_tac st0 st =
   1.143    let val hyps0 = #hyps (rep_thm st0)
   1.144        val hyps = #hyps (crep_thm st)