author  wenzelm 
Sat, 21 Jul 2007 23:25:00 +0200  
changeset 23894  1a4167d761ac 
parent 23590  ad95084a5c63 
child 24040  0d5cf52ebf87 
permissions  rwrr 
9869  1 
(* Title: HOL/Tools/meson.ML 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

2 
ID: $Id$ 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

4 
Copyright 1992 University of Cambridge 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

5 

9869  6 
The MESON resolution proof procedure for HOL. 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

7 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

8 
When making clauses, avoids using the rewriter  instead uses RS recursively 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

9 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

10 
NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

11 
FUNCTION nodups  if done to goal clauses too! 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

12 
*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

13 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

14 
signature BASIC_MESON = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

15 
sig 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

16 
val size_of_subgoals : thm > int 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

17 
val make_cnf : thm list > thm > thm list 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

18 
val finish_cnf : thm list > thm list 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

19 
val make_nnf : thm > thm 
17849  20 
val make_nnf1 : thm > thm 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

21 
val skolemize : thm > thm 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

22 
val make_clauses : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

23 
val make_horns : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

24 
val best_prolog_tac : (thm > int) > thm list > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

25 
val depth_prolog_tac : thm list > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

26 
val gocls : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

27 
val skolemize_prems_tac : thm list > int > tactic 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

28 
val MESON : (thm list > thm list) > (thm list > tactic) > int > tactic 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

29 
val best_meson_tac : (thm > int) > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

30 
val safe_best_meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

31 
val depth_meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

32 
val prolog_step_tac' : thm list > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

33 
val iter_deepen_prolog_tac : thm list > tactic 
16563  34 
val iter_deepen_meson_tac : thm list > int > tactic 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

35 
val meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

36 
val negate_head : thm > thm 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

37 
val select_literal : int > thm > thm 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

38 
val skolemize_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

39 
end 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

40 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

41 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

42 
structure Meson = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

43 
struct 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

44 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

45 
val not_conjD = thm "meson_not_conjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

46 
val not_disjD = thm "meson_not_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

47 
val not_notD = thm "meson_not_notD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

48 
val not_allD = thm "meson_not_allD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

49 
val not_exD = thm "meson_not_exD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

50 
val imp_to_disjD = thm "meson_imp_to_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

51 
val not_impD = thm "meson_not_impD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

52 
val iff_to_disjD = thm "meson_iff_to_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

53 
val not_iffD = thm "meson_not_iffD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

54 
val conj_exD1 = thm "meson_conj_exD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

55 
val conj_exD2 = thm "meson_conj_exD2"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

56 
val disj_exD = thm "meson_disj_exD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

57 
val disj_exD1 = thm "meson_disj_exD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

58 
val disj_exD2 = thm "meson_disj_exD2"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

59 
val disj_assoc = thm "meson_disj_assoc"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

60 
val disj_comm = thm "meson_disj_comm"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

61 
val disj_FalseD1 = thm "meson_disj_FalseD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

62 
val disj_FalseD2 = thm "meson_disj_FalseD2"; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

63 

16563  64 
val depth_limit = ref 2000; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

65 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

66 
(**** Operators for forward proof ****) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

67 

20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

68 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

69 
(** Firstorder Resolution **) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

70 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

71 
fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty); 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

72 
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

73 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

74 
val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

75 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

76 
(*FIXME: currently does not "rename variables apart"*) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

77 
fun first_order_resolve thA thB = 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

78 
let val thy = theory_of_thm thA 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

79 
val tmA = concl_of thA 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

80 
val Const("==>",_) $ tmB $ _ = prop_of thB 
23440
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

81 
val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0) 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

82 
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

83 
in thA RS (cterm_instantiate ct_pairs thB) end 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

84 
handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); 
18175
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset

85 

23440
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

86 
fun flexflex_first_order th = 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

87 
case (tpairs_of th) of 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

88 
[] => th 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

89 
 pairs => 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

90 
let val thy = theory_of_thm th 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

91 
val (tyenv,tenv) = 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

92 
foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

93 
val t_pairs = map term_pair_of (Vartab.dest tenv) 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

94 
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

95 
in th' end 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

96 
handle THM _ => th; 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

97 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

