author  paulson 
Mon, 02 May 2005 16:28:33 +0200  
changeset 15908  f45296bb1485 
parent 15872  8336ff711d80 
child 15946  94e5f157ab09 
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 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

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

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

21 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

37 
val meson_setup : (theory > theory) list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

39 

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

40 

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

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

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

43 

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

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

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

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

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

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

49 
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

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

51 
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

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

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

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

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

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

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

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

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

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

61 
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

62 

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

63 

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

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

65 

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

66 
(*raises exception if no rules apply  unlike RL*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

68 
 tryres (th, []) = raise THM("tryres", 0, [th]); 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

69 

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

70 
(*Permits forward proof from rules that discharge assumptions*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

72 
case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

74 
 NONE => raise THM("forward_res", 0, [st]); 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

75 

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

76 

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

77 
(*Are any of the constants in "bs" present in the term?*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

79 
let fun has (Const(a,_)) = a mem bs 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

80 
 has (Const ("Hilbert_Choice.Eps",_) $ _) = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

81 
(*ignore constants within @terms*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

82 
 has (f$u) = has f orelse has u 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

83 
 has (Abs(_,_,t)) = has t 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

86 

15736  87 
(* for tracing: encloses each string element in brackets. *) 
88 
fun concat_with_and [] = "" 

89 
 concat_with_and [x] = "(" ^ x ^ ")" 

90 
 concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs; 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15653
diff
changeset

91 

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

92 

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

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

94 

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

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

96 
 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

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

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

99 

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

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

101 
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

102 

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

103 
(*to detect, and remove, tautologous clauses*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

105 
 taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

106 

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

107 
(*Include False as a literal: an occurrence of ~False is a tautology*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

108 
fun is_taut th = taut_lits ((true, HOLogic.false_const) :: 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

109 
literals (prop_of th)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

110 

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

111 
(*Generation of unique names  maxidx cannot be relied upon to increase! 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

112 
Cannot rely on "variant", since variables might coincide when literals 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

113 
are joined to make a clause... 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

114 
19 chooses "U" as the first variable name*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

115 
val name_ref = ref 19; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

116 

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

117 
(*Replaces universally quantified variables by FREE variables  because 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

120 
let val sth = th RS spec 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

121 
val newname = (name_ref := !name_ref + 1; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

122 
radixstring(26, "A", !name_ref)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

123 
in read_instantiate [("x", newname)] sth end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

124 

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

125 
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

126 

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

127 
(*Conjunctive normal form, detecting tautologies early. 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

128 
Strips universal quantifiers and breaks up conjunctions. *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

129 
fun cnf_aux seen (th,ths) = 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

130 
if taut_lits (literals(prop_of th) @ seen) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

131 
then ths (*tautology ignored*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

132 
else if not (has_consts ["All","op &"] (prop_of th)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

133 
then th::ths (*no work to do, terminate*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

134 
else (*conjunction?*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

135 
cnf_aux seen (th RS conjunct1, 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

136 
cnf_aux seen (th RS conjunct2, ths)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

137 
handle THM _ => (*universal quant?*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

138 
cnf_aux seen (freeze_spec th, ths) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

139 
handle THM _ => (*disjunction?*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

141 
(METAHYPS (resop (cnf_nil seen)) 1) THEN 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

142 
(fn st' => st' > 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

143 
METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

144 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

145 
and cnf_nil seen th = (cnf_aux seen (th,[])) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

146 

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

147 
(*Toplevel call to cnf  it's safe to reset name_ref*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

148 
fun cnf (th,ths) = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

149 
(name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

150 
handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

151 

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

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

153 

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

154 
(*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

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

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

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

158 
(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

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

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

161 
 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

162 

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

163 
(*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

164 
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

165 
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

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

167 
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

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

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

170 

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

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

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

173 
if null(findrep(literals(prop_of th))) then th 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

175 

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

176 

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

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

178 

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

179 
(*Associate disjuctions to right  make leftmost disjunct a LITERAL*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

182 

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

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

184 
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

185 

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

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

187 
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

188 

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

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

190 
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

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

192 
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

193 

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

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

195 
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

196 

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

197 
(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

199 

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

200 
(*Convert all suitable free variables to schematic variables*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

201 
fun generalize th = forall_elim_vars 0 (forall_intr_frees th); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

202 

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

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

206 
 has_bool _ = false; 

207 

15613  208 
(*Is the string the name of a connective? It doesn't matter if this list is 
209 
incomplete, since when actually called, the only connectives likely to 

210 
remain are &  Not.*) 

211 
fun is_conn c = c mem_string 

212 
["Trueprop", "op &", "op ", "op >", "op =", "Not", 

213 
"All", "Ex", "Ball", "Bex"]; 

214 

215 
(*True if the term contains a function where the type of any argument contains 

216 
bool.*) 

217 
val has_bool_arg_const = 

218 
exists_Const 

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

15908  220 

221 
val has_meta_conn = 

222 
exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]); 

15613  223 

15581  224 
(*Raises an exception if any Vars in the theorem mention type bool. That would mean 
15613  225 
they are higherorder, and in addition, they could cause make_horn to loop! 
226 
Functions taking Boolean arguments are also rejected.*) 

15581  227 
fun check_no_bool th = 
15613  228 
let val {prop,...} = rep_thm th 
15908  229 
in if exists (has_bool o fastype_of) (term_vars prop) orelse 
230 
has_bool_arg_const prop orelse 

231 
has_meta_conn prop 

15613  232 
then raise THM ("check_no_bool", 0, [th]) else th 
233 
end; 

15581  234 

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

235 
(*Create a metalevel Horn clause*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

238 

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

239 
(*Generate Horn clauses for all contrapositives of a clause*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

242 
 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

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

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

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

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

248 

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

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

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

251 
let fun name1 (th, (k,ths)) = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

252 
(k1, Thm.name_thm (label ^ string_of_int k, th) :: ths) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

253 

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

254 
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

255 

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

256 
(*Find an allnegative support clause*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

257 
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

258 

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

259 
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

260 

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

261 

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

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

263 

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

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

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

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

267 

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

268 
(** 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

269 

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

270 
(*The stringtree detects repeated assumptions.*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

271 
fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

272 

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

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

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

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

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

277 
 has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

278 
handle INSERT => true; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

279 

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

280 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

281 
fun TRYALL_eq_assume_tac 0 st = Seq.single st 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

283 
TRYALL_eq_assume_tac (i1) (eq_assumption i st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

284 
handle THM _ => TRYALL_eq_assume_tac (i1) st; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

285 

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

286 
(*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

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

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

289 
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

290 
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

291 

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

292 

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

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

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

295 
(assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

297 

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

298 
(*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

299 
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

300 

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

301 
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

302 

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

303 

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

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

305 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  306 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  307 

308 
fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls)) 

9869  309 
handle THM _ => 
15581  310 
forward_res make_nnf1 
9869  311 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

313 

15872  314 
(*The simplification removes occurrences of True and False.*) 
315 
val nnf_ss = HOL_basic_ss addsimps Ball_def::Bex_def::simp_thms; 

316 

317 
fun make_nnf th = th > simplify nnf_ss 

318 
> check_no_bool > make_nnf1 

15581  319 

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

320 
(*Pull existential quantifiers (Skolemization)*) 
9869  321 
fun skolemize th = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

322 
if not (has_consts ["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

323 
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

324 
disj_exD, disj_exD1, disj_exD2]))) 
9869  325 
handle THM _ => 
326 
skolemize (forward_res skolemize 

327 
(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

328 
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

329 

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

330 

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

331 
(*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

332 
The resulting clauses are HOL disjunctions.*) 
9869  333 
fun make_clauses ths = 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

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

335 

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

336 

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

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

339 
name_thms "Horn#" 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

340 
(gen_distinct Drule.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

341 

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

342 
(*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

343 
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

344 

9869  345 
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

346 
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

347 

9869  348 
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

349 
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

350 

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

351 
(*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

352 
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

353 

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

354 

15008  355 
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

356 
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

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

358 

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

359 
(*Shell of all mesontactics. Supplies cltac with clauses: HOL disjunctions*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

360 
fun MESON cltac = SELECT_GOAL 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

361 
(EVERY1 [rtac ccontr, 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

362 
METAHYPS (fn negs => 
15008  363 
EVERY1 [skolemize_prems_tac negs, 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

364 
METAHYPS (cltac o make_clauses)])]); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

365 

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

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

367 

9869  368 
fun best_meson_tac sizef = 
369 
MESON (fn cls => 

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

370 
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

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

372 
(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

373 

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

374 
(*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

375 
val safe_best_meson_tac = 
9869  376 
SELECT_GOAL (TRY Safe_tac THEN 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

377 
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

378 

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

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

380 

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

381 
val depth_meson_tac = 
9869  382 
MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

384 

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

385 

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

386 

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

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

388 

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

389 
(*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

390 
having only one eq_assume_tac speeds it up!*) 
9869  391 
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

392 
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

393 
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

394 
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

395 
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

396 
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

397 
((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

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

399 

9869  400 
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

401 
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

402 

9869  403 
val iter_deepen_meson_tac = 
404 
MESON (fn cls => 

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

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

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

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

408 

9869  409 
fun meson_claset_tac cs = 
410 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac); 

411 

412 
val meson_tac = CLASET' meson_claset_tac; 

413 

414 

14813  415 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  416 

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

14744  419 

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

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

422 
prevents a double negation.*) 

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

424 
val notEfalse' = rotate_prems 1 notEfalse; 

425 

15448  426 
fun negated_asm_of_head th = 
14744  427 
th RS notEfalse handle THM _ => th RS notEfalse'; 
428 

429 
(*Converting one clause*) 

15581  430 
fun make_meta_clause th = 
431 
negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th)); 

14744  432 

433 
fun make_meta_clauses ths = 

434 
name_thms "MClause#" 

435 
(gen_distinct Drule.eq_thm_prop (map make_meta_clause ths)); 

436 

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

438 
fun make_last i th = 

439 
let val n = nprems_of th 

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

441 
then Thm.permute_prems (i1) 1 th 

15118  442 
else raise THM("select_literal", i, [th]) 
14744  443 
end; 
444 

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

446 
doublenegations.*) 

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

448 

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

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

451 

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

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

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

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

457 
might generate many subgoals.*) 

458 
val skolemize_tac = 

459 
SUBGOAL 

460 
(fn (prop,_) => 

461 
let val ts = Logic.strip_assums_hyp prop 

462 
in EVERY1 

463 
[METAHYPS 

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

464 
(fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 
14813  465 
THEN REPEAT (etac exE 1))), 
466 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 

467 
end); 

468 

15118  469 
(*Toplevel conversion to metalevel clauses. Each clause has 
470 
leading !!bound universal variables, to express generality. To get 

471 
disjunctions instead of metaclauses, remove "make_meta_clauses" below.*) 

15008  472 
val make_clauses_tac = 
473 
SUBGOAL 

474 
(fn (prop,_) => 

475 
let val ts = Logic.strip_assums_hyp prop 

476 
in EVERY1 

477 
[METAHYPS 

478 
(fn hyps => 

15151  479 
(Method.insert_tac 
15118  480 
(map forall_intr_vars 
481 
(make_meta_clauses (make_clauses hyps))) 1)), 

15008  482 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 
483 
end); 

484 

14744  485 

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

486 
(*** proof method setup ***) 
9869  487 

488 
fun meson_meth ctxt = 

10821  489 
Method.SIMPLE_METHOD' HEADGOAL 
15032  490 
(CHANGED_PROP o meson_claset_tac (local_claset_of ctxt)); 
9869  491 

14890  492 
val skolemize_meth = 
493 
Method.SIMPLE_METHOD' HEADGOAL 

494 
(CHANGED_PROP o skolemize_tac); 

495 

15008  496 
val make_clauses_meth = 
497 
Method.SIMPLE_METHOD' HEADGOAL 

498 
(CHANGED_PROP o make_clauses_tac); 

499 

9869  500 

501 
val meson_setup = 

502 
[Method.add_methods 

14813  503 
[("meson", Method.ctxt_args meson_meth, 
504 
"The MESON resolution proof procedure"), 

14890  505 
("skolemize", Method.no_args skolemize_meth, 
15008  506 
"Skolemization into existential quantifiers"), 
507 
("make_clauses", Method.no_args make_clauses_meth, 

15118  508 
"Conversion to !!quantified metalevel clauses")]]; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

509 

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

510 
end; 
9869  511 

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

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

513 
open BasicMeson; 