src/HOL/Tools/reconstruction.ML
changeset 18729 216e31270509
parent 18708 4b3dadb4fe33
child 19963 806eaa2a2a5e
     1.1 --- a/src/HOL/Tools/reconstruction.ML	Sat Jan 21 23:02:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/reconstruction.ML	Sat Jan 21 23:02:20 2006 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  (*Attributes for reconstructing external resolution proofs*)
     1.5  
     1.6  structure Reconstruction =
     1.7 -let open Attrib
     1.8 -in
     1.9  struct
    1.10  
    1.11  (**************************************************************)
    1.12 @@ -16,10 +14,10 @@
    1.13  (**************************************************************)
    1.14  
    1.15  fun mksubstlist [] sublist = sublist
    1.16 -  | mksubstlist ((a, (_, b)) :: rest) sublist = 
    1.17 +  | mksubstlist ((a, (_, b)) :: rest) sublist =
    1.18        let val vartype = type_of b
    1.19            val avar = Var(a,vartype)
    1.20 -          val newlist = ((avar,b)::sublist) 
    1.21 +          val newlist = ((avar,b)::sublist)
    1.22        in mksubstlist rest newlist end;
    1.23  
    1.24  
    1.25 @@ -31,21 +29,15 @@
    1.26       select_literal (lit1 + 1) cl1
    1.27       RSN ((lit2 + 1), cl2);
    1.28  
    1.29 -fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
    1.30 -
    1.31 -fun gen_binary thm = syntax
    1.32 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
    1.33 -val binary_global = gen_binary global_thm;
    1.34 -val binary_local = gen_binary local_thm;
    1.35 -
    1.36 -(*I have not done the MRR rule because it seems to be identifical to 
    1.37 -binary*)
    1.38 +val binary = Attrib.syntax
    1.39 +  (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    1.40 +    >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    1.41  
    1.42  
    1.43  fun inst_single sign t1 t2 cl =
    1.44      let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
    1.45      in  hd (Seq.list_of(distinct_subgoals_tac
    1.46 -			    (cterm_instantiate [(ct1,ct2)] cl)))  
    1.47 +                            (cterm_instantiate [(ct1,ct2)] cl)))
    1.48      end;
    1.49  
    1.50  fun inst_subst sign substs cl =
    1.51 @@ -71,9 +63,8 @@
    1.52         inst_subst sign (mksubstlist envlist []) cl
    1.53      end;
    1.54  
    1.55 -fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
    1.56 -
    1.57 -fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
    1.58 +val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
    1.59 +  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
    1.60  
    1.61  
    1.62  (** Paramodulation **)
    1.63 @@ -91,32 +82,24 @@
    1.64      in Meson.negated_asm_of_head newth' end;
    1.65  
    1.66  
    1.67 -fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
    1.68 -
    1.69 -fun gen_paramod thm = syntax
    1.70 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
    1.71 -val paramod_global = gen_paramod global_thm;
    1.72 -val paramod_local = gen_paramod local_thm;
    1.73 +val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    1.74 +  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
    1.75  
    1.76  
    1.77  (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
    1.78  
    1.79 -fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
    1.80 +fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
    1.81      let  val eq_lit_th = select_literal (lit1+1) cl1
    1.82           val mod_lit_th = select_literal (lit2+1) cl2
    1.83 -	 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
    1.84 +         val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
    1.85           val eqsubst = eq_lit_th RSN (2,rev_subst)
    1.86           val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
    1.87           val offset = #maxidx(rep_thm newth) + 1
    1.88 -	                  (*ensures "renaming apart" even when Vars are frozen*)
    1.89 +                          (*ensures "renaming apart" even when Vars are frozen*)
    1.90      in Meson.negated_asm_of_head (thaw offset newth) end;
    1.91  
    1.92 -fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
    1.93 -
    1.94 -fun gen_demod thm = syntax
    1.95 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> demod_syntax);
    1.96 -val demod_global = gen_demod global_thm;
    1.97 -val demod_local = gen_demod local_thm;
    1.98 +val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    1.99 +  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
   1.100  
   1.101  
   1.102  (** Conversion of a theorem into clauses **)
   1.103 @@ -124,22 +107,18 @@
   1.104  (*For efficiency, we rely upon memo-izing in ResAxioms.*)
   1.105  fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
   1.106  
   1.107 -fun clausify_syntax i (x, th) = (x, clausify_rule (th,i));
   1.108 -
   1.109 -fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
   1.110 +val clausify = Attrib.syntax (Scan.lift Args.nat
   1.111 +  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   1.112  
   1.113  
   1.114  (** theory setup **)
   1.115  
   1.116  val setup =
   1.117    Attrib.add_attributes
   1.118 -    [("binary", (binary_global, binary_local), "binary resolution"),
   1.119 -     ("paramod", (paramod_global, paramod_local), "paramodulation"),
   1.120 -     ("demod", (demod_global, demod_local), "demodulation"),
   1.121 -     ("factor", (factor, factor), "factoring"),
   1.122 -     ("clausify", (clausify, clausify), "conversion to clauses")];
   1.123 +    [("binary", binary, "binary resolution"),
   1.124 +     ("paramod", paramod, "paramodulation"),
   1.125 +     ("demod", demod, "demodulation"),
   1.126 +     ("factor", factor, "factoring"),
   1.127 +     ("clausify", clausify, "conversion to clauses")];
   1.128  
   1.129  end
   1.130 -end
   1.131 -
   1.132 -