98 
(*raises exception if no rules apply  unlike RL*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

99 
fun tryres (th, rls) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

100 
let fun tryall [] = raise THM("tryres", 0, th::rls) 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

101 
 tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

102 
in tryall rls end; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

103 

21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

104 
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st, 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

105 
e.g. from conj_forward, should have the form 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

106 
"[ P' ==> ?P; Q' ==> ?Q ] ==> ?P & ?Q" 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

107 
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

108 
fun forward_res nf st = 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

109 
let fun forward_tacf [prem] = rtac (nf prem) 1 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

110 
 forward_tacf prems = 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

111 
error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

112 
string_of_thm st ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

113 
"\nPremises:\n" ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

114 
cat_lines (map string_of_thm prems)) 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

115 
in 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

116 
case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st) 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

117 
of SOME(th,_) => th 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

118 
 NONE => raise THM("forward_res", 0, [st]) 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

119 
end; 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

120 

20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

121 
(*Are any of the logical connectives in "bs" present in the term?*) 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

122 
fun has_conns bs = 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

123 
let fun has (Const(a,_)) = false 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

124 
 has (Const("Trueprop",_) $ p) = has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

125 
 has (Const("Not",_) $ p) = has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

126 
 has (Const("op ",_) $ p $ q) = member (op =) bs "op " orelse has p orelse has q 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

127 
 has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

128 
 has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

129 
 has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

130 
 has _ = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

131 
in has end; 
17716  132 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

133 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

134 
(**** Clause handling ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

135 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

136 
fun literals (Const("Trueprop",_) $ P) = literals P 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

137 
 literals (Const("op ",_) $ P $ Q) = literals P @ literals Q 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

138 
 literals (Const("Not",_) $ P) = [(false,P)] 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

139 
 literals P = [(true,P)]; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

140 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

141 
(*number of literals in a term*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

142 
val nliterals = length o literals; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

143 

18389  144 

145 
(*** Tautology Checking ***) 

146 

147 
fun signed_lits_aux (Const ("op ", _) $ P $ Q) (poslits, neglits) = 

148 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 

149 
 signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) 

150 
 signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); 

151 

152 
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); 

153 

154 
(*Literals like X=X are tautologous*) 

155 
fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u 

156 
 taut_poslit (Const("True",_)) = true 

157 
 taut_poslit _ = false; 

158 

159 
fun is_taut th = 

160 
let val (poslits,neglits) = signed_lits th 

161 
in exists taut_poslit poslits 

162 
orelse 

20073  163 
exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) 
19894  164 
end 
165 
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) 

18389  166 

167 

168 
(*** To remove trivial negated equality literals from clauses ***) 

169 

170 
(*They are typically functional reflexivity axioms and are the converses of 

171 
injectivity equivalences*) 

172 

173 
val not_refl_disj_D = thm"meson_not_refl_disj_D"; 

174 

20119  175 
(*Is either term a Var that does not properly occur in the other term?*) 
176 
fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) 

177 
 eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) 

178 
 eliminable _ = false; 

179 

18389  180 
fun refl_clause_aux 0 th = th 
181 
 refl_clause_aux n th = 

182 
case HOLogic.dest_Trueprop (concl_of th) of 

183 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _) => 

184 
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) 

