author  paulson 
Thu, 29 Jun 2006 18:10:59 +0200  
changeset 19963  806eaa2a2a5e 
parent 18729  216e31270509 
child 20258  4fe3c0911907 
permissions  rwrr 
15151  1 
(* Title: HOL/Reconstruction.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Claire Quigley 

4 
Copyright 2004 University of Cambridge 

5 
*) 

6 

7 
(*Attributes for reconstructing external resolution proofs*) 

8 

9 
structure Reconstruction = 

10 
struct 

11 

12 
(**** attributes ****) 

13 

14 
(** Binary resolution **) 

15 

16 
fun binary_rule ((cl1, lit1), (cl2 , lit2)) = 

17 
select_literal (lit1 + 1) cl1 

18 
RSN ((lit2 + 1), cl2); 

19 

18729  20 
val binary = Attrib.syntax 
21 
(Scan.lift Args.nat  Attrib.thm  Scan.lift Args.nat 

22 
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); 

15151  23 

24 

19963  25 
(** Factoring **) 
26 

27 
(*NB this code did not work at all before 29/6/2006. Even now its behaviour may 

28 
not be as expected. It unifies the designated literals 

29 
and then deletes ALL duplicates of literals (not just those designated)*) 

30 

31 
fun mksubstlist [] sublist = sublist 

32 
 mksubstlist ((a, (T, b)) :: rest) sublist = 

33 
mksubstlist rest ((Var(a,T), b)::sublist); 

15151  34 

19963  35 
fun reorient (x,y) = 
36 
if is_Var x then (x,y) 

37 
else if is_Var y then (y,x) 

38 
else error "Reconstruction.reorient: neither term is a Var"; 

15151  39 

19963  40 
fun inst_subst sign subst cl = 
41 
let val subst' = map (pairself (cterm_of sign) o reorient) subst 

42 
in 

43 
Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl)) 

44 
end; 

15151  45 

46 
fun factor_rule (cl, lit1, lit2) = 

47 
let 

48 
val prems = prems_of cl 

49 
val fac1 = List.nth (prems,lit1) 

50 
val fac2 = List.nth (prems,lit2) 

51 
val sign = sign_of_thm cl 

52 
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)]) 

17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
15955
diff
changeset

53 
val newenv = ReconTranslateProof.getnewenv unif_env 
15151  54 
val envlist = Envir.alist_of newenv 
55 
in 

56 
inst_subst sign (mksubstlist envlist []) cl 

57 
end; 

58 

18729  59 
val factor = Attrib.syntax (Scan.lift (Args.nat  Args.nat) 
60 
>> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j)))); 

15151  61 

62 

63 
(** Paramodulation **) 

64 

15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

65 
(*subst with premises exchanged: that way, side literals of the equality will appear 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

66 
as the second to last premises of the result.*) 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

67 
val rev_subst = rotate_prems 1 subst; 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

68 

15499  69 
fun paramod_rule ((cl1, lit1), (cl2, lit2)) = 
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

70 
let val eq_lit_th = select_literal (lit1+1) cl1 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

71 
val mod_lit_th = select_literal (lit2+1) cl2 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

72 
val eqsubst = eq_lit_th RSN (2,rev_subst) 
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

73 
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) 
15499  74 
val newth' = Seq.hd (flexflex_rule newth) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15531
diff
changeset

75 
in Meson.negated_asm_of_head newth' end; 
15151  76 

77 

18729  78 
val paramod = Attrib.syntax (Scan.lift Args.nat  Attrib.thm  Scan.lift Args.nat 
79 
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j))))); 

15151  80 

81 

15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

82 
(** Demodulation: rewriting of a single literal (NonUnit Rewriting, SPASS) **) 
15151  83 

18729  84 
fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
15151  85 
let val eq_lit_th = select_literal (lit1+1) cl1 
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

86 
val mod_lit_th = select_literal (lit2+1) cl2 
18729  87 
val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th 
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset

88 
val eqsubst = eq_lit_th RSN (2,rev_subst) 
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15466
diff
changeset

89 
val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst) 
15499  90 
val offset = #maxidx(rep_thm newth) + 1 
18729  91 
(*ensures "renaming apart" even when Vars are frozen*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15531
diff
changeset

92 
in Meson.negated_asm_of_head (thaw offset newth) end; 
15151  93 

18729  94 
val demod = Attrib.syntax (Scan.lift Args.nat  Attrib.thm  Scan.lift Args.nat 
95 
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j))))); 

15151  96 

97 

15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset

98 
(** Conversion of a theorem into clauses **) 
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset

99 

15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15794
diff
changeset

100 
(*For efficiency, we rely upon memoizing in ResAxioms.*) 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15794
diff
changeset

101 
fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i) 
15466  102 

18729  103 
val clausify = Attrib.syntax (Scan.lift Args.nat 
104 
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); 

15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset

105 

8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset

106 

15151  107 
(** theory setup **) 
108 

109 
val setup = 

18708  110 
Attrib.add_attributes 
18729  111 
[("binary", binary, "binary resolution"), 
112 
("paramod", paramod, "paramodulation"), 

113 
("demod", demod, "demodulation"), 

114 
("factor", factor, "factoring"), 

115 
("clausify", clausify, "conversion to clauses")]; 

15151  116 

117 
end 