author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 62519  a564458f94db 
child 67399  eab6ce8368fa 
permissions  rwrr 
50530  1 
(* Title: HOL/Library/refute.ML 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29004
diff
changeset

2 
Author: Tjark Weber, TU Muenchen 
14350  3 

14965  4 
Finite model generation for HOL formulas, using a SAT solver. 
14350  5 
*) 
6 

7 
signature REFUTE = 

8 
sig 

9 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

10 
exception REFUTE of string * string 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

11 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

12 
(*  *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

13 
(* Model/interpretation related code (translation HOL > propositional logic *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

14 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

15 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

16 
type params 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

17 
type interpretation 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

18 
type model 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

19 
type arguments 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

20 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

21 
exception MAXVARS_EXCEEDED 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

22 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

23 
val add_interpreter : string > (Proof.context > model > arguments > term > 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

24 
(interpretation * model * arguments) option) > theory > theory 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

25 
val add_printer : string > (Proof.context > model > typ > 
33243  26 
interpretation > (int > bool) > term option) > theory > theory 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

27 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

28 
val interpret : Proof.context > model > arguments > term > 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

29 
(interpretation * model * arguments) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

30 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

31 
val print : Proof.context > model > typ > interpretation > (int > bool) > term 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

32 
val print_model : Proof.context > model > (int > bool) > string 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

33 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

34 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

35 
(* Interface *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

36 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

37 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

38 
val set_default_param : (string * string) > theory > theory 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

39 
val get_default_param : Proof.context > string > string option 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

40 
val get_default_params : Proof.context > (string * string) list 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

41 
val actual_params : Proof.context > (string * string) list > params 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

42 

45387
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

43 
val find_model : 
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

44 
Proof.context > params > term list > term > bool > string 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

45 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

46 
(* tries to find a model for a formula: *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

47 
val satisfy_term : 
45387
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

48 
Proof.context > (string * string) list > term list > term > string 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

49 
(* tries to find a model that refutes a formula: *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

50 
val refute_term : 
45387
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

51 
Proof.context > (string * string) list > term list > term > string 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

52 
val refute_goal : 
45387
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

53 
Proof.context > (string * string) list > thm > int > string 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

54 

29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

55 
(*  *) 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

56 
(* Additional functions used by Nitpick (to be factored out) *) 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

57 
(*  *) 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

58 

33243  59 
val get_classdef : theory > string > (string * term) option 
60 
val norm_rhs : term > term 

61 
val get_def : theory > string * typ > (string * term) option 

62 
val get_typedef : theory > typ > (string * term) option 

63 
val is_IDT_constructor : theory > string * typ > bool 

64 
val is_IDT_recursor : theory > string * typ > bool 

65 
val is_const_of_class: theory > string * typ > bool 

66 
val string_of_typ : typ > string 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

67 
end; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

68 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

69 
structure Refute : REFUTE = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

70 
struct 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

71 

41471  72 
open Prop_Logic; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

73 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

74 
(* We use 'REFUTE' only for internal error conditions that should *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

75 
(* never occur in the first place (i.e. errors caused by bugs in our *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

76 
(* code). Otherwise (e.g. to indicate invalid input data) we use *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

77 
(* 'error'. *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

78 
exception REFUTE of string * string; (* ("in function", "cause") *) 
14350  79 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

80 
(* should be raised by an interpreter when more variables would be *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

81 
(* required than allowed by 'maxvars' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

82 
exception MAXVARS_EXCEEDED; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

83 

14350  84 

85 
(*  *) 

86 
(* TREES *) 

87 
(*  *) 

88 

89 
(*  *) 

90 
(* tree: implements an arbitrarily (but finitely) branching tree as a list *) 

91 
(* of (lists of ...) elements *) 

92 
(*  *) 

93 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

94 
datatype 'a tree = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

95 
Leaf of 'a 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

96 
 Node of ('a tree) list; 
14350  97 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

98 
fun tree_map f tr = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

99 
case tr of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

100 
Leaf x => Leaf (f x) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

101 
 Node xs => Node (map (tree_map f) xs); 
14350  102 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

103 
fun tree_pair (t1, t2) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

104 
case t1 of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

105 
Leaf x => 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

106 
(case t2 of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

107 
Leaf y => Leaf (x,y) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

108 
 Node _ => raise REFUTE ("tree_pair", 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

109 
"trees are of different height (second tree is higher)")) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

110 
 Node xs => 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

111 
(case t2 of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

112 
(* '~~' will raise an exception if the number of branches in *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

113 
(* both trees is different at the current node *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

114 
Node ys => Node (map tree_pair (xs ~~ ys)) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

115 
 Leaf _ => raise REFUTE ("tree_pair", 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

116 
"trees are of different height (first tree is higher)")); 
14350  117 

118 
(*  *) 

14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

119 
(* params: parameters that control the translation into a propositional *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

120 
(* formula/model generation *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

121 
(* *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

122 
(* The following parameters are supported (and required (!), except for *) 
30314
853778f6ef7d
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
blanchet
parents:
30312
diff
changeset

123 
(* "sizes" and "expect"): *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

124 
(* *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

125 
(* Name Type Description *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

126 
(* *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

127 
(* "sizes" (string * int) list *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

128 
(* Size of ground types (e.g. 'a=2), or depth of IDTs. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

129 
(* "minsize" int If >0, minimal size of each ground type/IDT depth. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

130 
(* "maxsize" int If >0, maximal size of each ground type/IDT depth. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

131 
(* "maxvars" int If >0, use at most 'maxvars' Boolean variables *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

132 
(* when transforming the term into a propositional *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

133 
(* formula. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

134 
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

135 
(* "satsolver" string SAT solver to be used. *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

136 
(* "no_assms" bool If "true", assumptions in structured proofs are *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

137 
(* not considered. *) 
30314
853778f6ef7d
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
blanchet
parents:
30312
diff
changeset

138 
(* "expect" string Expected result ("genuine", "potential", "none", or *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

139 
(* "unknown"). *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

140 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

141 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

142 
type params = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

143 
{ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

144 
sizes : (string * int) list, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

145 
minsize : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

146 
maxsize : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

147 
maxvars : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

148 
maxtime : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

149 
satsolver: string, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

150 
no_assms : bool, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

151 
expect : string 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

152 
}; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

153 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

154 
(*  *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

155 
(* interpretation: a term's interpretation is given by a variable of type *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

156 
(* 'interpretation' *) 
14350  157 
(*  *) 
158 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

159 
type interpretation = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

160 
prop_formula list tree; 
14350  161 

162 
(*  *) 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

163 
(* model: a model specifies the size of types and the interpretation of *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

164 
(* terms *) 
14350  165 
(*  *) 
166 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

167 
type model = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

168 
(typ * int) list * (term * interpretation) list; 
14350  169 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

170 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

171 
(* arguments: additional arguments required during interpretation of terms *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

172 
(*  *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

173 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

174 
type arguments = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

175 
{ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

176 
(* just passed unchanged from 'params': *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

177 
maxvars : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

178 
(* whether to use 'make_equality' or 'make_def_equality': *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

179 
def_eq : bool, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

180 
(* the following may change during the translation: *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

181 
next_idx : int, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

182 
bounds : interpretation list, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

183 
wellformed: prop_formula 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

184 
}; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

185 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

186 
structure Data = Theory_Data 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

187 
( 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

188 
type T = 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

189 
{interpreters: (string * (Proof.context > model > arguments > term > 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

190 
(interpretation * model * arguments) option)) list, 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

191 
printers: (string * (Proof.context > model > typ > interpretation > 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

192 
(int > bool) > term option)) list, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

193 
parameters: string Symtab.table}; 
46960  194 
val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

195 
val extend = I; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

196 
fun merge 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

197 
({interpreters = in1, printers = pr1, parameters = pa1}, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

198 
{interpreters = in2, printers = pr2, parameters = pa2}) : T = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

199 
{interpreters = AList.merge (op =) (K true) (in1, in2), 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

200 
printers = AList.merge (op =) (K true) (pr1, pr2), 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41471
diff
changeset

201 
parameters = Symtab.merge (op =) (pa1, pa2)}; 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

202 
); 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

203 

42361  204 
val get_data = Data.get o Proof_Context.theory_of; 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

205 

14350  206 

207 
(*  *) 

15334
d5a92997dc1b
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
webertj
parents:
15333
diff
changeset

208 
(* interpret: interprets the term 't' using a suitable interpreter; returns *) 
d5a92997dc1b
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
webertj
parents:
15333
diff
changeset

209 
(* the interpretation and a (possibly extended) model that keeps *) 
d5a92997dc1b
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
webertj
parents:
15333
diff
changeset

210 
(* track of the interpretation of subterms *) 
14350  211 
(*  *) 
212 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

213 
fun interpret ctxt model args t = 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

214 
case get_first (fn (_, f) => f ctxt model args t) 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

215 
(#interpreters (get_data ctxt)) of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

216 
NONE => raise REFUTE ("interpret", 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

217 
"no interpreter for term " ^ quote (Syntax.string_of_term ctxt t)) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

218 
 SOME x => x; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

219 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

220 
(*  *) 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

221 
(* print: converts the interpretation 'intr', which must denote a term of *) 
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

222 
(* type 'T', into a term using a suitable printer *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

223 
(*  *) 
14350  224 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

225 
fun print ctxt model T intr assignment = 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

226 
case get_first (fn (_, f) => f ctxt model T intr assignment) 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

227 
(#printers (get_data ctxt)) of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

228 
NONE => raise REFUTE ("print", 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

229 
"no printer for type " ^ quote (Syntax.string_of_typ ctxt T)) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

230 
 SOME x => x; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

231 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

232 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

233 
(* print_model: turns the model into a string, using a fixed interpretation *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

234 
(* (given by an assignment for Boolean variables) and suitable *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

235 
(* printers *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

236 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

237 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

238 
fun print_model ctxt model assignment = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

239 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

240 
val (typs, terms) = model 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

241 
val typs_msg = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

242 
if null typs then 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

243 
"empty universe (no type variables in term)\n" 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

244 
else 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

245 
"Size of types: " ^ commas (map (fn (T, i) => 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

246 
Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n" 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

247 
val show_consts_msg = 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
39049
diff
changeset

248 
if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
39049
diff
changeset

249 
"enable \"show_consts\" to show the interpretation of constants\n" 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

250 
else 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

251 
"" 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

252 
val terms_msg = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

253 
if null terms then 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

254 
"empty interpretation (no free variables in term)\n" 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

255 
else 
32952  256 
cat_lines (map_filter (fn (t, intr) => 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

257 
(* print constants only if 'show_consts' is true *) 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
39049
diff
changeset

258 
if Config.get ctxt show_consts orelse not (is_Const t) then 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

259 
SOME (Syntax.string_of_term ctxt t ^ ": " ^ 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

260 
Syntax.string_of_term ctxt 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

261 
(print ctxt model (Term.type_of t) intr assignment)) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

262 
else 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

263 
NONE) terms) ^ "\n" 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

264 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

265 
typs_msg ^ show_consts_msg ^ terms_msg 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

266 
end; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

267 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

268 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

269 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

270 
(* PARAMETER MANAGEMENT *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

271 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

272 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

273 
fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} => 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

274 
case AList.lookup (op =) interpreters name of 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

275 
NONE => {interpreters = (name, f) :: interpreters, 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

276 
printers = printers, parameters = parameters} 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

277 
 SOME _ => error ("Interpreter " ^ name ^ " already declared")); 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

278 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

279 
fun add_printer name f = Data.map (fn {interpreters, printers, parameters} => 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

280 
case AList.lookup (op =) printers name of 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

281 
NONE => {interpreters = interpreters, 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

282 
printers = (name, f) :: printers, parameters = parameters} 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

283 
 SOME _ => error ("Printer " ^ name ^ " already declared")); 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

284 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

285 
(*  *) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

286 
(* set_default_param: stores the '(name, value)' pair in Data's *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

287 
(* parameter table *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

288 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

289 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

290 
fun set_default_param (name, value) = Data.map 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

291 
(fn {interpreters, printers, parameters} => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

292 
{interpreters = interpreters, printers = printers, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

293 
parameters = Symtab.update (name, value) parameters}); 
14350  294 

295 
(*  *) 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

296 
(* get_default_param: retrieves the value associated with 'name' from *) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

297 
(* Data's parameter table *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

298 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

299 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

300 
val get_default_param = Symtab.lookup o #parameters o get_data; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

301 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

302 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

303 
(* get_default_params: returns a list of all '(name, value)' pairs that are *) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

304 
(* stored in Data's parameter table *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

305 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

306 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

307 
val get_default_params = Symtab.dest o #parameters o get_data; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

308 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

309 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

310 
(* actual_params: takes a (possibly empty) list 'params' of parameters that *) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

311 
(* override the default parameters currently specified, and *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

312 
(* returns a record that can be passed to 'find_model'. *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

313 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

314 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

315 
fun actual_params ctxt override = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

316 
let 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

317 
fun read_bool (parms, name) = 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

318 
case AList.lookup (op =) parms name of 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

319 
SOME "true" => true 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

320 
 SOME "false" => false 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

321 
 SOME s => error ("parameter " ^ quote name ^ 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

322 
" (value is " ^ quote s ^ ") must be \"true\" or \"false\"") 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

323 
 NONE => error ("parameter " ^ quote name ^ 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

324 
" must be assigned a value") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

325 
fun read_int (parms, name) = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

326 
case AList.lookup (op =) parms name of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

327 
SOME s => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

328 
(case Int.fromString s of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

329 
SOME i => i 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

330 
 NONE => error ("parameter " ^ quote name ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

331 
" (value is " ^ quote s ^ ") must be an integer value")) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

332 
 NONE => error ("parameter " ^ quote name ^ 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

333 
" must be assigned a value") 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

334 
fun read_string (parms, name) = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

335 
case AList.lookup (op =) parms name of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

336 
SOME s => s 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

337 
 NONE => error ("parameter " ^ quote name ^ 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

338 
" must be assigned a value") 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

339 
(* 'override' first, defaults last: *) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

340 
val allparams = override @ get_default_params ctxt 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

341 
val minsize = read_int (allparams, "minsize") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

342 
val maxsize = read_int (allparams, "maxsize") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

343 
val maxvars = read_int (allparams, "maxvars") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

344 
val maxtime = read_int (allparams, "maxtime") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

345 
val satsolver = read_string (allparams, "satsolver") 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

346 
val no_assms = read_bool (allparams, "no_assms") 
30314
853778f6ef7d
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
blanchet
parents:
30312
diff
changeset

347 
val expect = the_default "" (AList.lookup (op =) allparams "expect") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

348 
(* all remaining parameters of the form "string=int" are collected in *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

349 
(* 'sizes' *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

350 
(* TODO: it is currently not possible to specify a size for a type *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

351 
(* whose name is one of the other parameters (e.g. 'maxvars') *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

352 
(* (string * int) list *) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

353 
val sizes = map_filter 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

354 
(fn (name, value) => Option.map (pair name) (Int.fromString value)) 
33317  355 
(filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

356 
andalso name<>"maxvars" andalso name<>"maxtime" 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

357 
andalso name<>"satsolver" andalso name<>"no_assms") allparams) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

358 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

359 
{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

360 
maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect} 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

361 
end; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

362 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

363 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

364 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

365 
(* TRANSLATION HOL > PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT > MODEL *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

366 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

367 

58120  368 
fun typ_of_dtyp _ typ_assoc (Old_Datatype_Aux.DtTFree a) = 
369 
the (AList.lookup (op =) typ_assoc (Old_Datatype_Aux.DtTFree a)) 

370 
 typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtType (s, Us)) = 

55891
d1a9b07783ab
support 'datatype_new'defined datatypes in Nitpick + better support for 'codatatype's
blanchet
parents:
55507
diff
changeset

371 
Type (s, map (typ_of_dtyp descr typ_assoc) Us) 
58120  372 
 typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtRec i) = 
55891
d1a9b07783ab
support 'datatype_new'defined datatypes in Nitpick + better support for 'codatatype's
blanchet
parents:
55507
diff
changeset

373 
let val (s, ds, _) = the (AList.lookup (op =) descr i) in 
d1a9b07783ab
support 'datatype_new'defined datatypes in Nitpick + better support for 'codatatype's
blanchet
parents:
55507
diff
changeset

374 
Type (s, map (typ_of_dtyp descr typ_assoc) ds) 
d1a9b07783ab
support 'datatype_new'defined datatypes in Nitpick + better support for 'codatatype's
blanchet
parents:
55507
diff
changeset

375 
end 
d1a9b07783ab
support 'datatype_new'defined datatypes in Nitpick + better support for 'codatatype's
blanchet
parents:
55507
diff
changeset

376 

54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54556
diff
changeset

377 
val close_form = ATP_Util.close_form 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
42680
diff
changeset

378 
val specialize_type = ATP_Util.specialize_type 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

379 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

380 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

381 
(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

382 
(* denotes membership to an axiomatic type class *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

383 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

384 

46096  385 
fun is_const_of_class thy (s, _) = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

386 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

387 
val class_const_names = map Logic.const_of_class (Sign.all_classes thy) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

388 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

389 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

390 
(* or if we should also check the type 'T'. *) 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36555
diff
changeset

391 
member (op =) class_const_names s 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

392 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

393 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

394 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

395 
(* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

396 
(* of an inductive datatype in 'thy' *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

397 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

398 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

399 
fun is_IDT_constructor thy (s, T) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

400 
(case body_type T of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

401 
Type (s', _) => 
58129
3ec65a7f2b50
ported Refute to use new datatypes when possible
blanchet
parents:
58120
diff
changeset

402 
(case BNF_LFP_Compat.get_constrs thy s' of 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

403 
SOME constrs => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

404 
List.exists (fn (cname, cty) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

405 
cname = s andalso Sign.typ_instance thy (T, cty)) constrs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

406 
 NONE => false) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

407 
 _ => false); 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

408 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

409 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

410 
(* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

411 
(* operator of an inductive datatype in 'thy' *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

412 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

413 

46096  414 
fun is_IDT_recursor thy (s, _) = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

415 
let 
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58322
diff
changeset

416 
val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.get_all thy []) [] 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

417 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

418 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

419 
(* or if we should also check the type 'T'. *) 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36555
diff
changeset

420 
member (op =) rec_names s 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

421 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

422 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

423 
(*  *) 
30275
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

424 
(* norm_rhs: maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

425 
(*  *) 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

426 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

427 
fun norm_rhs eqn = 
30275
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

428 
let 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

429 
fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

430 
 lambda v t = raise TERM ("lambda", [v, t]) 
30275
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

431 
val (lhs, rhs) = Logic.dest_equals eqn 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

432 
val (_, args) = Term.strip_comb lhs 
30275
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

433 
in 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

434 
fold lambda (rev args) rhs 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

435 
end 
381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

436 

381ce8d88cb8
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
blanchet
parents:
30242
diff
changeset

437 
(*  *) 
37405  438 
(* get_def: looks up the definition of a constant *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

439 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

440 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

441 
fun get_def thy (s, T) = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

442 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

443 
fun get_def_ax [] = NONE 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

444 
 get_def_ax ((axname, ax) :: axioms) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

445 
(let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

446 
val (lhs, _) = Logic.dest_equals ax (* equations only *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

447 
val c = Term.head_of lhs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

448 
val (s', T') = Term.dest_Const c 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

449 
in 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

450 
if s=s' then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

451 
let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

452 
val typeSubs = Sign.typ_match thy (T', T) Vartab.empty 
61770  453 
val ax' = Envir.subst_term_types typeSubs ax 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

454 
val rhs = norm_rhs ax' 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

455 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

456 
SOME (axname, rhs) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

457 
end 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

458 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

459 
get_def_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

460 
end handle ERROR _ => get_def_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

461 
 TERM _ => get_def_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

462 
 Type.TYPE_MATCH => get_def_ax axioms) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

463 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

464 
get_def_ax (Theory.all_axioms_of thy) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

465 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

466 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

467 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

468 
(* get_typedef: looks up the definition of a type, as created by "typedef" *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

469 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

470 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

471 
fun get_typedef thy T = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

472 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

473 
fun get_typedef_ax [] = NONE 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

474 
 get_typedef_ax ((axname, ax) :: axioms) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

475 
(let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

476 
fun type_of_type_definition (Const (s', T')) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

477 
if s'= @{const_name type_definition} then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

478 
SOME T' 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

479 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

480 
NONE 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

481 
 type_of_type_definition (Free _) = NONE 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

482 
 type_of_type_definition (Var _) = NONE 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

483 
 type_of_type_definition (Bound _) = NONE 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

484 
 type_of_type_definition (Abs (_, _, body)) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

485 
type_of_type_definition body 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

486 
 type_of_type_definition (t1 $ t2) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

487 
(case type_of_type_definition t1 of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

488 
SOME x => SOME x 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

489 
 NONE => type_of_type_definition t2) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

490 
in 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

491 
case type_of_type_definition ax of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

492 
SOME T' => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

493 
let 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

494 
val T'' = domain_type (domain_type T') 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

495 
val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

496 
in 
61770  497 
SOME (axname, Envir.subst_term_types typeSubs ax) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

498 
end 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

499 
 NONE => get_typedef_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

500 
end handle ERROR _ => get_typedef_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

501 
 TERM _ => get_typedef_ax axioms 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

502 
 Type.TYPE_MATCH => get_typedef_ax axioms) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

503 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

504 
get_typedef_ax (Theory.all_axioms_of thy) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

505 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

506 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

507 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

508 
(* get_classdef: looks up the defining axiom for an axiomatic type class, as *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

509 
(* created by the "axclass" command *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

510 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

511 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

512 
fun get_classdef thy class = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

513 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

514 
val axname = class ^ "_class_def" 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

515 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

516 
Option.map (pair axname) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

517 
(AList.lookup (op =) (Theory.all_axioms_of thy) axname) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

518 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

519 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

520 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

521 
(* unfold_defs: unfolds all defined constants in a term 't', betaeta *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

522 
(* normalizes the result term; certain constants are not *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

523 
(* unfolded (cf. 'collect_axioms' and the various interpreters *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

524 
(* below): if the interpretation respects a definition anyway, *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

525 
(* that definition does not need to be unfolded *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

526 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

527 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

528 
(* Note: we could intertwine unfolding of constants and beta(eta) *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

529 
(* normalization; this would save some unfolding for terms where *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

530 
(* constants are eliminated by betareduction (e.g. 'K c1 c2'). On *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

531 
(* the other hand, this would cause additional work for terms where *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

532 
(* constants are duplicated by betareduction (e.g. 'S c1 c2 c3'). *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

533 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

534 
fun unfold_defs thy t = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

535 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

536 
fun unfold_loop t = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

537 
case t of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

538 
(* Pure *) 
56245  539 
Const (@{const_name Pure.all}, _) => t 
540 
 Const (@{const_name Pure.eq}, _) => t 

541 
 Const (@{const_name Pure.imp}, _) => t 

56243  542 
 Const (@{const_name Pure.type}, _) => t (* axiomatic type classes *) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

543 
(* HOL *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

544 
 Const (@{const_name Trueprop}, _) => t 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

545 
 Const (@{const_name Not}, _) => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

546 
 (* redundant, since 'True' is also an IDT constructor *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

547 
Const (@{const_name True}, _) => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

548 
 (* redundant, since 'False' is also an IDT constructor *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

549 
Const (@{const_name False}, _) => t 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

550 
 Const (@{const_name undefined}, _) => t 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

551 
 Const (@{const_name The}, _) => t 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

552 
 Const (@{const_name Hilbert_Choice.Eps}, _) => t 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

553 
 Const (@{const_name All}, _) => t 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

554 
 Const (@{const_name Ex}, _) => t 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

555 
 Const (@{const_name HOL.eq}, _) => t 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

556 
 Const (@{const_name HOL.conj}, _) => t 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

557 
 Const (@{const_name HOL.disj}, _) => t 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38553
diff
changeset

558 
 Const (@{const_name HOL.implies}, _) => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

559 
(* sets *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

560 
 Const (@{const_name Collect}, _) => t 
37677  561 
 Const (@{const_name Set.member}, _) => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

562 
(* other optimizations *) 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

563 
 Const (@{const_name Finite_Set.card}, _) => t 
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

564 
 Const (@{const_name Finite_Set.finite}, _) => t 
37388  565 
 Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

566 
Type ("fun", [@{typ nat}, @{typ bool}])])) => t 
37388  567 
 Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

568 
Type ("fun", [@{typ nat}, @{typ nat}])])) => t 
37388  569 
 Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

570 
Type ("fun", [@{typ nat}, @{typ nat}])])) => t 
37388  571 
 Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

572 
Type ("fun", [@{typ nat}, @{typ nat}])])) => t 
56252  573 
 Const (@{const_name append}, _) => t 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

574 
 Const (@{const_name fst}, _) => t 
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

575 
 Const (@{const_name snd}, _) => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

576 
(* simplytyped lambda calculus *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

577 
 Const (s, T) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

578 
(if is_IDT_constructor thy (s, T) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

579 
orelse is_IDT_recursor thy (s, T) then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

580 
t (* do not unfold IDT constructors/recursors *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

581 
(* unfold the constant if there is a defining equation *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

582 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

583 
case get_def thy (s, T) of 
46096  584 
SOME ((*axname*) _, rhs) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

585 
(* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

586 
(* occurs on the righthand side of the equation, i.e. in *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

587 
(* 'rhs', we must not use this equation to unfold, because *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

588 
(* that would loop. Here would be the right place to *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

589 
(* check this. However, getting this really right seems *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

590 
(* difficult because the user may state arbitrary axioms, *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

591 
(* which could interact with overloading to create loops. *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

592 
((*tracing (" unfolding: " ^ axname);*) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

593 
unfold_loop rhs) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

594 
 NONE => t) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

595 
 Free _ => t 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

596 
 Var _ => t 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

597 
 Bound _ => t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

598 
 Abs (s, T, body) => Abs (s, T, unfold_loop body) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

599 
 t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

600 
val result = Envir.beta_eta_contract (unfold_loop t) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

601 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

602 
result 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

603 
end; 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

604 

acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

605 
(*  *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

606 
(* collect_axioms: collects (monomorphic, universally quantified, unfolded *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

607 
(* versions of) all HOL axioms that are relevant w.r.t 't' *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

608 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

609 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

610 
(* Note: to make the collection of axioms more easily extensible, this *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

611 
(* function could be based on usersupplied "axiom collectors", *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

612 
(* similar to 'interpret'/interpreters or 'print'/printers *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

613 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

614 
(* Note: currently we use "inverse" functions to the definitional *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

615 
(* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

616 
(* "typedef", "definition". A more general approach could consider *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

617 
(* *every* axiom of the theory and collect it if it has a constant/ *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

618 
(* type/typeclass in common with the term 't'. *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

619 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

620 
(* Which axioms are "relevant" for a particular term/type goes hand in *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

621 
(* hand with the interpretation of that term/type by its interpreter (see *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

622 
(* way below): if the interpretation respects an axiom anyway, the axiom *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

623 
(* does not need to be added as a constraint here. *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

624 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

625 
(* To avoid collecting the same axiom multiple times, we use an *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

626 
(* accumulator 'axs' which contains all axioms collected so far. *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

627 

56256  628 
local 
629 

630 
fun get_axiom thy xname = 

631 
Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none); 

632 

633 
val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial"; 

634 
val someI = get_axiom @{theory Hilbert_Choice} "someI"; 

635 

636 
in 

637 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

638 
fun collect_axioms ctxt t = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

639 
let 
42361  640 
val thy = Proof_Context.theory_of ctxt 
32950  641 
val _ = tracing "Adding axioms..." 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

642 
fun collect_this_axiom (axname, ax) axs = 
33246  643 
let 
644 
val ax' = unfold_defs thy ax 

645 
in 

646 
if member (op aconv) axs ax' then axs 

647 
else (tracing axname; collect_term_axioms ax' (ax' :: axs)) 

648 
end 

649 
and collect_sort_axioms T axs = 

650 
let 

651 
val sort = 

652 
(case T of 

653 
TFree (_, sort) => sort 

654 
 TVar (_, sort) => sort 

655 
 _ => raise REFUTE ("collect_axioms", 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

656 
"type " ^ Syntax.string_of_typ ctxt T ^ " is not a variable")) 
33246  657 
(* obtain axioms for all superclasses *) 
658 
val superclasses = sort @ maps (Sign.super_classes thy) sort 

659 
(* merely an optimization, because 'collect_this_axiom' disallows *) 

660 
(* duplicate axioms anyway: *) 

661 
val superclasses = distinct (op =) superclasses 

662 
val class_axioms = maps (fn class => map (fn ax => 

663 
("<" ^ class ^ ">", Thm.prop_of ax)) 

51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51557
diff
changeset

664 
(#axioms (Axclass.get_info thy class) handle ERROR _ => [])) 
33246  665 
superclasses 
666 
(* replace the (at most one) schematic type variable in each axiom *) 

667 
(* by the actual type 'T' *) 

668 
val monomorphic_class_axioms = map (fn (axname, ax) => 

669 
(case Term.add_tvars ax [] of 

670 
[] => (axname, ax) 

61770  671 
 [(idx, S)] => (axname, Envir.subst_term_types (Vartab.make [(idx, (S, T))]) ax) 
33246  672 
 _ => 
673 
raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

674 
Syntax.string_of_term ctxt ax ^ 
33246  675 
") contains more than one type variable"))) 
676 
class_axioms 

677 
in 

678 
fold collect_this_axiom monomorphic_class_axioms axs 

679 
end 

680 
and collect_type_axioms T axs = 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

681 
case T of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

682 
(* simple types *) 
56252  683 
Type (@{type_name prop}, []) => axs 
684 
 Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) 

46098
ce939621a1fe
handle "set" correctly in Refute  inspired by old code from Isabelle2007
blanchet
parents:
46096
diff
changeset

685 
 Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

686 
(* axiomatic type classes *) 
56252  687 
 Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs 
33246  688 
 Type (s, Ts) => 
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58322
diff
changeset

689 
(case BNF_LFP_Compat.get_info thy [] s of 
46096  690 
SOME _ => (* inductive datatype *) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

691 
(* only collect relevant type axioms for the argument types *) 
33246  692 
fold collect_type_axioms Ts axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

693 
 NONE => 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

694 
(case get_typedef thy T of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

695 
SOME (axname, ax) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

696 
collect_this_axiom (axname, ax) axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

697 
 NONE => 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

698 
(* unspecified type, perhaps introduced with "typedecl" *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

699 
(* at least collect relevant type axioms for the argument types *) 
33246  700 
fold collect_type_axioms Ts axs)) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

701 
(* axiomatic type classes *) 
33246  702 
 TFree _ => collect_sort_axioms T axs 
703 
(* axiomatic type classes *) 

704 
 TVar _ => collect_sort_axioms T axs 

705 
and collect_term_axioms t axs = 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

706 
case t of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

707 
(* Pure *) 
56245  708 
Const (@{const_name Pure.all}, _) => axs 
709 
 Const (@{const_name Pure.eq}, _) => axs 

710 
 Const (@{const_name Pure.imp}, _) => axs 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

711 
(* axiomatic type classes *) 
56243  712 
 Const (@{const_name Pure.type}, T) => collect_type_axioms T axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

713 
(* HOL *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

714 
 Const (@{const_name Trueprop}, _) => axs 
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

715 
 Const (@{const_name Not}, _) => axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

716 
(* redundant, since 'True' is also an IDT constructor *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

717 
 Const (@{const_name True}, _) => axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

718 
(* redundant, since 'False' is also an IDT constructor *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

719 
 Const (@{const_name False}, _) => axs 
33246  720 
 Const (@{const_name undefined}, T) => collect_type_axioms T axs 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

721 
 Const (@{const_name The}, T) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

722 
let 
56256  723 
val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

724 
in 
56256  725 
collect_this_axiom (#1 the_eq_trivial, ax) axs 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

726 
end 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

727 
 Const (@{const_name Hilbert_Choice.Eps}, T) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

728 
let 
56256  729 
val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

730 
in 
56256  731 
collect_this_axiom (#1 someI, ax) axs 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

732 
end 
33246  733 
 Const (@{const_name All}, T) => collect_type_axioms T axs 
734 
 Const (@{const_name Ex}, T) => collect_type_axioms T axs 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

735 
 Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

736 
 Const (@{const_name HOL.conj}, _) => axs 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

737 
 Const (@{const_name HOL.disj}, _) => axs 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38553
diff
changeset

738 
 Const (@{const_name HOL.implies}, _) => axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

739 
(* sets *) 
33246  740 
 Const (@{const_name Collect}, T) => collect_type_axioms T axs 
37677  741 
 Const (@{const_name Set.member}, T) => collect_type_axioms T axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

742 
(* other optimizations *) 
33246  743 
 Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

744 
 Const (@{const_name Finite_Set.finite}, T) => 
33246  745 
collect_type_axioms T axs 
37388  746 
 Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat}, 
38553
56965d8e4e11
use HOLogic.boolT and @{typ bool} more pervasively
haftmann
parents:
37677
diff
changeset

747 
Type ("fun", [@{typ nat}, @{typ bool}])])) => 
33246  748 
collect_type_axioms T axs 
37388  749 
 Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat}, 
750 
Type ("fun", [@{typ nat}, @{typ nat}])])) => 

33246  751 
collect_type_axioms T axs 
37388  752 
 Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat}, 
753 
Type ("fun", [@{typ nat}, @{typ nat}])])) => 

33246  754 
collect_type_axioms T axs 
37388  755 
 Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat}, 
756 
Type ("fun", [@{typ nat}, @{typ nat}])])) => 

33246  757 
collect_type_axioms T axs 
56252  758 
 Const (@{const_name append}, T) => collect_type_axioms T axs 
33246  759 
 Const (@{const_name fst}, T) => collect_type_axioms T axs 
760 
 Const (@{const_name snd}, T) => collect_type_axioms T axs 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

761 
(* simplytyped lambda calculus *) 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

762 
 Const (s, T) => 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

763 
if is_const_of_class thy (s, T) then 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

764 
(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

765 
(* and the class definition *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

766 
let 
33246  767 
val class = Logic.class_of_const s 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31784
diff
changeset

768 
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) 
33246  769 
val ax_in = SOME (specialize_type thy (s, T) of_class) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

770 
(* type match may fail due to sort constraints *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

771 
handle Type.TYPE_MATCH => NONE 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

772 
val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in 
33246  773 
val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

774 
in 
33246  775 
collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

776 
end 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

777 
else if is_IDT_constructor thy (s, T) 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

778 
orelse is_IDT_recursor thy (s, T) 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

779 
then 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

780 
(* only collect relevant type axioms *) 
33246  781 
collect_type_axioms T axs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

782 
else 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

783 
(* other constants should have been unfolded, with some *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

784 
(* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

785 
(* typedefs, or typeclass related constants *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

786 
(* only collect relevant type axioms *) 
33246  787 
collect_type_axioms T axs 
788 
 Free (_, T) => collect_type_axioms T axs 

789 
 Var (_, T) => collect_type_axioms T axs 

790 
 Bound _ => axs 

791 
 Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs) 

792 
 t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs) 

793 
val result = map close_form (collect_term_axioms t []) 

32950  794 
val _ = tracing " ...done." 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

795 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

796 
result 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

797 
end; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

798 

56256  799 
end; 
800 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

801 
(*  *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

802 
(* ground_types: collects all ground types in a term (including argument *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

803 
(* types of other types), suppressing duplicates. Does not *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

804 
(* return function types, set types, nonrecursive IDTs, or *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

805 
(* 'propT'. For IDTs, also the argument types of constructors *) 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

806 
(* and all mutually recursive IDTs are considered. *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

807 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

808 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

809 
fun ground_types ctxt t = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

810 
let 
42361  811 
val thy = Proof_Context.theory_of ctxt 
29272  812 
fun collect_types T acc = 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

813 
(case T of 
56252  814 
Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc) 
815 
 Type (@{type_name prop}, []) => acc 

46098
ce939621a1fe
handle "set" correctly in Refute  inspired by old code from Isabelle2007
blanchet
parents:
46096
diff
changeset

816 
 Type (@{type_name set}, [T1]) => collect_types T1 acc 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

817 
 Type (s, Ts) => 
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58322
diff
changeset

818 
(case BNF_LFP_Compat.get_info thy [] s of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

819 
SOME info => (* inductive datatype *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

820 
let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

821 
val index = #index info 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

822 
val descr = #descr info 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

823 
val (_, typs, _) = the (AList.lookup (op =) descr index) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

824 
val typ_assoc = typs ~~ Ts 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

825 
(* sanity check: every element in 'dtyps' must be a *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

826 
(* 'DtTFree' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

827 
val _ = if Library.exists (fn d => 
58120  828 
case d of Old_Datatype_Aux.DtTFree _ => false  _ => true) typs then 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

829 
raise REFUTE ("ground_types", "datatype argument (for type " 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

830 
^ Syntax.string_of_typ ctxt T ^ ") is not a variable") 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

831 
else () 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

832 
(* required for mutually recursive datatypes; those need to *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

833 
(* be added even if they are an instance of an otherwise non *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

834 
(* recursive datatype *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

835 
fun collect_dtyp d acc = 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

836 
let 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

837 
val dT = typ_of_dtyp descr typ_assoc d 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

838 
in 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

839 
case d of 
58120  840 
Old_Datatype_Aux.DtTFree _ => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

841 
collect_types dT acc 
58120  842 
 Old_Datatype_Aux.DtType (_, ds) => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

843 
collect_types dT (fold_rev collect_dtyp ds acc) 
58120  844 
 Old_Datatype_Aux.DtRec i => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

845 
if member (op =) acc dT then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

846 
acc (* prevent infinite recursion *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

847 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

848 
let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

849 
val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

850 
(* if the current type is a recursive IDT (i.e. a depth *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

851 
(* is required), add it to 'acc' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

852 
val acc_dT = if Library.exists (fn (_, ds) => 
58120  853 
Library.exists Old_Datatype_Aux.is_rec_type ds) dconstrs then 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

854 
insert (op =) dT acc 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

855 
else acc 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

856 
(* collect argument types *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

857 
val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

858 
(* collect constructor types *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

859 
val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

860 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

861 
acc_dconstrs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

862 
end 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

863 
end 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

864 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

865 
(* argument types 'Ts' could be added here, but they are also *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

866 
(* added by 'collect_dtyp' automatically *) 
58120  867 
collect_dtyp (Old_Datatype_Aux.DtRec index) acc 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

868 
end 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

869 
 NONE => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

870 
(* not an inductive datatype, e.g. defined via "typedef" or *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

871 
(* "typedecl" *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

872 
insert (op =) T (fold collect_types Ts acc)) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

873 
 TFree _ => insert (op =) T acc 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

874 
 TVar _ => insert (op =) T acc) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

875 
in 
29272  876 
fold_types collect_types t [] 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

877 
end; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

878 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

879 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

880 
(* string_of_typ: (rather naive) conversion from types to strings, used to *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

881 
(* look up the size of a type in 'sizes'. Parameterized *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

882 
(* types with different parameters (e.g. "'a list" vs. "bool *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

883 
(* list") are identified. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

884 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

885 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

886 
fun string_of_typ (Type (s, _)) = s 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

887 
 string_of_typ (TFree (s, _)) = s 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

888 
 string_of_typ (TVar ((s,_), _)) = s; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

889 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

890 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

891 
(* first_universe: returns the "first" (i.e. smallest) universe by assigning *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

892 
(* 'minsize' to every type for which no size is specified in *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

893 
(* 'sizes' *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

894 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

895 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

896 
fun first_universe xs sizes minsize = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

897 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

898 
fun size_of_typ T = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

899 
case AList.lookup (op =) sizes (string_of_typ T) of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

900 
SOME n => n 
33246  901 
 NONE => minsize 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

902 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

903 
map (fn T => (T, size_of_typ T)) xs 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

904 
end; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

905 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

906 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

907 
(* next_universe: enumerates all universes (i.e. assignments of sizes to *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

908 
(* types), where the minimal size of a type is given by *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

909 
(* 'minsize', the maximal size is given by 'maxsize', and a *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

910 
(* type may have a fixed size given in 'sizes' *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

911 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

912 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

913 
fun next_universe xs sizes minsize maxsize = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

914 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

915 
(* creates the "first" list of length 'len', where the sum of all list *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

916 
(* elements is 'sum', and the length of the list is 'len' *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

917 
fun make_first _ 0 sum = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

918 
if sum = 0 then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

919 
SOME [] 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

920 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

921 
NONE 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

922 
 make_first max len sum = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

923 
if sum <= max orelse max < 0 then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

924 
Option.map (fn xs' => sum :: xs') (make_first max (len1) 0) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

925 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

926 
Option.map (fn xs' => max :: xs') (make_first max (len1) (summax)) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

927 
(* enumerates all int lists with a fixed length, where 0<=x<='max' for *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

928 
(* all list elements x (unless 'max'<0) *) 
46096  929 
fun next _ _ _ [] = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

930 
NONE 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

931 
 next max len sum [x] = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

932 
(* we've reached the last list element, so there's no shift possible *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

933 
make_first max (len+1) (sum+x+1) (* increment 'sum' by 1 *) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

934 
 next max len sum (x1::x2::xs) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

935 
if x1>0 andalso (x2<max orelse max<0) then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

936 
(* we can shift *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

937 
SOME (the (make_first max (len+1) (sum+x11)) @ (x2+1) :: xs) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

938 
else 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

939 
(* continue search *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

940 
next max (len+1) (sum+x1) (x2::xs) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

941 
(* only consider those types for which the size is not fixed *) 
33317  942 
val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

943 
(* subtract 'minsize' from every size (will be added again at the end) *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

944 
val diffs = map (fn (_, n) => nminsize) mutables 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

945 
in 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

946 
case next (maxsizeminsize) 0 0 diffs of 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

947 
SOME diffs' => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

948 
(* merge with those types for which the size is fixed *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

949 
SOME (fst (fold_map (fn (T, _) => fn ds => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

950 
case AList.lookup (op =) sizes (string_of_typ T) of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

951 
(* return the fixed size *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

952 
SOME n => ((T, n), ds) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

953 
(* consume the head of 'ds', add 'minsize' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

954 
 NONE => ((T, minsize + hd ds), tl ds)) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

955 
xs diffs')) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

956 
 NONE => NONE 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

957 
end; 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

958 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

959 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

960 
(* toTrue: converts the interpretation of a Boolean value to a propositional *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

961 
(* formula that is true iff the interpretation denotes "true" *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

962 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

963 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

964 
fun toTrue (Leaf [fm, _]) = fm 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

965 
 toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

966 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

967 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

968 
(* toFalse: converts the interpretation of a Boolean value to a *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

969 
(* propositional formula that is true iff the interpretation *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

970 
(* denotes "false" *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

971 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

972 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

973 
fun toFalse (Leaf [_, fm]) = fm 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

974 
 toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

975 

e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

976 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

977 
(* find_model: repeatedly calls 'interpret' with appropriate parameters, *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

978 
(* applies a SAT solver, and (in case a model is found) displays *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

979 
(* the model to the user by calling 'print_model' *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

980 
(* {...} : parameters that control the translation/model generation *) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

981 
(* assm_ts : assumptions to be considered unless "no_assms" is specified *) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

982 
(* t : term to be translated into a propositional formula *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

983 
(* negate : if true, find a model that makes 't' false (rather than true) *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

984 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

985 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

986 
fun find_model ctxt 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

987 
{sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect} 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

988 
assm_ts t negate = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

989 
let 
42361  990 
val thy = Proof_Context.theory_of ctxt 
33054
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

991 
fun check_expect outcome_code = 
45387
ccffb3f9f42b
return outcome code, so that it can be picked up by Mutabelle
blanchet
parents:
44121
diff
changeset

992 
if expect = "" orelse outcome_code = expect then outcome_code 
33054
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

993 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

994 
fun wrapper () = 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

995 
let 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

996 
val timer = Timer.startRealTimer () 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

997 
val t = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

998 
if no_assms then t 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

999 
else if negate then Logic.list_implies (assm_ts, t) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1000 
else Logic.mk_conjunction_list (t :: assm_ts) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1001 
val u = unfold_defs thy t 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1002 
val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u) 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1003 
val axioms = collect_axioms ctxt u 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1004 
val types = fold (union (op =) o ground_types ctxt) (u :: axioms) [] 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1005 
val _ = tracing ("Ground types: " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1006 
^ (if null types then "none." 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1007 
else commas (map (Syntax.string_of_typ ctxt) types))) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1008 
(* we can only consider fragments of recursive IDTs, so we issue a *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1009 
(* warning if the formula contains a recursive IDT *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1010 
(* TODO: no warning needed for /positive/ occurrences of IDTs *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1011 
val maybe_spurious = Library.exists (fn 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1012 
Type (s, _) => 
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58322
diff
changeset

1013 
(case BNF_LFP_Compat.get_info thy [] s of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1014 
SOME info => (* inductive datatype *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1015 
let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1016 
val index = #index info 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1017 
val descr = #descr info 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1018 
val (_, _, constrs) = the (AList.lookup (op =) descr index) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1019 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1020 
(* recursive datatype? *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1021 
Library.exists (fn (_, ds) => 
58120  1022 
Library.exists Old_Datatype_Aux.is_rec_type ds) constrs 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1023 
end 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1024 
 NONE => false) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1025 
 _ => false) types 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1026 
val _ = 
59352
63c02d051661
tuned warnings: observe Context_Position.is_visible;
wenzelm
parents:
58893
diff
changeset

1027 
if maybe_spurious andalso Context_Position.is_visible ctxt then 
63c02d051661
tuned warnings: observe Context_Position.is_visible;
wenzelm
parents:
58893
diff
changeset

1028 
warning "Term contains a recursive datatype; countermodel(s) may be spurious!" 
63c02d051661
tuned warnings: observe Context_Position.is_visible;
wenzelm
parents:
58893
diff
changeset

1029 
else () 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1030 
fun find_model_loop universe = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1031 
let 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1032 
val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1033 
val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime 
62519  1034 
orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1035 
val init_model = (universe, []) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1036 
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1037 
bounds = [], wellformed = True} 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1038 
val _ = tracing ("Translating term (sizes: " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1039 
^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1040 
(* translate 'u' and all axioms *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1041 
val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1042 
let 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1043 
val (i, m', a') = interpret ctxt m a t' 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1044 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1045 
(* set 'def_eq' to 'true' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1046 
(i, (m', {maxvars = #maxvars a', def_eq = true, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1047 
next_idx = #next_idx a', bounds = #bounds a', 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1048 
wellformed = #wellformed a'})) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1049 
end) (u :: axioms) (init_model, init_args) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1050 
(* make 'u' either true or false, and make all axioms true, and *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1051 
(* add the wellformedness side condition *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1052 
val fm_u = (if negate then toFalse else toTrue) (hd intrs) 
41471  1053 
val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) 
1054 
val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1055 
val _ = 
59352
63c02d051661
tuned warnings: observe Context_Position.is_visible;
wenzelm
parents:
58893
diff
changeset

1056 
(if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1057 
warning ("Using SAT solver " ^ quote satsolver ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1058 
"; for better performance, consider installing an \ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1059 
\external solver.") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1060 
else ()); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1061 
val solver = 
56853  1062 
SAT_Solver.invoke_solver satsolver 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1063 
handle Option.Option => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1064 
error ("Unknown SAT solver: " ^ quote satsolver ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1065 
". Available solvers: " ^ 
56853  1066 
commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1067 
in 
58843  1068 
writeln "Invoking SAT solver..."; 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1069 
(case solver fm of 
56853  1070 
SAT_Solver.SATISFIABLE assignment => 
58843  1071 
(writeln ("Model found:\n" ^ print_model ctxt model 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1072 
(fn i => case assignment i of SOME b => b  NONE => true)); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1073 
if maybe_spurious then "potential" else "genuine") 
56853  1074 
 SAT_Solver.UNSATISFIABLE _ => 
58843  1075 
(writeln "No model exists."; 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1076 
case next_universe universe sizes minsize maxsize of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1077 
SOME universe' => find_model_loop universe' 
58843  1078 
 NONE => (writeln 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39811
diff
changeset

1079 
"Search terminated, no larger universe within the given limits."; 
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39811
diff
changeset

1080 
"none")) 
56853  1081 
 SAT_Solver.UNKNOWN => 
58843  1082 
(writeln "No model found."; 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1083 
case next_universe universe sizes minsize maxsize of 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1084 
SOME universe' => find_model_loop universe' 
58843  1085 
 NONE => (writeln 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1086 
"Search terminated, no larger universe within the given limits."; 
56853  1087 
"unknown"))) handle SAT_Solver.NOT_CONFIGURED => 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1088 
(error ("SAT solver " ^ quote satsolver ^ " is not configured."); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1089 
"unknown") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1090 
end 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1091 
handle MAXVARS_EXCEEDED => 
58843  1092 
(writeln ("Search terminated, number of Boolean variables (" 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1093 
^ string_of_int maxvars ^ " allowed) exceeded."); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1094 
"unknown") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1095 

30314
853778f6ef7d
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
blanchet
parents:
30312
diff
changeset

1096 
val outcome_code = find_model_loop (first_universe types sizes minsize) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1097 
in 
33054
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1098 
check_expect outcome_code 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1099 
end 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1100 
in 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1101 
(* some parameter sanity checks *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1102 
minsize>=1 orelse 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1103 
error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1104 
maxsize>=1 orelse 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1105 
error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1106 
maxsize>=minsize orelse 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1107 
error ("\"maxsize\" (=" ^ string_of_int maxsize ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1108 
") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1109 
maxvars>=0 orelse 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1110 
error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1111 
maxtime>=0 orelse 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1112 
error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1113 
(* enter loop with or without time limit *) 
58843  1114 
writeln ("Trying to find a model that " 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1115 
^ (if negate then "refutes" else "satisfies") ^ ": " 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1116 
^ Syntax.string_of_term ctxt t); 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1117 
if maxtime > 0 then ( 
62519  1118 
Timeout.apply (Time.fromSeconds maxtime) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1119 
wrapper () 
62519  1120 
handle Timeout.TIMEOUT _ => 
58843  1121 
(writeln ("Search terminated, time limit (" ^ 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1122 
string_of_int maxtime 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1123 
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded."); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1124 
check_expect "unknown") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1125 
) else wrapper () 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1126 
end; 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1127 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1128 

cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1129 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1130 
(* INTERFACE, PART 2: FINDING A MODEL *) 
14350  1131 
(*  *) 
1132 

1133 
(*  *) 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1134 
(* satisfy_term: calls 'find_model' to find a model that satisfies 't' *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1135 
(* params : list of '(name, value)' pairs used to override default *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1136 
(* parameters *) 
14350  1137 
(*  *) 
1138 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1139 
fun satisfy_term ctxt params assm_ts t = 
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1140 
find_model ctxt (actual_params ctxt params) assm_ts t false; 
14350  1141 

1142 
(*  *) 

14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1143 
(* refute_term: calls 'find_model' to find a model that refutes 't' *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1144 
(* params : list of '(name, value)' pairs used to override default *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1145 
(* parameters *) 
14350  1146 
(*  *) 
1147 

39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1148 
fun refute_term ctxt params assm_ts t = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1149 
let 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1150 
(* disallow schematic type variables, since we cannot properly negate *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1151 
(* terms containing them (their logical meaning is that there EXISTS a *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1152 
(* type s.t. ...; to refute such a formula, we would have to show that *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1153 
(* for ALL types, not ...) *) 
29272  1154 
val _ = null (Term.add_tvars t []) orelse 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1155 
error "Term to be refuted contains schematic type variables" 
21556  1156 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1157 
(* existential closure over schematic variables *) 
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60190
diff
changeset

1158 
val vars = sort_by (fst o fst) (Term.add_vars t []) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1159 
(* Term.term *) 
33246  1160 
val ex_closure = fold (fn ((x, i), T) => fn t' => 
1161 
HOLogic.exists_const T $ 

1162 
Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1163 
(* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1164 
(* 'HOLogic.exists_const' is not typecorrect. However, this is not *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1165 
(* really a problem as long as 'find_model' still interprets the *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1166 
(* resulting term correctly, without checking its type. *) 
21556  1167 

22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1168 
(* replace outermost universally quantified variables by Free's: *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1169 
(* refuting a term with Free's is generally faster than refuting a *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1170 
(* term with (nested) quantifiers, because quantifiers are expanded, *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1171 
(* while the SAT solver searches for an interpretation for Free's. *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1172 
(* Also we get more information back that way, namely an *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1173 
(* interpretation which includes values for the (formerly) *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1174 
(* quantified variables. *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1175 
(* maps !!x1...xn. !xk...xm. t to t *) 
56245  1176 
fun strip_all_body (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1177 
strip_all_body t 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

1178 
 strip_all_body (Const (@{const_name Trueprop}, _) $ t) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1179 
strip_all_body t 
29820
07f53494cf20
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
blanchet
parents:
29802
diff
changeset

1180 
 strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1181 
strip_all_body t 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

1182 
 strip_all_body t = t 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1183 
(* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) 
56245  1184 
fun strip_all_vars (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1185 
(a, T) :: strip_all_vars t 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

1186 
 strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1187 
strip_all_vars t 
29802
d201a838d0f7
Make some Refute functions public so I can use them in Nitpick,
blanchet
parents:
29288
diff
changeset

1188 
 strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) = 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1189 
(a, T) :: strip_all_vars t 
46096  1190 
 strip_all_vars _ = [] : (string * typ) list 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1191 
val strip_t = strip_all_body ex_closure 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1192 
val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1193 
val subst_t = Term.subst_bounds (map Free frees, strip_t) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1194 
in 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1195 
find_model ctxt (actual_params ctxt params) assm_ts subst_t true 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1196 
end; 
14350  1197 

1198 
(*  *) 

32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
31986
diff
changeset

1199 
(* refute_goal *) 
14350  1200 
(*  *) 
1201 

39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1202 
fun refute_goal ctxt params th i = 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1203 
let 
59582  1204 
val t = th > Thm.prop_of 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1205 
in 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1206 
if Logic.count_prems t = 0 then 
58843  1207 
(writeln "No subgoal!"; "none") 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1208 
else 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1209 
let 
59582  1210 
val assms = map Thm.term_of (Assumption.all_assms_of ctxt) 
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1211 
val (t, frees) = Logic.goal_params t i 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

1212 
in 
39049
423b72f2d242
prefer regular Proof.context over background theory;
wenzelm
parents:
39048
diff
changeset

1213 
refute_term ctxt params assms (subst_bounds (frees, t)) 
34120
f9920a3ddf50
added 