185 
 (Const ("op ", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 

20119  186 
if eliminable(t,u) 
187 
then refl_clause_aux (n1) (th RS not_refl_disj_D) (*Var inequation: delete*) 

18389  188 
else refl_clause_aux (n1) (th RS disj_comm) (*not between Vars: ignore*) 
189 
 (Const ("op ", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) 

18752
c9c6ae9e8b88
Clausification now handles some IFs in rewrite rules (ifsplit did not work)
paulson
parents:
18708
diff
changeset

190 
 _ => (*not a disjunction*) th; 
18389  191 

192 
fun notequal_lits_count (Const ("op ", _) $ P $ Q) = 

193 
notequal_lits_count P + notequal_lits_count Q 

194 
 notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 

195 
 notequal_lits_count _ = 0; 

196 

197 
(*Simplify a clause by applying reflexivity to its negated equality literals*) 

198 
fun refl_clause th = 

199 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 

19894  200 
in zero_var_indexes (refl_clause_aux neqs th) end 
201 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 

18389  202 

203 

204 
(*** The basic CNF transformation ***) 

205 

21900  206 
val max_clauses = ref 40; 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

207 

e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

208 
fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses; 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

209 
fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses; 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

210 

19894  211 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

212 
fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

213 
 signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

214 
 signed_nclauses b (Const("op &",_) $ t $ u) = 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

215 
if b then sum (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

216 
else prod (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

217 
 signed_nclauses b (Const("op ",_) $ t $ u) = 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

218 
if b then prod (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

219 
else sum (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

220 
 signed_nclauses b (Const("op >",_) $ t $ u) = 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

221 
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

222 
else sum (signed_nclauses (not b) t) (signed_nclauses b u) 
21616
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

223 
 signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

224 
if T = HOLogic.boolT then (*Boolean equality is ifandonlyif*) 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

225 
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

226 
(prod (signed_nclauses (not b) u) (signed_nclauses b t)) 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

227 
else sum (prod (signed_nclauses b t) (signed_nclauses b u)) 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

228 
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) 
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

229 
else 1 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

230 
 signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

231 
 signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

232 
 signed_nclauses _ _ = 1; (* literal *) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

233 

e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

234 
val nclauses = signed_nclauses true; 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

235 

e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

236 
fun too_many_clauses t = nclauses t >= !max_clauses; 
19894  237 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

238 
(*Replaces universally quantified variables by FREE variables  because 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

239 
assumptions may not contain scheme variables. Later, we call "generalize". *) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

240 
fun freeze_spec th = 
20361  241 
let val newname = gensym "mes_" 
19154  242 
val spec' = read_instantiate [("x", newname)] spec 
243 
in th RS spec' end; 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

244 

15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

245 
(*Used with METAHYPS below. There is one assumption, which gets bound to prem 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

246 
and then normalized via function nf. The normal form is given to resolve_tac, 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

247 
instantiate a Boolean variable created by resolution with disj_forward. Since 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

248 
(nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

249 
fun resop nf [prem] = resolve_tac (nf prem) 1; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

250 

20822
634070b40731
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
paulson
parents:
20524
diff
changeset

251 
(*Any need to extend this list with 
23262  252 
"HOL.type_class","HOL.eq_class","ProtoPure.term"?*) 
18389  253 
val has_meta_conn = 
22871  254 
exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1); 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

255 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

256 
fun apply_skolem_ths (th, rls) = 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

257 
let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

258 
 tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

259 
in tryall rls end; 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

260 

15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

261 
(*Conjunctive normal form, adding clauses from th in front of ths (for foldr). 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

262 
Strips universal quantifiers and breaks up conjunctions. 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

263 
Eliminates existential quantifiers using skoths: Skolemization theorems.*) 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

264 
fun cnf skoths (th,ths) = 
18389  265 
let fun cnf_aux (th,ths) = 
21174
4d733b76b5fa
removed is_Trueprop (use can dest_Trueprop'' instead);
wenzelm
parents:
21102
diff
changeset

266 
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*metalevel: ignore*) 
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

267 
else if not (has_conns ["All","Ex","op &"] (prop_of th)) 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

268 
then th::ths (*no work to do, terminate*) 
16588  269 
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of 
270 
Const ("op &", _) => (*conjunction*) 

20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

271 
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) 
16588  272 
 Const ("All", _) => (*universal quantifier*) 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

273 
cnf_aux (freeze_spec th, ths) 
16588  274 
 Const ("Ex", _) => 
275 
(*existential quantifier: Insert Skolem functions*) 

20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

276 
cnf_aux (apply_skolem_ths (th,skoths), ths) 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

277 
 Const ("op ", _) => 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

278 
(*Disjunction of P, Q: Create new goal of proving ?P  ?Q and solve it using 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

279 
all combinations of converting P, Q to CNF.*) 
16588  280 
let val tac = 
18389  281 
(METAHYPS (resop cnf_nil) 1) THEN 
19154  282 
(fn st' => st' > METAHYPS (resop cnf_nil) 1) 
16588  283 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 
284 
 _ => (*no work to do*) th::ths 

19154  285 
and cnf_nil th = cnf_aux (th,[]) 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

286 
in 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

287 
if too_many_clauses (concl_of th) 
22130  288 
then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths) 
19894  289 
else cnf_aux (th,ths) 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

290 
end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

291 

22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

292 
fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

293 
 all_names _ = []; 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

294 

f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

295 
fun new_names n [] = [] 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

296 
 new_names n (x::xs) = 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

297 
if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

298 
else new_names n xs; 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

299 

f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

300 
(*The gensym names are ugly, so don't let the user see them. When forall_elim_vars 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

301 
is called, it will ensure that no name clauses ensue.*) 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

302 
fun nice_names th = 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

303 
let val old_names = all_names (prop_of th) 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

304 
in Drule.rename_bvars (new_names 0 old_names) th end; 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

305 

16012  306 
(*Convert all suitable free variables to schematic variables, 
307 
but don't discharge assumptions.*) 

22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

308 
fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th))); 
16012  309 

20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

310 
fun make_cnf skoths th = cnf skoths (th, []); 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

311 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

312 
(*Generalization, removal of redundant equalities, removal of tautologies.*) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

313 
fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths); 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

314 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

315 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

316 
(**** Removal of duplicate literals ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

317 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

318 
(*Forward proof, passing extra assumptions as theorems to the tactic*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

319 
fun forward_res2 nf hyps st = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

320 
case Seq.pull 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

321 
(REPEAT 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

322 
(METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

323 
st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

324 
of SOME(th,_) => th 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

325 
 NONE => raise THM("forward_res2", 0, [st]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

326 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

327 
(*Remove duplicates in PQ by assuming ~P in Q 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

328 
rls (initially []) accumulates assumptions of the form P==>False*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

329 
fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

330 
handle THM _ => tryres(th,rls) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

331 
handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

332 
[disj_FalseD1, disj_FalseD2, asm_rl]) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

333 
handle THM _ => th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

334 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

335 
(*Remove duplicate literals, if there are any*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

336 
fun nodups th = 
20972  337 
if has_duplicates (op =) (literals (prop_of th)) 
338 
then nodups_aux [] th 

339 
else th; 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

340 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

341 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

342 
(**** Generation of contrapositives ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

343 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

344 
fun is_left (Const ("Trueprop", _) $ 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

345 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _)) = true 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

346 
 is_left _ = false; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

347 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

348 
(*Associate disjuctions to right  make leftmost disjunct a LITERAL*) 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

349 
fun assoc_right th = 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

350 
if is_left (prop_of th) then assoc_right (th RS disj_assoc) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

351 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

352 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

353 
(*Must check for negative literal first!*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

354 
val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

355 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

356 
(*For ordinary resolution. *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

357 
val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

358 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

359 
(*Create a goal or support clause, conclusing False*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

360 
fun make_goal th = (*Must check for negative literal first!*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

361 
make_goal (tryres(th, clause_rules)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

362 
handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

363 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

364 
(*Sort clauses by number of literals*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

365 
fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

366 

18389  367 
fun sort_clauses ths = sort (make_ord fewerlits) ths; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

368 

15581  369 
(*True if the given type contains bool anywhere*) 
370 
fun has_bool (Type("bool",_)) = true 

371 
 has_bool (Type(_, Ts)) = exists has_bool Ts 

372 
 has_bool _ = false; 

373 

20524
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

374 
(*Is the string the name of a connective? Really only  and Not can remain, 
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

375 
since this code expects to be called on a clause form.*) 
19875  376 
val is_conn = member (op =) 
20524
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

377 
["Trueprop", "op &", "op ", "op >", "Not", 
15613  378 
"All", "Ex", "Ball", "Bex"]; 
379 

20524
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

380 
(*True if the term contains a functionnot a logical connectivewhere the type 
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

381 
of any argument contains bool.*) 
15613  382 
val has_bool_arg_const = 
383 
exists_Const 

384 
(fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); 

22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

385 

cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

386 
(*A higherorder instance of a firstorder constant? Example is the definition of 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

387 
HOL.one, 1, at a function type in theory SetsAndFunctions.*) 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

388 
fun higher_inst_const thy (c,T) = 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

389 
case binder_types T of 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

390 
[] => false (*not a function type, OK*) 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

391 
 Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

392 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

393 
(*Raises an exception if any Vars in the theorem mention type bool. 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

394 
Also rejects functions whose arguments are Booleans or other functions.*) 
22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

395 
fun is_fol_term thy t = 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

396 
Term.is_first_order ["all","All","Ex"] t andalso 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

397 
not (exists (has_bool o fastype_of) (term_vars t) orelse 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

398 
has_bool_arg_const t orelse 
22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

399 
exists_Const (higher_inst_const thy) t orelse 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

400 
has_meta_conn t); 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

401 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

402 
fun rigid t = not (is_Var (head_of t)); 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

403 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

404 
fun ok4horn (Const ("Trueprop",_) $ (Const ("op ", _) $ t $ _)) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

405 
 ok4horn (Const ("Trueprop",_) $ t) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

406 
 ok4horn _ = false; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

407 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

408 
(*Create a metalevel Horn clause*) 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

409 
fun make_horn crules th = 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

410 
if ok4horn (concl_of th) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

411 
then make_horn crules (tryres(th,crules)) handle THM _ => th 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

412 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

413 

16563  414 
(*Generate Horn clauses for all contrapositives of a clause. The input, th, 
415 
is a HOL disjunction.*) 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

416 
fun add_contras crules (th,hcs) = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

417 
let fun rots (0,th) = hcs 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

418 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

419 
rots(k1, assoc_right (th RS disj_comm)) 
15862  420 
in case nliterals(prop_of th) of 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

421 
1 => th::hcs 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

422 
 n => rots(n, assoc_right th) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

423 
end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

424 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

425 
(*Use "theorem naming" to label the clauses*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

426 
fun name_thms label = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

427 
let fun name1 (th, (k,ths)) = 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21616
diff
changeset

428 
(k1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

429 
in fn ths => #2 (foldr name1 (length ths, []) ths) end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

430 

16563  431 
(*Is the given disjunction an allnegative support clause?*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

432 
fun is_negative th = forall (not o #1) (literals (prop_of th)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

433 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

434 
val neg_clauses = List.filter is_negative; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

435 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

436 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

437 
(***** MESON PROOF PROCEDURE *****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

438 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

439 
fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

440 
As) = rhyps(phi, A::As) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

441 
 rhyps (_, As) = As; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

442 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

443 
(** Detecting repeated assumptions in a subgoal **) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

444 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

445 
(*The stringtree detects repeated assumptions.*) 
16801  446 
fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

447 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

448 
(*detects repetitions in a list of terms*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

449 
fun has_reps [] = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

450 
 has_reps [_] = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

451 
 has_reps [t,u] = (t aconv u) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

452 
 has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) 
19875  453 
handle Net.INSERT => true; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

454 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

455 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  456 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
457 
 TRYING_eq_assume_tac i st = 

458 
TRYING_eq_assume_tac (i1) (eq_assumption i st) 

459 
handle THM _ => TRYING_eq_assume_tac (i1) st; 

460 

461 
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st; 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

462 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

463 
(*Loop checking: FAIL if trying to prove the same thing twice 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

464 
 if *ANY* subgoal has repeated literals*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

465 
fun check_tac st = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

466 
if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

467 
then Seq.empty else Seq.single st; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

468 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

469 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

470 
(* net_resolve_tac actually made it slower... *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

471 
fun prolog_step_tac horns i = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

472 
(assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN 
18508  473 
TRYALL_eq_assume_tac; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

474 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

475 
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

476 
fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

477 

32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

478 
fun size_of_subgoals st = foldr addconcl 0 (prems_of st); 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

479 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

480 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

481 
(*Negation Normal Form*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

482 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  483 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  484 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

485 
fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

486 
 ok4nnf (Const ("Trueprop",_) $ t) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

487 
 ok4nnf _ = false; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

488 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

489 
fun make_nnf1 th = 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

490 
if ok4nnf (concl_of th) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

491 
then make_nnf1 (tryres(th, nnf_rls)) 
9869  492 
handle THM _ => 
15581  493 
forward_res make_nnf1 
9869  494 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

495 
handle THM _ => th 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

496 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

497 

20018  498 
(*The simplification removes defined quantifiers and occurrences of True and False. 
499 
nnf_ss also includes the onepoint simprocs, 

18405
afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

500 
which are needed to avoid the various onepoint theorems from generating junk clauses.*) 
19894  501 
val nnf_simps = 
20018  502 
[simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
19894  503 
if_False, if_cancel, if_eq_cancel, cases_simp]; 
504 
val nnf_extra_simps = 

505 
thms"split_ifs" @ ex_simps @ all_simps @ simp_thms; 

18405
afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

506 

afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

507 
val nnf_ss = 
19894  508 
HOL_basic_ss addsimps nnf_extra_simps 
509 
addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; 

15872  510 

21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

511 
fun make_nnf th = case prems_of th of 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

512 
[] => th > rewrite_rule (map safe_mk_meta_eq nnf_simps) 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

513 
> simplify nnf_ss 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

514 
> make_nnf1 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

515 
 _ => raise THM ("make_nnf: premises in argument", 0, [th]); 
15581  516 

15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15946
diff
changeset

517 
(*Pull existential quantifiers to front. This accomplishes Skolemization for 
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15946
diff
changeset

518 
clauses that arise from a subgoal.*) 
9869  519 
fun skolemize th = 
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

520 
if not (has_conns ["Ex"] (prop_of th)) then th 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

521 
else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2, 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15653
diff
changeset

522 
disj_exD, disj_exD1, disj_exD2]))) 
9869  523 
handle THM _ => 
524 
skolemize (forward_res skolemize 

525 
(tryres (th, [conj_forward, disj_forward, all_forward]))) 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

526 
handle THM _ => forward_res skolemize (th RS ex_forward); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

527 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

528 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

529 
(*Make clauses from a list of theorems, previously Skolemized and put into nnf. 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

530 
The resulting clauses are HOL disjunctions.*) 
9869  531 
fun make_clauses ths = 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

532 
(sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths))); 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

533 

16563  534 
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) 
9869  535 
fun make_horns ths = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

536 
name_thms "Horn#" 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22130
diff
changeset

537 
(distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

538 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

539 
(*Could simply use nprems_of, which would count remaining subgoals  no 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

540 
discrimination as to their size! With BEST_FIRST, fails for problem 41.*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

541 

9869  542 
fun best_prolog_tac sizef horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

543 
BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

544 

9869  545 
fun depth_prolog_tac horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

546 
DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

547 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

548 
(*Return all negative clauses, as possible goal clauses*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

549 
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

550 

15008  551 
fun skolemize_prems_tac prems = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

552 
cut_facts_tac (map (skolemize o make_nnf) prems) THEN' 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

553 
REPEAT o (etac exE); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

554 

22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

555 
(*Basis of all mesontactics. Supplies cltac with clauses: HOL disjunctions. 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

556 
Function mkcl converts theorems to clauses.*) 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

557 
fun MESON mkcl cltac i st = 
16588  558 
SELECT_GOAL 
23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23552
diff
changeset

559 
(EVERY [ObjectLogic.atomize_prems_tac 1, 
23552  560 
rtac ccontr 1, 
16588  561 
METAHYPS (fn negs => 
562 
EVERY1 [skolemize_prems_tac negs, 

22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22646
diff
changeset

563 
METAHYPS (cltac o mkcl)]) 1]) i st 
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22646
diff
changeset

564 
handle THM _ => no_tac st; (*probably from make_meta_clause, not firstorder*) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

565 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

566 
(** Bestfirst search versions **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

567 

16563  568 
(*ths is a list of additional clauses (HOL disjunctions) to use.*) 
9869  569 
fun best_meson_tac sizef = 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

570 
MESON make_clauses 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

571 
(fn cls => 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

572 
THEN_BEST_FIRST (resolve_tac (gocls cls) 1) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

573 
(has_fewer_prems 1, sizef) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

574 
(prolog_step_tac (make_horns cls) 1)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

575 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

576 
(*First, breaks the goal into independent units*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

577 
val safe_best_meson_tac = 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23590
diff
changeset

578 
SELECT_GOAL (TRY (CLASET safe_tac) THEN 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

579 
TRYALL (best_meson_tac size_of_subgoals)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

580 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

581 
(** Depthfirst search version **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

582 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

583 
val depth_meson_tac = 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

584 
MESON make_clauses 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

585 
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

586 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

587 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

588 
(** Iterative deepening version **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

589 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

590 
(*This version does only one inference per call; 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

591 
having only one eq_assume_tac speeds it up!*) 
9869  592 
fun prolog_step_tac' horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

593 
let val (horn0s, hornps) = (*0 subgoals vs 1 or more*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

594 
take_prefix Thm.no_prems horns 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

595 
val nrtac = net_resolve_tac horns 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

596 
in fn i => eq_assume_tac i ORELSE 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

597 
match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

598 
((assume_tac i APPEND nrtac i) THEN check_tac) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

599 
end; 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

600 

9869  601 
fun iter_deepen_prolog_tac horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

602 
ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

603 

22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

604 
fun iter_deepen_meson_tac ths = MESON make_clauses 
21095  605 
(fn cls => 
606 
case (gocls (cls@ths)) of 

607 
[] => no_tac (*no goal clauses*) 

608 
 goes => 

609 
let val horns = make_horns (cls@ths) 

22130  610 
val _ = 
611 
Output.debug (fn () => ("meson method called:\n" ^ 

21095  612 
space_implode "\n" (map string_of_thm (cls@ths)) ^ 
613 
"\nclauses:\n" ^ 

22130  614 
space_implode "\n" (map string_of_thm horns))) 
21095  615 
in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) 
616 
end 

617 
); 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

618 

16563  619 
fun meson_claset_tac ths cs = 
620 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); 

9869  621 

16563  622 
val meson_tac = CLASET' (meson_claset_tac []); 
9869  623 

624 

14813  625 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  626 

15008  627 
(*Convert a list of clauses (disjunctions) to metalevel clauses (==>), 
628 
with no contrapositives, for ordinary resolution.*) 

14744  629 

630 
(*Rules to convert the head literal into a negated assumption. If the head 

631 
literal is already negated, then using notEfalse instead of notEfalse' 

632 
prevents a double negation.*) 

633 
val notEfalse = read_instantiate [("R","False")] notE; 

634 
val notEfalse' = rotate_prems 1 notEfalse; 

635 

15448  636 
fun negated_asm_of_head th = 
14744  637 
th RS notEfalse handle THM _ => th RS notEfalse'; 
638 

639 
(*Converting one clause*) 

22646  640 
val make_meta_clause = 
641 
zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules; 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

642 

14744  643 
fun make_meta_clauses ths = 
644 
name_thms "MClause#" 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22130
diff
changeset

645 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  646 

647 
(*Permute a rule's premises to move the ith premise to the last position.*) 

648 
fun make_last i th = 

649 
let val n = nprems_of th 

650 
in if 1 <= i andalso i <= n 

651 
then Thm.permute_prems (i1) 1 th 

15118  652 
else raise THM("select_literal", i, [th]) 
14744  653 
end; 
654 

655 
(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing 

656 
doublenegations.*) 

657 
val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection]; 

658 

659 
(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i1),P(i+1),...Pn] ==> ~P*) 

660 
fun select_literal i cl = negate_head (make_last i cl); 

661 

18508  662 

14813  663 
(*Toplevel Skolemization. Allows part of the conversion to clauses to be 
664 
expressed as a tactic (or Isar method). Each assumption of the selected 

665 
goal is converted to NNF and then its existential quantifiers are pulled 

666 
to the front. Finally, all existential quantifiers are eliminated, 

667 
leaving !!quantified variables. Perhaps Safe_tac should follow, but it 

668 
might generate many subgoals.*) 

18194
940515d2fa26
 removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
mengj
parents:
18175
diff
changeset

669 

19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

670 
fun skolemize_tac i st = 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

671 
let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i1)) 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

672 
in 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

673 
EVERY' [METAHYPS 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

674 
(fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 
14813  675 
THEN REPEAT (etac exE 1))), 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

676 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

677 
end 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

678 
handle Subscript => Seq.empty; 
18194
940515d2fa26
 removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
mengj
parents:
18175
diff
changeset

679 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

680 
end; 
9869  681 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

682 
structure BasicMeson: BASIC_MESON = Meson; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

683 
open BasicMeson; 