author  paulson 
Wed, 27 Apr 2005 16:40:27 +0200  
changeset 15862  67574c1b15a0 
parent 15779  aed221aff642 
child 15872  8336ff711d80 
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)); 

220 

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

15581  224 
fun check_no_bool th = 
15613  225 
let val {prop,...} = rep_thm th 
226 
in if exists (has_bool o fastype_of) (term_vars prop) orelse 

227 
has_bool_arg_const prop 

228 
then raise THM ("check_no_bool", 0, [th]) else th 

229 
end; 

15581  230 

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

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

232 
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

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

234 

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

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

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

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

238 
 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

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

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

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

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

244 

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

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

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

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

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

249 

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

250 
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

251 

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

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

253 
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

254 

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

255 
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

256 

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

257 

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

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

259 

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

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

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

262 
 rhyps (_, As) = As; 
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 
(** 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

265 

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

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

267 
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

268 

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

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

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

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

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

273 
 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

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

275 

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

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

277 
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

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

279 
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

280 
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

281 

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

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

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

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

285 
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

286 
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

287 

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

288 

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

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

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

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

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

293 

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

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

295 
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

296 

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

297 
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

298 

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

299 

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

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

301 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  302 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  303 

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

9869  305 
handle THM _ => 
15581  306 
forward_res make_nnf1 
9869  307 
(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

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

309 

15581  310 
fun make_nnf th = make_nnf1 (check_no_bool th); 
311 

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

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

314 
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

315 
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

316 
disj_exD, disj_exD1, disj_exD2]))) 
9869  317 
handle THM _ => 
318 
skolemize (forward_res skolemize 

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

320 
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

321 

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

322 

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

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

324 
The resulting clauses are HOL disjunctions.*) 
9869  325 
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

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

327 

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

328 

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

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

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

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

333 

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

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

335 
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

336 

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

338 
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

339 

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

341 
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

342 

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

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

344 
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

345 

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

346 

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

348 
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

349 
REPEAT o (etac exE); 
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 
(*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

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

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

354 
METAHYPS (fn negs => 
15008  355 
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

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

357 

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

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

359 

9869  360 
fun best_meson_tac sizef = 
361 
MESON (fn cls => 

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

362 
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

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

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

365 

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

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

367 
val safe_best_meson_tac = 
9869  368 
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

369 
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

370 

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

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

372 

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

373 
val depth_meson_tac = 
9869  374 
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

375 
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

376 

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

377 

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 
(** Iterative deepening 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 
(*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

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

384 
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

385 
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

386 
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

387 
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

388 
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

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

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

391 

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

393 
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

394 

9869  395 
val iter_deepen_meson_tac = 
396 
MESON (fn cls => 

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

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

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

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

400 

9869  401 
fun meson_claset_tac cs = 
402 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac); 

403 

404 
val meson_tac = CLASET' meson_claset_tac; 

405 

406 

14813  407 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  408 

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

14744  411 

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

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

414 
prevents a double negation.*) 

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

416 
val notEfalse' = rotate_prems 1 notEfalse; 

417 

15448  418 
fun negated_asm_of_head th = 
14744  419 
th RS notEfalse handle THM _ => th RS notEfalse'; 
420 

421 
(*Converting one clause*) 

15581  422 
fun make_meta_clause th = 
423 
negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th)); 

14744  424 

425 
fun make_meta_clauses ths = 

426 
name_thms "MClause#" 

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

428 

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

430 
fun make_last i th = 

431 
let val n = nprems_of th 

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

433 
then Thm.permute_prems (i1) 1 th 

15118  434 
else raise THM("select_literal", i, [th]) 
14744  435 
end; 
436 

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

438 
doublenegations.*) 

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

440 

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

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

443 

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

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

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

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

449 
might generate many subgoals.*) 

450 
val skolemize_tac = 

451 
SUBGOAL 

452 
(fn (prop,_) => 

453 
let val ts = Logic.strip_assums_hyp prop 

454 
in EVERY1 

455 
[METAHYPS 

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

456 
(fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 
14813  457 
THEN REPEAT (etac exE 1))), 
458 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 

459 
end); 

460 

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

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

15008  464 
val make_clauses_tac = 
465 
SUBGOAL 

466 
(fn (prop,_) => 

467 
let val ts = Logic.strip_assums_hyp prop 

468 
in EVERY1 

469 
[METAHYPS 

470 
(fn hyps => 

15151  471 
(Method.insert_tac 
15118  472 
(map forall_intr_vars 
473 
(make_meta_clauses (make_clauses hyps))) 1)), 

15008  474 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 
475 
end); 

476 

14744  477 

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

478 
(*** proof method setup ***) 
9869  479 

480 
fun meson_meth ctxt = 

10821  481 
Method.SIMPLE_METHOD' HEADGOAL 
15032  482 
(CHANGED_PROP o meson_claset_tac (local_claset_of ctxt)); 
9869  483 

14890  484 
val skolemize_meth = 
485 
Method.SIMPLE_METHOD' HEADGOAL 

486 
(CHANGED_PROP o skolemize_tac); 

487 

15008  488 
val make_clauses_meth = 
489 
Method.SIMPLE_METHOD' HEADGOAL 

490 
(CHANGED_PROP o make_clauses_tac); 

491 

9869  492 

493 
val meson_setup = 

494 
[Method.add_methods 

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

14890  497 
("skolemize", Method.no_args skolemize_meth, 
15008  498 
"Skolemization into existential quantifiers"), 
499 
("make_clauses", Method.no_args make_clauses_meth, 

15118  500 
"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

501 

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

502 
end; 
9869  503 

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

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

505 
open BasicMeson; 