author  webertj 
Thu, 04 Jan 2007 00:12:30 +0100  
changeset 21985  acfb13e8819e 
parent 21931  314f9e2a442c 
child 21992  337990f42ce0 
permissions  rwrr 
14350  1 
(* Title: HOL/Tools/refute.ML 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

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

4 
Copyright 20032007 
14350  5 

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

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

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

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

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

14 
signature REFUTE = 

15 
sig 

16 

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

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

18 

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

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

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

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

22 

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

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

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

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

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

27 

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

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

29 

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

30 
val add_interpreter : string > (theory > model > arguments > Term.term > (interpretation * model * arguments) option) > theory > 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

31 
val add_printer : string > (theory > model > Term.term > interpretation > (int > bool) > Term.term option) > theory > theory 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

32 

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

33 
val interpret : theory > model > arguments > Term.term > (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

34 

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 
val print : theory > model > Term.term > interpretation > (int > bool) > Term.term 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

37 

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

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

43 
val get_default_param : theory > string > string option 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

44 
val get_default_params : theory > (string * string) 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

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

46 

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

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

48 

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

49 
val satisfy_term : theory > (string * string) list > Term.term > unit (* tries to find a model for a formula *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

50 
val refute_term : theory > (string * string) list > Term.term > unit (* tries to find a model that refutes a formula *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

51 
val refute_subgoal : theory > (string * string) list > Thm.thm > int > unit 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

52 

18708  53 
val setup : theory > theory 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

55 

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

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

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

58 

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

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

60 

14350  61 
(* We use 'REFUTE' only for internal error conditions that should *) 
62 
(* never occur in the first place (i.e. errors caused by bugs in our *) 

63 
(* code). Otherwise (e.g. to indicate invalid input data) we use *) 

64 
(* 'error'. *) 

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

65 
exception REFUTE of string * string; (* ("in function", "cause") *) 
14350  66 

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

67 
(* should be raised by an interpreter when more variables would be *) 
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

68 
(* required than allowed by 'maxvars' *) 
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

69 
exception MAXVARS_EXCEEDED; 
14350  70 

71 
(*  *) 

72 
(* TREES *) 

73 
(*  *) 

74 

75 
(*  *) 

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

77 
(* of (lists of ...) elements *) 

78 
(*  *) 

79 

80 
datatype 'a tree = 

81 
Leaf of 'a 

82 
 Node of ('a tree) list; 

83 

84 
(* ('a > 'b) > 'a tree > 'b tree *) 

85 

86 
fun tree_map f tr = 

87 
case tr of 

88 
Leaf x => Leaf (f x) 

89 
 Node xs => Node (map (tree_map f) xs); 

90 

91 
(* ('a * 'b > 'a) > 'a * ('b tree) > 'a *) 

92 

93 
fun tree_foldl f = 

94 
let 

95 
fun itl (e, Leaf x) = f(e,x) 

15570  96 
 itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs) 
14350  97 
in 
98 
itl 

99 
end; 

100 

101 
(* 'a tree * 'b tree > ('a * 'b) tree *) 

102 

15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

103 
fun tree_pair (t1, t2) = 
14350  104 
case t1 of 
105 
Leaf x => 

106 
(case t2 of 

107 
Leaf y => Leaf (x,y) 

108 
 Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)")) 

109 
 Node xs => 

110 
(case t2 of 

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

111 
(* '~~' will raise an exception if the number of branches 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

112 
(* both trees is different at the current node *) 
14350  113 
Node ys => Node (map tree_pair (xs ~~ ys)) 
114 
 Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)")); 

115 

116 
(*  *) 

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

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

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

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

120 
(* The following parameters are supported (and required (!), except for *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

135 

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

136 
type params = 
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

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

138 
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

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

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

141 
maxvars : int, 
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 
maxtime : int, 
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 
satsolver: string 
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 

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

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

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

148 
(* 'interpretation' *) 
14350  149 
(*  *) 
150 

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

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

152 
prop_formula list tree; 
14350  153 

154 
(*  *) 

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

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

156 
(* terms *) 
14350  157 
(*  *) 
158 

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

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

160 
(Term.typ * int) list * (Term.term * interpretation) list; 
14350  161 

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

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

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

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

165 

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

166 
type 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

167 
{ 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

168 
maxvars : int, (* just passed unchanged from 'params' *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

169 
def_eq : bool, (* whether to use 'make_equality' or 'make_def_equality' *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

170 
(* the following may change during the translation *) 
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

171 
next_idx : int, 
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

172 
bounds : interpretation 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

173 
wellformed: prop_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

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

175 

14350  176 

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

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

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

179 
val name = "HOL/refute"; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

181 
{interpreters: (string * (theory > model > arguments > Term.term > (interpretation * model * arguments) option)) 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

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

183 
parameters: string Symtab.table}; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

184 
val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

185 
val copy = I; 
16424  186 
val extend = I; 
187 
fun merge _ 

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

188 
({interpreters = in1, printers = pr1, parameters = pa1}, 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

189 
{interpreters = in2, printers = pr2, parameters = pa2}) = 
21098
d0d8a48ae4e6
switched merge_alists'' to AList.merge'' whenever appropriate
haftmann
parents:
21078
diff
changeset

190 
{interpreters = AList.merge (op =) (K true) (in1, in2), 
d0d8a48ae4e6
switched merge_alists'' to AList.merge'' whenever appropriate
haftmann
parents:
21078
diff
changeset

191 
printers = AList.merge (op =) (K true) (pr1, pr2), 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

192 
parameters = Symtab.merge (op=) (pa1, pa2)}; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

193 
fun print sg {interpreters, printers, parameters} = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

194 
Pretty.writeln (Pretty.chunks 
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

195 
[Pretty.strs ("default parameters:" :: List.concat (map (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))), 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

196 
Pretty.strs ("interpreters:" :: map fst interpreters), 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

197 
Pretty.strs ("printers:" :: map fst printers)]); 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

199 

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

200 
structure RefuteData = TheoryDataFun(RefuteDataArgs); 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

201 

14350  202 

203 
(*  *) 

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

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

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

206 
(* track of the interpretation of subterms *) 
14350  207 
(*  *) 
208 

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

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

210 

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

211 
fun interpret thy model args t = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

212 
(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

213 
NONE => raise REFUTE ("interpret", "no interpreter for term " ^ quote (Sign.string_of_term (sign_of thy) t)) 
15531  214 
 SOME x => x); 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

215 

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

216 
(*  *) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

217 
(* print: converts the constant denoted by the term 't' into a term using a *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

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

219 
(*  *) 
14350  220 

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

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

222 

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

223 
fun print thy model t intr assignment = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

224 
(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

225 
NONE => raise REFUTE ("print", "no printer for term " ^ quote (Sign.string_of_term (sign_of thy) t)) 
15531  226 
 SOME x => x); 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

227 

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

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

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

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

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

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

233 

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

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

235 

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

236 
fun print_model thy model assignment = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

238 
val (typs, terms) = model 
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

239 
val typs_msg = 
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

240 
if null typs then 
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

241 
"empty universe (no type variables in term)\n" 
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

242 
else 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

243 
"Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n" 
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

244 
val show_consts_msg = 
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

245 
if not (!show_consts) andalso Library.exists (is_Const o fst) terms then 
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

246 
"set \"show_consts\" to show the interpretation of constants\n" 
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

247 
else 
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

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

249 
val terms_msg = 
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

250 
if null terms then 
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

251 
"empty interpretation (no free variables in term)\n" 
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

252 
else 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

253 
space_implode "\n" (List.mapPartial (fn (t, intr) => 
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

254 
(* print constants only if 'show_consts' is 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

255 
if (!show_consts) orelse not (is_Const t) then 
15531  256 
SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment)) 
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

257 
else 
15531  258 
NONE) terms) ^ "\n" 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

259 
in 
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

260 
typs_msg ^ show_consts_msg ^ terms_msg 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

262 

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

263 

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

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

267 

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

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

269 

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

270 
fun add_interpreter name f thy = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

272 
val {interpreters, printers, parameters} = RefuteData.get thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

273 
in 
17314  274 
case AList.lookup (op =) interpreters name of 
15531  275 
NONE => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy 
276 
 SOME _ => error ("Interpreter " ^ name ^ " already declared") 

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

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

278 

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

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

280 

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

281 
fun add_printer name f thy = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

283 
val {interpreters, printers, parameters} = RefuteData.get thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

284 
in 
17314  285 
case AList.lookup (op =) printers name of 
15531  286 
NONE => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy 
287 
 SOME _ => error ("Printer " ^ name ^ " already declared") 

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

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

289 

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

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

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

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

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

294 

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

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

296 

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

297 
fun set_default_param (name, value) thy = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

299 
val {interpreters, printers, parameters} = RefuteData.get thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

300 
in 
17412  301 
case Symtab.lookup parameters name of 
15531  302 
NONE => RefuteData.put 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

303 
{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy 
15531  304 
 SOME _ => RefuteData.put 
17412  305 
{interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters} thy 
14350  306 
end; 
307 

308 
(*  *) 

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

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

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

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

312 

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

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

314 

17412  315 
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

316 

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

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

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

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

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

321 

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

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

323 

17261  324 
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

325 

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

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

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

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

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

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

331 

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

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

333 

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

334 
fun actual_params thy override = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

337 
fun read_int (parms, name) = 
17314  338 
case AList.lookup (op =) parms name of 
15531  339 
SOME s => (case Int.fromString s of 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

340 
SOME i => i 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

341 
 NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value")) 
15531  342 
 NONE => error ("parameter " ^ quote name ^ " must be assigned a value") 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

344 
fun read_string (parms, name) = 
17314  345 
case AList.lookup (op =) parms name of 
15531  346 
SOME s => s 
347 
 NONE => error ("parameter " ^ quote name ^ " must be assigned a value") 

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

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

349 
val allparams = override @ (get_default_params thy) (* 'override' first, defaults last *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

351 
val minsize = read_int (allparams, "minsize") 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

352 
val maxsize = read_int (allparams, "maxsize") 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

353 
val maxvars = read_int (allparams, "maxvars") 
20544  354 
val maxtime = read_int (allparams, "maxtime") 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

356 
val satsolver = read_string (allparams, "satsolver") 
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

357 
(* all remaining parameters of the form "string=int" are collected 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

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

359 
(* TODO: it is currently not possible to specify a size for a type *) 
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

360 
(* whose name is one of the other parameters (e.g. 'maxvars') *) 
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

361 
(* (string * int) list *) 
15570  362 
val sizes = List.mapPartial 
15531  363 
(fn (name,value) => (case Int.fromString value of SOME i => SOME (name, i)  NONE => NONE)) 
15570  364 
(List.filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver") 
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

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

366 
in 
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

367 
{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver} 
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

368 
end; 
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

369 

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

370 

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

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

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

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

374 

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

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

376 
(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *) 
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

377 
(* ('Term.typ'), given type parameters for the data type's type *) 
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

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

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

380 

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

381 
(* DatatypeAux.descr > (DatatypeAux.dtyp * Term.typ) list > DatatypeAux.dtyp > Term.typ *) 
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

382 

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

383 
fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = 
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

384 
(* replace a 'DtTFree' variable by the associated type *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

385 
(Option.valOf o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

386 
 typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

387 
Type (s, map (typ_of_dtyp descr typ_assoc) ds) 
15335
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

388 
 typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = 
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

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

390 
val (s, ds, _) = (Option.valOf o AList.lookup (op =) descr) i 
15335
f81e6e24351f
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj
parents:
15334
diff
changeset

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

392 
Type (s, map (typ_of_dtyp descr typ_assoc) ds) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

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

394 

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

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

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

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

398 

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

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

400 

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

401 
fun close_form t = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

403 
(* (Term.indexname * Term.typ) list *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

404 
val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

407 
(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

408 
(t, vars) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

410 

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

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

412 
(* monomorphic_term: applies a type substitution 'typeSubs' for all type *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

413 
(* variables in a term 't' *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

415 

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

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

417 

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

418 
fun monomorphic_term typeSubs t = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

420 
(fn v => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

421 
case Type.lookup (typeSubs, v) of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

423 
(* schematic type variable not instantiated *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

424 
raise REFUTE ("monomorphic_term", 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

425 
"no substitution for type variable " ^ fst (fst v) ^ 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

426 
" in term " ^ Display.raw_string_of_term t) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

427 
 SOME typ => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

428 
typ)) t; 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

429 

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

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

431 
(* specialize_type: given a constant 's' of type 'T', which is a subterm of *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

432 
(* 't', where 't' has a (possibly) more general type, the *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

433 
(* schematic type variables in 't' are instantiated to *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

434 
(* match the type 'T' (may raise Type.TYPE_MATCH) *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

436 

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

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

438 

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

439 
fun specialize_type thy (s, T) t = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

441 
fun find_typeSubs (Const (s', T')) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

442 
if s=s' then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

443 
SOME (Sign.typ_match thy (T', T) Vartab.empty) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

444 
handle Type.TYPE_MATCH => NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

447 
 find_typeSubs (Free _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

448 
 find_typeSubs (Var _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

449 
 find_typeSubs (Bound _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

450 
 find_typeSubs (Abs (_, _, body)) = find_typeSubs body 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

451 
 find_typeSubs (t1 $ t2) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

452 
(case find_typeSubs t1 of SOME x => SOME x 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

453 
 NONE => find_typeSubs t2) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

455 
case find_typeSubs t of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

456 
SOME typeSubs => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

459 
(* no match found  perhaps due to sort constraints *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

460 
raise Type.TYPE_MATCH 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

462 

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

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

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

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

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

467 

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

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

469 

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

470 
fun is_const_of_class thy (s, T) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

472 
val class_const_names = map Logic.const_of_class (Sign.all_classes thy) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

474 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

475 
(* or if we should also check the type 'T'. *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

478 

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

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

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

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

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

483 

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

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

485 

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

486 
fun is_IDT_constructor thy (s, T) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

487 
(case body_type T of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

488 
Type (s', _) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

489 
(case DatatypePackage.get_datatype_constrs thy s' of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

490 
SOME constrs => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

491 
List.exists (fn (cname, cty) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

492 
cname = s andalso Sign.typ_instance thy (T, cty)) constrs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

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

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

497 

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

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

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

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

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

502 

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

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

504 

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

505 
fun is_IDT_recursor thy (s, T) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

507 
val rec_names = Symtab.fold (append o #rec_names o snd) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

508 
(DatatypePackage.get_datatypes thy) [] 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

510 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

511 
(* or if we should also check the type 'T'. *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

514 

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

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

516 
(* get_def: looks up the definition of a constant, as created by "constdefs" *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

518 

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

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

520 

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

521 
fun get_def thy (s, T) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

523 
(* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

524 
fun norm_rhs eqn = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

526 
fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

527 
 lambda v t = raise TERM ("lambda", [v, t]) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

528 
val (lhs, rhs) = Logic.dest_equals eqn 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

529 
val (_, args) = Term.strip_comb lhs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

531 
fold lambda (rev args) rhs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

534 
fun get_def_ax [] = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

535 
 get_def_ax ((axname, ax) :: axioms) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

537 
val (lhs, _) = Logic.dest_equals ax (* equations only *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

538 
val c = Term.head_of lhs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

539 
val (s', T') = Term.dest_Const c 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

541 
if s=s' then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

543 
val typeSubs = Sign.typ_match thy (T', T) Vartab.empty 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

544 
val ax' = monomorphic_term typeSubs ax 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

545 
val rhs = norm_rhs ax' 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

547 
SOME (axname, rhs) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

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

551 
end handle ERROR _ => get_def_ax axioms 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

552 
 TERM _ => get_def_ax axioms 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

553 
 Type.TYPE_MATCH => get_def_ax axioms) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

555 
get_def_ax (Theory.all_axioms_of thy) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

557 

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

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

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

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

561 

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

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

563 

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

564 
fun get_typedef thy T = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

567 
fun get_typedef_ax [] = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

568 
 get_typedef_ax ((axname, ax) :: axioms) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

571 
fun type_of_type_definition (Const (s', T')) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

572 
if s'="Typedef.type_definition" then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

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

576 
 type_of_type_definition (Free _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

577 
 type_of_type_definition (Var _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

578 
 type_of_type_definition (Bound _) = NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

579 
 type_of_type_definition (Abs (_, _, body)) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

581 
 type_of_type_definition (t1 $ t2) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

582 
(case type_of_type_definition t1 of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

583 
SOME x => SOME x 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

584 
 NONE => type_of_type_definition t2) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

586 
case type_of_type_definition ax of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

587 
SOME T' => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

589 
val T'' = (domain_type o domain_type) T' 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

590 
val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

592 
SOME (axname, monomorphic_term typeSubs ax) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

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

596 
end handle ERROR _ => get_typedef_ax axioms 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

597 
 MATCH => get_typedef_ax axioms 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

598 
 Type.TYPE_MATCH => get_typedef_ax axioms) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

600 
get_typedef_ax (Theory.all_axioms_of thy) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

602 

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

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

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

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

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

607 

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

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

609 

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

610 
fun get_classdef thy class = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

612 
val axname = class ^ "_class_def" 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

614 
Option.map (pair axname) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

615 
(AList.lookup (op =) (Theory.all_axioms_of thy) axname) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

617 

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

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

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

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

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

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

625 

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

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

627 

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

628 
(* Note: we could intertwine unfolding of constants and beta(eta) *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

629 
(* normalization; this would save some unfolding for terms where *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

630 
(* constants are eliminated by betareduction (e.g. 'K c1 c2'). On *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

631 
(* the other hand, this would cause additional work for terms where *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

633 

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

634 
fun unfold_defs thy t = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

637 
fun unfold_loop t = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

640 
Const ("all", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

641 
 Const ("==", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

642 
 Const ("==>", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

643 
 Const ("TYPE", _) => t (* axiomatic type classes *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

645 
 Const ("Trueprop", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

646 
 Const ("Not", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

647 
 (* redundant, since 'True' is also an IDT constructor *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

648 
Const ("True", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

649 
 (* redundant, since 'False' is also an IDT constructor *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

650 
Const ("False", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

651 
 Const ("arbitrary", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

652 
 Const ("The", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

653 
 Const ("Hilbert_Choice.Eps", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

654 
 Const ("All", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

655 
 Const ("Ex", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

656 
 Const ("op =", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

657 
 Const ("op &", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

658 
 Const ("op ", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

659 
 Const ("op >", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

661 
 Const ("Collect", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

662 
 Const ("op :", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

664 
 Const ("Finite_Set.card", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

665 
 Const ("Finite_Set.Finites", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

666 
 Const ("Orderings.less", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

667 
 Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

668 
 Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

669 
 Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

670 
 Const ("List.op @", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

671 
 Const ("Lfp.lfp", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

672 
 Const ("Gfp.gfp", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

673 
 Const ("fst", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

674 
 Const ("snd", _) => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

676 
 Const (s, T) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

677 
(if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

678 
t (* do not unfold IDT constructors/recursors *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

679 
(* unfold the constant if there is a defining equation *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

680 
else case get_def thy (s, T) of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

681 
SOME (axname, rhs) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

682 
(* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

683 
(* occurs on the righthand side of the equation, i.e. in *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

684 
(* 'rhs', we must not use this equation to unfold, because *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

685 
(* that would loop. Here would be the right place to *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

686 
(* check this. However, getting this really right seems *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

687 
(* difficult because the user may state arbitrary axioms, *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

688 
(* which could interact with overloading to create loops. *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

689 
((*immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

690 
 NONE => t) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

691 
 Free _ => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

692 
 Var _ => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

693 
 Bound _ => t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

694 
 Abs (s, T, body) => Abs (s, T, unfold_loop body) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

695 
 t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

696 
val result = Envir.beta_eta_contract (unfold_loop t) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

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

700 

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

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

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

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

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

705 

15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

706 
(* Note: to make the collection of axioms more easily extensible, this *) 
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 
(* function could be based on usersupplied "axiom collectors", *) 
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 
(* similar to 'interpret'/interpreters or 'print'/printers *) 
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

709 

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

710 
(* Note: currently we use "inverse" functions to the definitional *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

711 
(* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

712 
(* "typedef", "constdefs". A more general approach could consider *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

713 
(* *every* axiom of the theory and collect it if it has a constant/ *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

715 

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

716 
(* theory > Term.term > Term.term 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

717 

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

718 
(* Which axioms are "relevant" for a particular term/type goes hand 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

719 
(* hand with the interpretation of that term/type by its interpreter (see *) 
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 
(* way below): if the interpretation respects an axiom anyway, the axiom *) 
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

721 
(* does not need to be added as a constraint here. *) 
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

722 

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

723 
(* To avoid collecting the same axiom multiple times, we use an *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

725 

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

726 
fun collect_axioms thy t = 
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

727 
let 
14984  728 
val _ = immediate_output "Adding axioms..." 
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

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

730 
val axioms = Theory.all_axioms_of thy 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

732 
fun collect_this_axiom (axname, ax) axs = 
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

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

734 
val ax' = unfold_defs thy ax 
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

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

736 
if member (op aconv) axs ax' then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

739 
immediate_output (" " ^ axname); 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

740 
collect_term_axioms (ax' :: axs, ax') 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

741 
) 
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

742 
end 
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

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

744 
and collect_sort_axioms (axs, T) = 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

747 
val sort = (case T of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

748 
TFree (_, sort) => sort 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

749 
 TVar (_, sort) => sort 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

750 
 _ => raise REFUTE ("collect_axioms", "type " ^ 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

751 
Sign.string_of_typ thy T ^ " is not a variable")) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

752 
(* obtain axioms for all superclasses *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

753 
val superclasses = sort @ (maps (Sign.super_classes thy) sort) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

754 
(* merely an optimization, because 'collect_this_axiom' disallows *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

756 
val superclasses = distinct (op =) superclasses 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

757 
val class_axioms = maps (fn class => map (fn ax => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

758 
("<" ^ class ^ ">", Thm.prop_of ax)) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

759 
(#axioms (AxClass.get_definition thy class) handle ERROR _ => [])) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

761 
(* replace the (at most one) schematic type variable in each axiom *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

762 
(* by the actual type 'T' *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

763 
val monomorphic_class_axioms = map (fn (axname, ax) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

764 
(case Term.term_tvars ax of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

765 
[] => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

766 
(axname, ax) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

767 
 [(idx, S)] => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

768 
(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

770 
raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

771 
Sign.string_of_term thy ax ^ 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

772 
") contains more than one type variable"))) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

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

775 
fold collect_this_axiom monomorphic_class_axioms axs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

776 
end 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

777 
(* Term.term list * Term.typ > Term.term list *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

778 
and collect_type_axioms (axs, 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

779 
case T of 
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

780 
(* simple types *) 
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

781 
Type ("prop", []) => axs 
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

782 
 Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2) 
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

783 
 Type ("set", [T1]) => collect_type_axioms (axs, T1) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

784 
 Type ("itself", [T1]) => collect_type_axioms (axs, T1) (* axiomatic type classes *) 
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

785 
 Type (s, Ts) => 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

786 
(case DatatypePackage.get_datatype thy s of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

787 
SOME info => (* inductive datatype *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

788 
(* only collect relevant type axioms for the argument types *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

789 
Library.foldl collect_type_axioms (axs, Ts) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

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

791 
(case get_typedef thy T of 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

792 
SOME (axname, ax) => 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

793 
collect_this_axiom (axname, ax) axs 
15531  794 
 NONE => 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

795 
(* unspecified type, perhaps introduced with "typedecl" *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

796 
(* at least collect relevant type axioms for the argument types *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

797 
Library.foldl collect_type_axioms (axs, Ts))) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

798 
 TFree _ => collect_sort_axioms (axs, T) (* axiomatic type classes *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

799 
 TVar _ => collect_sort_axioms (axs, T) (* axiomatic type classes *) 
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

800 
(* Term.term list * Term.term > Term.term 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

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

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

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

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

805 
 Const ("==", _) => axs 
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

806 
 Const ("==>", _) => axs 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

807 
 Const ("TYPE", T) => collect_type_axioms (axs, T) (* axiomatic type classes *) 
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

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

809 
 Const ("Trueprop", _) => axs 
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

810 
 Const ("Not", _) => axs 
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

811 
 Const ("True", _) => axs (* redundant, since 'True' is also an IDT constructor *) 
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

812 
 Const ("False", _) => axs (* redundant, since 'False' is also an IDT constructor *) 
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

813 
 Const ("arbitrary", T) => collect_type_axioms (axs, T) 
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

814 
 Const ("The", T) => 
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

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

816 
val ax = specialize_type thy ("The", T) ((Option.valOf o AList.lookup (op =) axioms) "HOL.the_eq_trivial") 
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

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

818 
collect_this_axiom ("HOL.the_eq_trivial", ax) axs 
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

819 
end 
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

820 
 Const ("Hilbert_Choice.Eps", T) => 
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

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

822 
val ax = specialize_type thy ("Hilbert_Choice.Eps", T) ((Option.valOf o AList.lookup (op =) axioms) "Hilbert_Choice.someI") 
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

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

824 
collect_this_axiom ("Hilbert_Choice.someI", ax) axs 
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

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

826 
 Const ("All", T) => collect_type_axioms (axs, T) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

827 
 Const ("Ex", T) => collect_type_axioms (axs, 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

828 
 Const ("op =", T) => collect_type_axioms (axs, T) 
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

829 
 Const ("op &", _) => axs 
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

830 
 Const ("op ", _) => axs 
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

831 
 Const ("op >", _) => axs 
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

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

833 
 Const ("Collect", T) => collect_type_axioms (axs, T) 
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

834 
 Const ("op :", T) => collect_type_axioms (axs, T) 
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

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

836 
 Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) 
15571  837 
 Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T) 
19277  838 
 Const ("Orderings.less", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T) 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18932
diff
changeset

839 
 Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18932
diff
changeset

840 
 Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18932
diff
changeset

841 
 Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) 
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

842 
 Const ("List.op @", T) => collect_type_axioms (axs, T) 
16050  843 
 Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) 
844 
 Const ("Gfp.gfp", T) => collect_type_axioms (axs, T) 

21267  845 
 Const ("fst", T) => collect_type_axioms (axs, T) 
846 
 Const ("snd", T) => collect_type_axioms (axs, 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

847 
(* simplytyped lambda calculus *) 
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

848 
 Const (s, T) => 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

849 
if is_const_of_class thy (s, T) then 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

850 
(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

851 
(* and the class definition *) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

852 
let 
18932  853 
val class = Logic.class_of_const s 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

854 
val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

855 
val ax_in = SOME (specialize_type thy (s, T) inclass) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

856 
(* type match may fail due to sort constraints *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

857 
handle Type.TYPE_MATCH => NONE 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

858 
val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax)) ax_in 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

859 
val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

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

861 
collect_type_axioms (fold collect_this_axiom 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

862 
(map_filter I [ax_1, ax_2]) axs, T) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

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

864 
else if is_IDT_constructor thy (s, T) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

865 
orelse is_IDT_recursor thy (s, T) then 
15125  866 
(* only collect relevant type axioms *) 
867 
collect_type_axioms (axs, T) 

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

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

869 
(* other constants should have been unfolded, with some *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

870 
(* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

871 
(* typedefs, or typeclass related constants *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

872 
(* only collect relevant type axioms *) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

873 
collect_type_axioms (axs, T) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

874 
 Free (_, T) => collect_type_axioms (axs, T) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

875 
 Var (_, T) => collect_type_axioms (axs, T) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

876 
 Bound i => axs 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

877 
 Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

878 
 t1 $ t2 => collect_term_axioms (collect_term_axioms (axs, t1), t2) 
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

879 
(* Term.term 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

880 
val result = map close_form (collect_term_axioms ([], t)) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

882 
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

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

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

885 

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

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

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

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

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

890 
(* 'propT'. For IDTs, also the argument types of constructors *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

893 

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

894 
(* theory > Term.term > Term.typ 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

895 

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 
fun ground_types thy t = 
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 
let 
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 
(* Term.typ * Term.typ list > Term.typ 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

899 
fun collect_types (T, acc) = 
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 
if T mem acc then 
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 
acc (* prevent infinite recursion (for 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

902 
else 
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

903 
(case T of 
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

904 
Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc)) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

905 
 Type ("prop", []) => acc 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

906 
 Type ("set", [T1]) => collect_types (T1, acc) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

907 
 Type (s, Ts) => 
19346  908 
(case DatatypePackage.get_datatype thy s of 
15531  909 
SOME info => (* inductive datatype *) 
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

910 
let 
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

911 
val index = #index info 
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

912 
val descr = #descr info 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

913 
val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index 
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

914 
val typ_assoc = dtyps ~~ Ts 
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

915 
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *) 
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

916 
val _ = (if Library.exists (fn d => 
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

917 
case d of DatatypeAux.DtTFree _ => false  _ => true) dtyps 
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

918 
then 
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

919 
raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") 
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

920 
else 
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

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

922 
(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *) 
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

923 
val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then 
20854  924 
insert (op =) T acc 
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

925 
else 
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

926 
acc) 
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

927 
(* collect argument types *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15571
diff
changeset

928 
val acc_args = foldr collect_types acc' Ts 
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

929 
(* collect constructor types *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15571
diff
changeset

930 
val acc_constrs = foldr collect_types acc_args (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs)) 
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

931 
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

932 
acc_constrs 
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

933 
end 
15531  934 
 NONE => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *) 
20854  935 
insert (op =) T (foldr collect_types acc Ts)) 
936 
 TFree _ => insert (op =) T acc 

937 
 TVar _ => insert (op =) T acc) 

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

938 
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

939 
it_term_types collect_types (t, []) 
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

940 
end; 
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

941 

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

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

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

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

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

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

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

948 

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

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

950 

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

951 
fun string_of_typ (Type (s, _)) = s 
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

952 
 string_of_typ (TFree (s, _)) = s 
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

953 
 string_of_typ (TVar ((s,_), _)) = s; 
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

954 

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

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

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

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

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

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

960 

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

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

962 

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

963 
fun first_universe xs sizes minsize = 
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

964 
let 
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

965 
fun size_of_typ T = 
17314  966 
case AList.lookup (op =) sizes (string_of_typ T) of 
15531  967 
SOME n => n 
968 
 NONE => minsize 

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

970 
map (fn T => (T, size_of_typ T)) xs 
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 
end; 
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 

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

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

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

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

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

979 

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

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

981 

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 
fun next_universe xs sizes minsize maxsize = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

983 
let 
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

984 
(* creates the "first" list of length 'len', where the sum of all 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

985 
(* elements is 'sum', and the length of the list is 'len' *) 
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 
(* int > int > int > int list option *) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

987 
fun make_first _ 0 sum = 
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

988 
if sum=0 then 
15531  989 
SOME [] 
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 
else 
15531  991 
NONE 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

992 
 make_first max len sum = 
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

993 
if sum<=max orelse max<0 then 
15570  994 
Option.map (fn xs' => sum :: xs') (make_first max (len1) 0) 
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

995 
else 
15570  996 
Option.map (fn xs' => max :: xs') (make_first max (len1) (summax)) 
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

997 
(* enumerates all int lists with a fixed length, where 0<=x<='max' for *) 
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

998 
(* all list elements x (unless 'max'<0) *) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

999 
(* int > int > int > int list > int list option *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1000 
fun next max len sum [] = 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1001 
NONE 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1002 
 next max len sum [x] = 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1003 
(* we've reached the last list element, so there's no shift possible *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1004 
make_first max (len+1) (sum+x+1) (* increment 'sum' by 1 *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1005 
 next max len sum (x1::x2::xs) = 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1006 
if x1>0 andalso (x2<max orelse max<0) then 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1007 
(* we can shift *) 
15570  1008 
SOME (valOf (make_first max (len+1) (sum+x11)) @ (x2+1) :: xs) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1009 
else 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1010 
(* continue search *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1011 
next max (len+1) (sum+x1) (x2::xs) 
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

1012 
(* only consider those types for which the size is not fixed *) 
17314  1013 
val mutables = List.filter (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs 
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

1014 
(* subtract 'minsize' from every size (will be added again at the end) *) 
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

1015 
val diffs = map (fn (_, n) => nminsize) mutables 
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

1016 
in 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1017 
case next (maxsizeminsize) 0 0 diffs of 
15531  1018 
SOME diffs' => 
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

1019 
(* merge with those types for which the size is fixed *) 
15531  1020 
SOME (snd (foldl_map (fn (ds, (T, _)) => 
17314  1021 
case AList.lookup (op =) sizes (string_of_typ T) of 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1022 
SOME n => (ds, (T, n)) (* return the fixed size *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1023 
 NONE => (tl ds, (T, minsize + hd ds))) (* consume the head of 'ds', add 'minsize' *) 
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

1024 
(diffs', xs))) 
15531  1025 
 NONE => 
1026 
NONE 

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

1027 
end; 
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

1028 

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

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

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

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

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

1033 

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

1034 
(* interpretation > prop_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

1035 

15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

1036 
fun toTrue (Leaf [fm, _]) = fm 
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

1037 
 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

1038 

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

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

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

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

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

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

1044 

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

1045 
(* interpretation > prop_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

1046 

15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

1047 
fun toFalse (Leaf [_, fm]) = fm 
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

1048 
 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

1049 

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

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

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

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

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

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

1055 
(* {...} : parameters that control the translation/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

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

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

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 
(* theory > params > Term.term > bool > unit *) 
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 

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 
fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t negate = 
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 
let 
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

1064 
(* unit > unit *) 
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 
fun wrapper () = 
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

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

1067 
val u = unfold_defs thy t 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1068 
val _ = writeln ("Unfolded term: " ^ Sign.string_of_term (sign_of thy) u) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1069 
val axioms = collect_axioms thy u 
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

1070 
(* Term.typ list *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1071 
val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], u :: axioms) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1072 
val _ = writeln ("Ground types: " 
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

1073 
^ (if null types then "none." 
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 
else commas (map (Sign.string_of_typ (sign_of thy)) types))) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1075 
(* we can only consider fragments of recursive IDTs, so we issue a *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1076 
(* warning if the formula contains a recursive IDT *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1077 
(* TODO: no warning needed for /positive/ occurrences of IDTs *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1078 
val _ = if Library.exists (fn 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1079 
Type (s, _) => 
19346  1080 
(case DatatypePackage.get_datatype thy s of 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1081 
SOME info => (* inductive datatype *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1082 
let 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1083 
val index = #index info 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1084 
val descr = #descr info 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1085 
val (_, _, constrs) = (Option.valOf o AList.lookup (op =) descr) index 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1086 
in 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1087 
(* recursive datatype? *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1088 
Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1089 
end 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1090 
 NONE => false) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1091 
 _ => false) types then 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1092 
warning "Term contains a recursive datatype; countermodel(s) may be spurious!" 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1093 
else 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

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

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

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

1097 
let 
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

1098 
val init_model = (universe, []) 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1099 
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True} 
14984  1100 
val _ = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1101 
(* translate 'u' and all axioms *) 
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

1102 
val ((model, args), intrs) = foldl_map (fn ((m, a), t') => 
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

1103 
let 
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

1104 
val (i, m', a') = interpret thy m a t' 
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

1105 
in 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1106 
(* set 'def_eq' to 'true' *) 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1107 
((m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'}), i) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1108 
end) ((init_model, init_args), u :: axioms) 
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1109 
(* make 'u' either true or false, and make all axioms true, 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

1110 
(* add the wellformedness side condition *) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1111 
val fm_u = (if negate then toFalse else toTrue) (hd intrs) 
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

1112 
val fm_ax = PropLogic.all (map toTrue (tl intrs)) 
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21931
diff
changeset

1113 
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u] 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1114 
in 
14984  1115 
immediate_output " invoking SAT solver..."; 
14965  1116 
(case SatSolver.invoke_solver satsolver fm of 
1117 
SatSolver.SATISFIABLE assignment => 

15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1118 
(writeln " model found!"; 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1119 
writeln ("*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b  NONE => true))) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
17412
diff
changeset

1120 
 SatSolver.UNSATISFIABLE _ => 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1121 
(immediate_output " no model exists.\n"; 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1122 
case next_universe universe sizes minsize maxsize of 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1123 
SOME universe' => find_model_loop universe' 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1124 
 NONE => writeln "Search terminated, no larger universe within the given limits.") 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1125 
 SatSolver.UNKNOWN => 
14984  1126 
(immediate_output " no model found.\n"; 
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

1127 
case next_universe universe sizes minsize maxsize of 
15531  1128 
SOME universe' => find_model_loop universe' 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1129 
 NONE => writeln "Search terminated, no larger universe within the given limits.") 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1130 
) handle SatSolver.NOT_CONFIGURED => 
14965  1131 
error ("SAT solver " ^ quote satsolver ^ " is not configured.") 
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

1132 
end handle MAXVARS_EXCEEDED => 
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

1133 
writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.") 
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

1134 
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

1135 
find_model_loop (first_universe types sizes minsize) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1136 
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

1137 
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

1138 
(* some parameter sanity checks *) 
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

1139 
assert (minsize>=1) ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); 
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

1140 
assert (maxsize>=1) ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); 
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

1141 
assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); 
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

1142 
assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); 
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

1143 
assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1144 
(* enter loop with or without time limit *) 
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

1145 
writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " 
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

1146 
^ Sign.string_of_term (sign_of thy) t); 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1147 
if maxtime>0 then ( 
18760  1148 
interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime)) 
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

1149 
wrapper () 
18760  1150 
handle Interrupt => 
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

1151 
writeln ("\nSearch terminated, time limit (" 
14965  1152 
^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") 
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1153 
^ ") exceeded.") 
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3valued logic with two kinds of equality; some bugfixes
webertj
parents:
15531
diff
changeset

1154 
) else 
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

1155 
wrapper () 
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

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

1157 

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

1158 

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

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

1160 
(* INTERFACE, PART 2: FINDING A MODEL *) 
14350  1161 
(*  *) 
1162 

1163 
(*  *) 

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

1164 
(* satisfy_term: calls 'find_model' to find a model that satisfies 't' *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1165 
(* params : list of '(name, value)' pairs used to override default *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1166 
(* parameters *) 
14350  1167 
(*  *) 
1168 

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

1169 
(* theory > (string * string) list > Term.term > unit *) 
14350  1170 

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

1171 
fun satisfy_term thy params 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

1172 
find_model thy (actual_params thy params) t false; 
14350  1173 

1174 
(*  *) 

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

1175 
(* refute_term: calls 'find_model' to find a model that refutes 't' *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1176 
(* params : list of '(name, value)' pairs used to override default *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1177 
(* parameters *) 
14350  1178 
(*  *) 
1179 

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

1180 
(* theory > (string * string) list > Term.term > unit *) 
14350  1181 

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

1182 
fun refute_term thy params t = 
14350  1183 
let 
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

1184 
(* disallow schematic type variables, since we cannot properly negate *) 
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

1185 
(* terms containing them (their logical meaning is that there EXISTS 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

1186 
(* type s.t. ...; to refute such a formula, we would have to show that *) 
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

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

1188 
val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables" 
21556  1189 

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

1190 
(* existential closure over schematic variables *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1191 
(* (Term.indexname * Term.typ) list *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1192 
val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1193 
(* Term.term *) 
15570  1194 
val ex_closure = Library.foldl 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

1195 
(fn (t', ((x, i), T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1196 
(t, vars) 
21556  1197 
(* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) 
1198 
(* 'HOLogic.exists_const' is not typecorrect. However, this is not *) 

1199 
(* really a problem as long as 'find_model' still interprets the *) 

1200 
(* resulting term correctly, without checking its type. *) 

1201 

1202 
(* replace outermost universally quantified variables by Free's: *) 

1203 
(* refuting a term with Free's is generally faster than refuting a *) 

1204 
(* term with (nested) quantifiers, because quantifiers are expanded, *) 

1205 
(* while the SAT solver searches for an interpretation for Free's. *) 

1206 
(* Also we get more information back that way, namely an *) 

1207 
(* interpretation which includes values for the (formerly) *) 

1208 
(* quantified variables. *) 

1209 
(* maps !!x1...xn. !xk...xm. t to t *) 

1210 
fun strip_all_body (Const ("all", _) $ Abs (_, _, t)) = strip_all_body t 

1211 
 strip_all_body (Const ("Trueprop", _) $ t) = strip_all_body t 

1212 
 strip_all_body (Const ("All", _) $ Abs (_, _, t)) = strip_all_body t 

1213 
 strip_all_body t = t 

1214 
(* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) 

1215 
fun strip_all_vars (Const ("all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t 

1216 
 strip_all_vars (Const ("Trueprop", _) $ t) = strip_all_vars t 
