author  wenzelm 
Thu, 02 Sep 2010 16:45:21 +0200  
changeset 39047  cdff476ba39e 
parent 39046  5b38730f3e12 
child 39048  4006f5c3f421 
permissions  rwrr 
14350  1 
(* Title: HOL/Tools/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 

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

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

8 
(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

9 
(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *) 
14350  10 
(*  *) 
11 

12 
signature REFUTE = 

13 
sig 

14 

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

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

16 

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

17 
(*  *) 
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

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

19 
(*  *) 
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 
type params 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

25 

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

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

27 

33243  28 
val add_interpreter : string > (theory > 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) option) > theory > theory 
33243  30 
val add_printer : string > (theory > model > typ > 
31 
interpretation > (int > bool) > term option) > theory > theory 

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

32 

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

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

35 

33243  36 
val print : theory > model > typ > interpretation > (int > bool) > term 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

38 

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

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

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

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

42 

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

43 
val set_default_param : (string * string) > theory > theory 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

44 
val get_default_param : theory > string > string option 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

45 
val get_default_params : theory > (string * string) list 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

47 

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

48 
val find_model : theory > params > term list > term > bool > unit 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

49 

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

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

51 
val satisfy_term : 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

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

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

54 
val refute_term : 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

55 
theory > (string * string) list > term list > term > unit 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

56 
val refute_goal : 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

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

58 

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

59 
val setup : theory > theory 
22092  60 

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

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

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

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

64 

33243  65 
val close_form : term > term 
66 
val get_classdef : theory > string > (string * term) option 

67 
val norm_rhs : term > term 

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

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

70 
val is_IDT_constructor : theory > string * typ > bool 

71 
val is_IDT_recursor : theory > string * typ > bool 

72 
val is_const_of_class: theory > string * typ > bool 

73 
val string_of_typ : typ > string 

74 
val typ_of_dtyp : Datatype.descr > (Datatype.dtyp * typ) list > Datatype.dtyp > typ 

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

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

76 

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

77 

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

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

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

80 

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

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

82 

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

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

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

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

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

87 
exception REFUTE of string * string; (* ("in function", "cause") *) 
14350  88 

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

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

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

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

92 

14350  93 

94 
(*  *) 

95 
(* TREES *) 

96 
(*  *) 

97 

98 
(*  *) 

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

100 
(* of (lists of ...) elements *) 

101 
(*  *) 

102 

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

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

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

105 
 Node of ('a tree) list; 
14350  106 

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

107 
(* ('a > 'b) > 'a tree > 'b tree *) 
14350  108 

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

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

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

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

112 
 Node xs => Node (map (tree_map f) xs); 
14350  113 

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

114 
(* ('a * 'b > 'a) > 'a * ('b tree) > 'a *) 
14350  115 

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

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

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

118 
fun itl (e, Leaf x) = f(e,x) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

119 
 itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

122 
end; 
14350  123 

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

124 
(* 'a tree * 'b tree > ('a * 'b) tree *) 
14350  125 

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

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

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

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

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

130 
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

131 
 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

132 
"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

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

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

135 
(* '~~' 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

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

137 
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

138 
 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

139 
"trees are of different height (first tree is higher)")); 
14350  140 

141 
(*  *) 

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

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

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

144 
(* *) 
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

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

146 
(* "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

147 
(* *) 
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

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

149 
(* *) 
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

150 
(* "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

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

152 
(* "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

153 
(* "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

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

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

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

157 
(* "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

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

159 
(* "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

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

161 
(* "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

162 
(* "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

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

164 

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

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

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

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

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

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

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

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

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

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

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

175 
}; 
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

176 

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

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

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

179 
(* 'interpretation' *) 
14350  180 
(*  *) 
181 

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

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

183 
prop_formula list tree; 
14350  184 

185 
(*  *) 

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

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

187 
(* terms *) 
14350  188 
(*  *) 
189 

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

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

191 
(typ * int) list * (term * interpretation) list; 
14350  192 

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

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

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

195 
(*  *) 
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

196 

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

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

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

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

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

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

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

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

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

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

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

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

208 

14350  209 

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

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

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

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

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

214 
(interpretation * model * arguments) option)) list, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

217 
parameters: string Symtab.table}; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

222 
{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

223 
{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

224 
printers = AList.merge (op =) (K true) (pr1, pr2), 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

227 

14350  228 

229 
(*  *) 

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

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

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

232 
(* track of the interpretation of subterms *) 
14350  233 
(*  *) 
234 

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

235 
(* theory > model > arguments > Term.term > 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

237 

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

238 
fun interpret thy model args t = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

239 
case get_first (fn (_, f) => f thy model args t) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

240 
(#interpreters (RefuteData.get thy)) of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

241 
NONE => raise REFUTE ("interpret", 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

244 

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

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

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

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

248 
(*  *) 
14350  249 

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

250 
(* theory > model > Term.typ > interpretation > (int > bool) > 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

252 

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

253 
fun print thy model T intr assignment = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

254 
case get_first (fn (_, f) => f thy model T intr assignment) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

255 
(#printers (RefuteData.get thy)) of 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

256 
NONE => raise REFUTE ("print", 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

259 

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

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

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

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

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

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

265 

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

266 
(* theory > model > (int > bool) > string *) 
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

267 

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

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

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

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

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

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

273 
"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

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

275 
"Size of types: " ^ commas (map (fn (T, i) => 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

276 
Syntax.string_of_typ_global thy 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

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

278 
if not (!show_consts) andalso Library.exists (is_Const o fst) terms then 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

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

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

284 
"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

285 
else 
32952  286 
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

287 
(* print constants only if 'show_consts' is true *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

288 
if (!show_consts) orelse not (is_Const t) then 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

289 
SOME (Syntax.string_of_term_global thy t ^ ": " ^ 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset

290 
Syntax.string_of_term_global thy 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

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

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

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

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

295 
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

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

297 

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 
(*  *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

300 
(* PARAMETER MANAGEMENT *) 
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 

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

303 
(* string > (theory > model > arguments > Term.term > 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

304 
(interpretation * model * arguments) option) > theory > theory *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

305 

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

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

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

308 
val {interpreters, printers, parameters} = RefuteData.get thy 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

311 
NONE => RefuteData.put {interpreters = (name, f) :: interpreters, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

312 
printers = printers, parameters = parameters} thy 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

313 
 SOME _ => error ("Interpreter " ^ name ^ " already declared") 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

315 

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

316 
(* string > (theory > model > Term.typ > interpretation > 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

317 
(int > bool) > Term.term option) > theory > theory *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

318 

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

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

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

321 
val {interpreters, printers, parameters} = RefuteData.get thy 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

324 
NONE => RefuteData.put {interpreters = interpreters, 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

325 
printers = (name, f) :: printers, parameters = parameters} thy 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

326 
 SOME _ => error ("Printer " ^ name ^ " already declared") 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

328 

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

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

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

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

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

333 

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

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

335 

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

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

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

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

339 
parameters = Symtab.update (name, value) parameters}); 
14350  340 

341 
(*  *) 

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

342 
(* get_default_param: retrieves the value associated with 'name' from *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

345 

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

346 
(* theory > string > string option *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

347 

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

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

349 

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

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

351 
(* get_default_params: returns a list of all '(name, value)' pairs that are *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

354 

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

355 
(* theory > (string * string) list *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

356 

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

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

358 

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

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

360 
(* actual_params: takes a (possibly empty) list 'params' of parameters that *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

361 
(* override the default parameters currently specified in 'thy', 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

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

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

364 

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

365 
(* theory > (string * string) list > params *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

366 

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

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

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

369 
(* (string * string) list * string > bool *) 
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34017
diff
changeset

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

371 
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

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

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

374 
 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

375 
" (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

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

377 
" 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

378 
(* (string * string) list * string > int *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

379 
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

380 
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

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

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

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

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

385 
" (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

386 
 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

387 
" 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

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

389 
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

390 
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

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

392 
 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

393 
" 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

394 
(* 'override' first, defaults last: *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

396 
val allparams = override @ (get_default_params thy) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

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

401 
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

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

403 
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

404 
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

405 
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

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

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

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

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

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

411 
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

412 
(fn (name, value) => Option.map (pair name) (Int.fromString value)) 
33317  413 
(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

414 
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

415 
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

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

417 
{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

418 
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

419 
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

420 

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

421 

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

422 
(*  *) 
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

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

424 
(*  *) 
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

425 

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

426 
fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

427 
(* replace a 'DtTFree' variable by the associated type *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

428 
the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a)) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

429 
 typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) = 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

430 
Type (s, map (typ_of_dtyp descr typ_assoc) ds) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

431 
 typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) = 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

435 
Type (s, map (typ_of_dtyp descr typ_assoc) ds) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

436 
end; 
15335
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

437 

f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

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

439 
(* close_form: universal closure over schematic variables in 't' *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

441 

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

442 
(* Term.term > Term.term *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

443 

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

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

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

446 
(* (Term.indexname * Term.typ) list *) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29004
diff
changeset

447 
val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

448 
in 
33246  449 
fold (fn ((x, i), T) => fn t' => 
450 
Term.all T $ 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

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

452 

36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36374
diff
changeset

453 
val monomorphic_term = Sledgehammer_Util.monomorphic_term 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36374
diff
changeset

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

455 

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

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

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

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

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

460 

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

461 
(* theory > string * Term.typ > bool *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

462 

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

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

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

465 
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

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

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

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

469 
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

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

471 

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

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

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

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

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

476 

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

477 
(* theory > string * Term.typ > bool *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

478 

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

479 
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

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

481 
Type (s', _) => 
31784  482 
(case Datatype.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

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

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

485 
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

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

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

488 

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

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

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

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

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

493 

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

494 
(* theory > string * Term.typ > bool *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

495 

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

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

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

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

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

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

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

503 
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

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

505 

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

506 
(*  *) 
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

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

508 
(*  *) 
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

509 

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

510 
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

511 
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

512 
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

513 
 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

514 
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

515 
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

516 
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

517 
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

518 
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

519 

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

520 
(*  *) 
37405  521 
(* 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

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

523 

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

524 
(* theory > string * Term.typ > (string * Term.term) option *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

525 

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

526 
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

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

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

529 
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

530 
 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

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

532 
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

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

534 
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

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

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

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

538 
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

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

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

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

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

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

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

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

546 
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

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

548 
 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

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

550 
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

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

552 

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

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

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

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

556 

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

557 
(* theory > Term.typ > (string * Term.term) option *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

558 

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

559 
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

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

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

562 
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

563 
 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

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

565 
(* Term.term > Term.typ option *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

566 
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

567 
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

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

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

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

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

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

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

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

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

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

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

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

579 
 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

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

581 
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

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

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

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

585 
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

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

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

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

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

590 
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

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

592 
 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

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

594 
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

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

596 

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

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

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

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

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

601 

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

602 
(* theory > string > (string * Term.term) option *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

603 

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

604 
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

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

606 
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

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

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

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

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

611 

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

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

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

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

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

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

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

618 
(*  *) 
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 
(* theory > Term.term > Term.term *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

621 

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

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

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

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

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

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

627 

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

628 
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

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

630 
(* Term.term > Term.term *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

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

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

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

637 
 Const (@{const_name 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

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

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

640 
 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

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

642 
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

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

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

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

646 
 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

647 
 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

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

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

650 
 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

651 
 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

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

653 
 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

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

655 
 Const (@{const_name Collect}, _) => t 
37677  656 
 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

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

658 
 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

659 
 Const (@{const_name Finite_Set.finite}, _) => t 
37388  660 
 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

661 
Type ("fun", [@{typ nat}, @{typ bool}])])) => t 
37388  662 
 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

663 
Type ("fun", [@{typ nat}, @{typ nat}])])) => t 
37388  664 
 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

665 
Type ("fun", [@{typ nat}, @{typ nat}])])) => t 
37388  666 
 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

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

668 
 Const (@{const_name List.append}, _) => t 
36130
9a672f7d488d
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
blanchet
parents:
35746
diff
changeset

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

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

671 
 Const (@{const_name gfp}, _) => t 
36130
9a672f7d488d
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
blanchet
parents:
35746
diff
changeset

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

673 
 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

674 
 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

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

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

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

678 
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

679 
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

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

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

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

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

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

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

686 
(* '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

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

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

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

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

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

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

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

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

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

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

697 
 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

698 
 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

699 
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

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

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

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

703 

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

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

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

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

707 
(*  *) 
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

708 

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

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

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

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

712 

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

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

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

715 
(* "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

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

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

718 

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

719 
(* theory > Term.term > Term.term list *) 
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

720 

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

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

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

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

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

725 

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

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

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

728 

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

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

730 
let 
32950  731 
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

732 
val axioms = 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

733 
fun collect_this_axiom (axname, ax) axs = 
33246  734 
let 
735 
val ax' = unfold_defs thy ax 

736 
in 

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

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

739 
end 

740 
and collect_sort_axioms T axs = 

741 
let 

742 
val sort = 

743 
(case T of 

744 
TFree (_, sort) => sort 

745 
 TVar (_, sort) => sort 

746 
 _ => raise REFUTE ("collect_axioms", 

747 
"type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable")) 

748 
(* obtain axioms for all superclasses *) 

749 
val superclasses = sort @ maps (Sign.super_classes thy) sort 

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

751 
(* duplicate axioms anyway: *) 

752 
val superclasses = distinct (op =) superclasses 

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

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

755 
(#axioms (AxClass.get_info thy class) handle ERROR _ => [])) 

756 
superclasses 

757 
(* replace the (at most one) schematic type variable in each axiom *) 

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

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

760 
(case Term.add_tvars ax [] of 

761 
[] => (axname, ax) 

762 
 [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) 

763 
 _ => 

764 
raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ 

765 
Syntax.string_of_term_global thy ax ^ 

766 
") contains more than one type variable"))) 

767 
class_axioms 

768 
in 

769 
fold collect_this_axiom monomorphic_class_axioms axs 

770 
end 

771 
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

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

773 
(* simple types *) 
33246  774 
Type ("prop", []) => axs 
775 
 Type ("fun", [T1, T2]) => collect_type_axioms T2 (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

776 
(* axiomatic type classes *) 
33246  777 
 Type ("itself", [T1]) => collect_type_axioms T1 axs 
778 
 Type (s, Ts) => 

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

780 
SOME info => (* inductive datatype *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

781 
(* only collect relevant type axioms for the argument types *) 
33246  782 
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

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

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

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

786 
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

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

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

789 
(* at least collect relevant type axioms for the argument types *) 
33246  790 
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

791 
(* axiomatic type classes *) 
33246  792 
 TFree _ => collect_sort_axioms T axs 
793 
(* axiomatic type classes *) 

794 
 TVar _ => collect_sort_axioms T axs 

795 
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

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

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

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

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

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

801 
(* axiomatic type classes *) 
33246  802 
 Const (@{const_name 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

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

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

805 
 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

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

807 
 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

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

809 
 Const (@{const_name False}, _) => axs 
33246  810 
 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

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

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

813 
val ax = specialize_type thy (@{const_name The}, T) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

814 
(the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

816 
collect_this_axiom ("HOL.the_eq_trivial", ax) axs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

818 
 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

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

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

821 
(the (AList.lookup (op =) axioms "Hilbert_Choice.someI")) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

823 
collect_this_axiom ("Hilbert_Choice.someI", ax) axs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

824 
end 
33246  825 
 Const (@{const_name All}, T) => collect_type_axioms T axs 
826 
 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

827 
 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

828 
 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

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

830 
 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

831 
(* sets *) 
33246  832 
 Const (@{const_name Collect}, T) => collect_type_axioms T axs 
37677  833 
 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

834 
(* other optimizations *) 
33246  835 
 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

836 
 Const (@{const_name Finite_Set.finite}, T) => 
33246  837 
collect_type_axioms T axs 
37388  838 
 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

839 
Type ("fun", [@{typ nat}, @{typ bool}])])) => 
33246  840 
collect_type_axioms T axs 
37388  841 
 Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat}, 
842 
Type ("fun", [@{typ nat}, @{typ nat}])])) => 

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

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

33246  849 
collect_type_axioms T axs 
850 
 Const (@{const_name List.append}, T) => collect_type_axioms T axs 

36130
9a672f7d488d
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
blanchet
parents:
35746
diff
changeset

851 
(* UNSOUND 
33246  852 
 Const (@{const_name lfp}, T) => collect_type_axioms T axs 
853 
 Const (@{const_name gfp}, T) => collect_type_axioms T axs 

36130
9a672f7d488d
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
blanchet
parents:
35746
diff
changeset

854 
*) 
33246  855 
 Const (@{const_name fst}, T) => collect_type_axioms T axs 
856 
 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

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

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

859 
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

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

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

862 
let 
33246  863 
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

864 
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) 
33246  865 
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

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

867 
handle Type.TYPE_MATCH => NONE 
33246  868 
val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in 
869 
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

870 
in 
33246  871 
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

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

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

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

875 
(* only collect relevant type axioms *) 
33246  876 
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

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

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

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

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

881 
(* only collect relevant type axioms *) 
33246  882 
collect_type_axioms T axs 
883 
 Free (_, T) => collect_type_axioms T axs 

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

885 
 Bound _ => axs 

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

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

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

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

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

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

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

893 

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

894 
(*  *) 
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

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

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

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

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

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

900 
(*  *) 
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

901 

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

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

903 
let 
29272  904 
fun collect_types T acc = 
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24928
diff
changeset

905 
(case T of 
29272  906 
Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) 
39046
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

907 
 Type ("prop", []) => acc 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

908 
 Type (s, Ts) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

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

914 
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

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

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

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

918 
val _ = if Library.exists (fn d => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

919 
case d of Datatype_Aux.DtTFree _ => false  _ => true) typs then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

920 
raise REFUTE ("ground_types", "datatype argument (for type " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

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

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

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

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

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

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

931 
Datatype_Aux.DtTFree _ => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

933 
 Datatype_Aux.DtType (_, ds) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

934 
collect_types dT (fold_rev collect_dtyp ds acc) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

937 
acc (* prevent infinite recursion *) 
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 
let 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

940 
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

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

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

943 
val acc_dT = if Library.exists (fn (_, ds) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

944 
Library.exists Datatype_Aux.is_rec_type ds) dconstrs then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

948 
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

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

950 
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

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

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

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

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

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

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

957 
(* added by 'collect_dtyp' automatically *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

958 
collect_dtyp (Datatype_Aux.DtRec index) acc 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

963 
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

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

965 
 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

966 
in 
29272  967 
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

968 
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

969 

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

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

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

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

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 

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

977 
(* Term.typ > string *) 
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

978 

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

979 
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

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

981 
 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

982 

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

985 
(* '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

986 
(* '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

987 
(*  *) 
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

988 

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

989 
(* Term.typ list > (string * int) list > int > (Term.typ * int) list *) 
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

990 

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

991 
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

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

993 
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

994 
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

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

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

998 
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

999 
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

1000 

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

1001 
(*  *) 
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

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

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

1004 
(* '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

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

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

1007 

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

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

1009 
(Term.typ * int) list option *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1010 

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

1011 
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

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

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

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

1015 
(* int > int > int > int list option *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

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

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

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

1022 
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

1023 
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

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

1025 
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

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

1027 
(* all list elements x (unless 'max'<0) *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

1028 
(* int > int > int > int list > int list option *) 
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

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

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

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

1033 
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

1034 
 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

1035 
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

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

1037 
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

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

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

1040 
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

1041 
(* only consider those types for which the size is not fixed *) 
33317  1042 
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

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

1044 
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

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

1046 
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

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

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

1049 
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

1050 
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

1051 
(* return the fixed size *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1052 
SOME n => ((T, n), ds) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1054 
 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

1055 
xs diffs')) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1057 
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

1058 

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

1059 
(*  *) 
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

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

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

1062 
(*  *) 
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

1063 

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

1064 
(* interpretation > prop_formula *) 
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

1065 

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

1066 
fun toTrue (Leaf [fm, _]) = fm 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1067 
 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

1068 

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

1069 
(*  *) 
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

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

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

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

1073 
(*  *) 
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

1074 

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

1075 
(* interpretation > prop_formula *) 
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

1076 

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

1077 
fun toFalse (Leaf [_, fm]) = fm 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1078 
 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

1079 

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

1080 
(*  *) 
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

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

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

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

1084 
(* thy : the current theory *) 
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

1085 
(* {...} : 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

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

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

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

1089 
(*  *) 
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

1090 

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

1091 
(* theory > params > Term.term > bool > unit *) 
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

1092 

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

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

1094 
{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

1095 
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

1096 
let 
33054
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1097 
(* string > unit *) 
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1098 
fun check_expect outcome_code = 
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1099 
if expect = "" orelse outcome_code = expect then () 
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1100 
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

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

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

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

1104 
val timer = Timer.startRealTimer () 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1106 
if no_assms then t 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1107 
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

1108 
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

1109 
val u = unfold_defs thy t 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1110 
val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1111 
val axioms = collect_axioms thy u 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1112 
(* Term.typ list *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1113 
val types = fold (union (op =) o ground_types thy) (u :: axioms) [] 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1114 
val _ = tracing ("Ground types: " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1115 
^ (if null types then "none." 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1116 
else commas (map (Syntax.string_of_typ_global thy) types))) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

1120 
val maybe_spurious = Library.exists (fn 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

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

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

1127 
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

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

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

1130 
Library.exists (fn (_, ds) => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1131 
Library.exists Datatype_Aux.is_rec_type ds) constrs 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

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

1137 
warning ("Term contains a recursive datatype; " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1138 
^ "countermodel(s) may be spurious!") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

1142 
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

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

1144 
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

1145 
val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1146 
orelse raise TimeLimit.TimeOut 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1147 
val init_model = (universe, []) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1148 
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

1149 
bounds = [], wellformed = True} 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1150 
val _ = tracing ("Translating term (sizes: " 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1151 
^ 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

1152 
(* translate 'u' and all axioms *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1153 
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

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

1155 
val (i, m', a') = interpret thy m a t' 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1157 
(* set 'def_eq' to 'true' *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1159 
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

1160 
wellformed = #wellformed a'})) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1161 
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

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

1163 
(* add the wellformedness side condition *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1164 
val fm_u = (if negate then toFalse else toTrue) (hd intrs) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1165 
val fm_ax = PropLogic.all (map toTrue (tl intrs)) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1166 
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u] 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1168 
(if satsolver = "dpll" orelse satsolver = "enumerate" then 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1169 
warning ("Using SAT solver " ^ quote satsolver ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1170 
"; for better performance, consider installing an \ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1171 
\external solver.") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

1174 
SatSolver.invoke_solver satsolver 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1176 
error ("Unknown SAT solver: " ^ quote satsolver ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1177 
". Available solvers: " ^ 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1178 
commas (map (quote o fst) (!SatSolver.solvers)) ^ ".") 
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22093
diff
changeset

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

1180 
priority "Invoking SAT solver..."; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1182 
SatSolver.SATISFIABLE assignment => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1183 
(priority ("*** Model found: ***\n" ^ print_model thy model 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1185 
if maybe_spurious then "potential" else "genuine") 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1186 
 SatSolver.UNSATISFIABLE _ => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1187 
(priority "No model exists."; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1188 
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

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

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

1191 
"Search terminated, no larger universe within the given limits."; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

1194 
(priority "No model found."; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1195 
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

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

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

1198 
"Search terminated, no larger universe within the given limits."; 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1199 
"unknown"))) handle SatSolver.NOT_CONFIGURED => 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

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

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

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

1204 
(priority ("Search terminated, number of Boolean variables (" 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

1205 
^ string_of_int maxvars ^ " allowed) exceeded."); 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1207 

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

1208 
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

1209 
in 
33054
dd1192a96968
fixed the "expect" mechanism of Refute in the face of timeouts
blanchet
parents:
32952
diff
changeset

1210 
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

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

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

1213 
(* some parameter sanity checks *) 
5b38730f3e12
tuned whitespace and indentation, emphasizing the logical structure of this long text;
wenzelm
parents:
38864
diff
changeset

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

1215 
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

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

1217 
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

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

1219 
error ("\"maxsize\" (=" ^ string_of_int maxsize ^ 