author  wenzelm 
Sat, 11 Jun 2005 22:15:51 +0200  
changeset 16366  6ff17d08c3d5 
parent 16331  386ce655d694 
child 16424  18a07ad8fea8 
permissions  rwrr 
14350  1 
(* Title: HOL/Tools/refute.ML 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

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

4 
Copyright 20032005 
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 

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

53 
val setup : (theory > theory) list 
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; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

186 
val prep_ext = I; 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

187 
fun merge 
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}) = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

190 
{interpreters = rev (merge_alists (rev in1) (rev in2)), 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

191 
printers = rev (merge_alists (rev pr1) (rev pr2)), 
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 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

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

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 

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

315 
fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name); 
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 

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

324 
fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy; 
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) = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

345 
case assoc_string (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") 
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

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 *) 
15570  385 
(valOf o assoc) (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 
15570  390 
val (s, ds, _) = (valOf o assoc) (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 
(*  *) 
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

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

397 
(* of) all HOL axioms that are relevant w.r.t '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

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

399 

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

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

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

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

403 

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

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

405 

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

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

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

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

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

410 

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

411 
(* When an axiom is added as relevant, further axioms may need to 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

412 
(* added as well (e.g. when a constant is defined in terms of other *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

413 
(* constants). To avoid infinite recursion (which should not happen 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

414 
(* constants anyway, but it could happen for "typedef"related axioms, *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

415 
(* since they contain the type again), we use an accumulator 'axs' and *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

416 
(* add a relevant axiom only if it is not in 'axs' yet. *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

417 

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

418 
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

419 
let 
14984  420 
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

421 
(* (string * Term.term) list *) 
16331  422 
val axioms = Theory.all_axioms_of thy; 
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

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

424 
val rec_names = Symtab.foldl (fn (acc, (_, 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

425 
#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy) 
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

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

427 
val const_of_class_names = map Sign.const_of_class (Sign.classes (sign_of thy)) 
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

428 
(* given a constant 's' of type 'T', which is a subterm of 't', where *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

429 
(* 't' has a (possibly) more general type, the schematic type *) 
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

430 
(* variables in 't' are instantiated to match the type 'T' (may raise *) 
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

431 
(* Type.TYPE_MATCH) *) 
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

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

433 
fun specialize_type ((s, T), 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

434 
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

435 
fun find_typeSubs (Const (s', 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

436 
(if s=s' then 
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

437 
SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) handle Type.TYPE_MATCH => 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

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

439 
NONE) 
15531  440 
 find_typeSubs (Free _) = NONE 
441 
 find_typeSubs (Var _) = NONE 

442 
 find_typeSubs (Bound _) = 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

443 
 find_typeSubs (Abs (_, _, body)) = find_typeSubs body 
15531  444 
 find_typeSubs (t1 $ t2) = (case find_typeSubs t1 of SOME x => SOME x  NONE => find_typeSubs 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

445 
val typeSubs = (case find_typeSubs t of 
15531  446 
SOME x => x 
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

447 
 NONE => raise Type.TYPE_MATCH (* no match found  perhaps due to sort constraints *)) 
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

448 
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

449 
map_term_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

450 
(map_type_tvar 
15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

451 
(fn v => 
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

452 
case Type.lookup (typeSubs, v) of 
15531  453 
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

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

455 
raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")") 
15531  456 
 SOME typ => 
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

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

458 
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

459 
end 
15280  460 
(* applies a type substitution 'typeSubs' for all type variables in a *) 
461 
(* term 't' *) 

15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

462 
(* (Term.sort * Term.typ) Term.Vartab.table > Term.term > Term.term *) 
15280  463 
fun monomorphic_term typeSubs t = 
464 
map_term_types (map_type_tvar 

15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

465 
(fn v => 
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

466 
case Type.lookup (typeSubs, v) of 
15531  467 
NONE => 
15280  468 
(* schematic type variable not instantiated *) 
469 
raise ERROR 

15531  470 
 SOME typ => 
15280  471 
typ)) 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

472 
(* Term.term list * Term.typ > Term.term list *) 
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

473 
fun collect_sort_axioms (axs, T) = 
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

474 
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

475 
(* collect the axioms for a single 'class' (but not for its superclasses) *) 
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

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

477 
fun collect_class_axioms (axs, class) = 
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

478 
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

479 
(* obtain the axioms generated by the "axclass" command *) 
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

480 
(* (string * Term.term) list *) 
15570  481 
val class_axioms = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms 
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

482 
(* replace the one schematic type variable in each axiom by the actual type 'T' *) 
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

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

484 
val monomorphic_class_axioms = map (fn (axname, ax) => 
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

485 
let 
15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

486 
val (idx, S) = (case term_tvars ax 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

487 
[is] => is 
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

488 
 _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable")) 
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

489 
in 
15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15783
diff
changeset

490 
(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) 
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

491 
end) class_axioms 
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

492 
(* Term.term list * (string * Term.term) list > 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

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

494 
if mem_term (ax, axs) 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

495 
axs 
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

496 
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

497 
immediate_output (" " ^ axname); 
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

498 
collect_term_axioms (ax :: axs, ax) 
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

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

500 
in 
15570  501 
Library.foldl collect_axiom (axs, monomorphic_class_axioms) 
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

502 
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

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

504 
val sort = (case T 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

505 
TFree (_, sort) => sort 
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

506 
 TVar (_, sort) => sort 
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

507 
 _ => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable")) 
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

508 
(* obtain all superclasses of classes in 'sort' *) 
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

509 
(* string list *) 
16366  510 
val superclasses = Graph.all_succs ((#2 o #classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort 
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

511 
in 
15570  512 
Library.foldl collect_class_axioms (axs, superclasses) 
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

513 
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

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

515 
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

516 
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

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

518 
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

519 
 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

520 
 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

521 
 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

522 
 Type (s, 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

523 
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

524 
(* look up the definition of a type, as created by "typedef" *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

526 
fun get_typedefn [] = 
15531  527 
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

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

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

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

531 
fun type_of_type_definition (Const (s', 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

532 
if s'="Typedef.type_definition" then 
15531  533 
SOME 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

534 
else 
15531  535 
NONE 
536 
 type_of_type_definition (Free _) = NONE 

537 
 type_of_type_definition (Var _) = NONE 

538 
 type_of_type_definition (Bound _) = 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

539 
 type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body 
15531  540 
 type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of SOME x => SOME x  NONE => type_of_type_definition 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

541 
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

542 
case type_of_type_definition ax of 
15531  543 
SOME 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

544 
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

545 
val T'' = (domain_type o domain_type) 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

546 
val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', 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

547 
in 
15531  548 
SOME (axname, monomorphic_term typeSubs 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

549 
end 
15531  550 
 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

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

552 
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

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

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

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

556 
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

557 
case DatatypePackage.datatype_info thy s of 
15531  558 
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

559 
(* only collect relevant type axioms for the argument types *) 
15570  560 
Library.foldl collect_type_axioms (axs, Ts) 
15531  561 
 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

562 
(case get_typedefn axioms of 
15531  563 
SOME (axname, 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

564 
if mem_term (ax, axs) then 
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

565 
(* only collect relevant type axioms for the argument types *) 
15570  566 
Library.foldl collect_type_axioms (axs, 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

567 
else 
14984  568 
(immediate_output (" " ^ axname); 
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

569 
collect_term_axioms (ax :: axs, ax)) 
15531  570 
 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

571 
(* unspecified type, perhaps introduced with 'typedecl' *) 
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

572 
(* at least collect relevant type axioms for the argument types *) 
15570  573 
Library.foldl collect_type_axioms (axs, 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

574 
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

575 
 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

576 
 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

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

578 
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

579 
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

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

581 
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

582 
 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

583 
 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

584 
 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

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

586 
 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

587 
 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

588 
 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

589 
 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

590 
 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

591 
 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

592 
let 
15570  593 
val ax = specialize_type (("The", T), (valOf o assoc) (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

594 
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

595 
if mem_term (ax, axs) 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

596 
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

597 
else 
14984  598 
(immediate_output " 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

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

600 
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

601 
 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

602 
let 
15570  603 
val ax = specialize_type (("Hilbert_Choice.Eps", T), (valOf o assoc) (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

604 
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

605 
if mem_term (ax, axs) 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

606 
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

607 
else 
14984  608 
(immediate_output " 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

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

610 
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

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

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

613 
 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

614 
 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

615 
 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

616 
 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

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

618 
 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

619 
 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

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

621 
 Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) 
15571  622 
 Const ("Finite_Set.Finites", T) => collect_type_axioms (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

623 
 Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T) 
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

624 
 Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) 
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

625 
 Const ("op ", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) 
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

626 
 Const ("op *", 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

627 
 Const ("List.op @", T) => collect_type_axioms (axs, T) 
16050  628 
 Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) 
629 
 Const ("Gfp.gfp", 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

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

631 
 Const (s, 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

632 
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

633 
(* look up the definition of a constant, as created by "constdefs" *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

634 
(* string > Term.typ > (string * Term.term) list > (string * Term.term) option *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

635 
fun get_defn [] = 
15531  636 
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

637 
 get_defn ((axname, ax)::axms) = 
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

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

639 
val (lhs, _) = Logic.dest_equals ax (* equations only *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

642 
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

643 
if s=s' 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

644 
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

645 
val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', 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

646 
in 
15531  647 
SOME (axname, monomorphic_term typeSubs 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

648 
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

649 
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

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

651 
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

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

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

654 
 Type.TYPE_MATCH => get_defn axms) 
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

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

656 
(* unit > bool *) 
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

657 
fun is_const_of_class () = 
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

658 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
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

659 
(* or if we should also check the type 'T' *) 
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

660 
s mem const_of_class_names 
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

661 
(* inductive data types *) 
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

662 
(* unit > bool *) 
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

663 
fun is_IDT_constructor () = 
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

664 
(case body_type T 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

665 
Type (s', _) => 
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

666 
(case DatatypePackage.constrs_of thy s' 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

667 
SOME 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

668 
Library.exists (fn c => 
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

669 
(case c 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

670 
Const (cname, ctype) => 
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

671 
cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype) 
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

672 
 _ => 
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

673 
raise REFUTE ("collect_axioms", "IDT constructor is not a constant"))) 
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

674 
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

675 
 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

676 
false) 
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

677 
 _ => 
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

678 
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

679 
(* unit > bool *) 
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

680 
fun is_IDT_recursor () = 
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

681 
(* I'm not quite sure if checking the name 's' is sufficient, *) 
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

682 
(* or if we should also check the type 'T' *) 
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

683 
s mem rec_names 
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

684 
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

685 
if is_const_of_class () 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

686 
(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *) 
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

687 
(* the introduction rule "class.intro" as axioms *) 
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

688 
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

689 
val class = Sign.class_of_const s 
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

690 
val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) 
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

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

692 
val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE) 
15570  693 
val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => 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

694 
val axs' = (case ofclass_ax of NONE => axs  SOME ax => if mem_term (ax, axs) 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

695 
(* collect relevant type axioms *) 
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

696 
collect_type_axioms (axs, T) 
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

697 
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

698 
(immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax); 
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

699 
collect_term_axioms (ax :: axs, ax))) 
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

700 
val axs'' = (case intro_ax of NONE => axs'  SOME ax => if mem_term (ax, axs') 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

701 
(* collect relevant type axioms *) 
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

702 
collect_type_axioms (axs', T) 
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

703 
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

704 
(immediate_output (" " ^ class ^ ".intro"); 
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

705 
collect_term_axioms (ax :: axs', ax))) 
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 
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

707 
axs'' 
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

708 
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

709 
else if is_IDT_constructor () then 
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

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

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

712 
else if is_IDT_recursor () then 
15125  713 
(* only collect relevant type axioms *) 
714 
collect_type_axioms (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

715 
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

716 
case get_defn axioms of 
15531  717 
SOME (axname, 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

718 
if mem_term (ax, axs) 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

719 
(* collect relevant type axioms *) 
e8ccb13d7774
major code change: refute can now 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 
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

721 
else 
14984  722 
(immediate_output (" " ^ axname); 
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

723 
collect_term_axioms (ax :: axs, ax)) 
15531  724 
 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

725 
(* collect relevant type axioms *) 
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

726 
collect_type_axioms (axs, T) 
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

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

728 
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

729 
 Free (_, 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

730 
 Var (_, 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

731 
 Bound i => 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

732 
 Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body) 
e8ccb13d7774
major code change: refute can now 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 
 t1 $ t2 => collect_term_axioms (collect_term_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

734 
(* universal closure over schematic 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

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

736 
fun close_form 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

737 
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

738 
(* (Term.indexname * 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

739 
val vars = sort_wrt (fst o fst) (map dest_Var (term_vars 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

740 
in 
15570  741 
Library.foldl 
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

742 
(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x, i), 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

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

744 
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

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

746 
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

747 
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

748 
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

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

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

751 

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

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

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

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

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

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

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

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

759 

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

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

761 

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

762 
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

763 
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

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

765 
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

766 
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

767 
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

768 
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

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

770 
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

771 
 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

772 
 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

773 
 Type (s, 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

774 
(case DatatypePackage.datatype_info thy s of 
15531  775 
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

776 
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

777 
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

778 
val descr = #descr info 
15570  779 
val (_, dtyps, constrs) = (valOf o assoc) (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

780 
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

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

782 
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

783 
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

784 
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

785 
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

786 
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

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

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

789 
val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs 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

790 
T ins 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

791 
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

792 
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

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

794 
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

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

796 
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

797 
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

798 
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

799 
end 
15531  800 
 NONE => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15571
diff
changeset

801 
T ins (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

802 
 TFree _ => T ins 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

803 
 TVar _ => T ins 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

804 
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

805 
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

806 
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

807 

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

808 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

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

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

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

813 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 

e8ccb13d7774
major code change: refute can now 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 
(* 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

816 

e8ccb13d7774
major code change: refute can now 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 
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

818 
 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

819 
 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

820 

e8ccb13d7774
major code change: refute can now 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 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

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

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

826 

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

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

828 

e8ccb13d7774
major code change: refute can now 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 
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

830 
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

831 
fun size_of_typ 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

832 
case assoc (sizes, string_of_typ T) of 
15531  833 
SOME n => n 
834 
 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

835 
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

836 
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

837 
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

838 

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

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

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

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

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

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

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

845 

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

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

847 

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

848 
fun next_universe xs sizes minsize maxsize = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

849 
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

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

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

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

853 
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

854 
if sum=0 then 
15531  855 
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

856 
else 
15531  857 
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

858 
 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

859 
if sum<=max orelse max<0 then 
15570  860 
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

861 
else 
15570  862 
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

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

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

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

866 
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

867 
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

868 
 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

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

870 
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

871 
 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

872 
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

873 
(* we can shift *) 
15570  874 
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

875 
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

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

877 
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

878 
(* only consider those types for which the size is not fixed *) 
15570  879 
val mutables = List.filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) 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

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

881 
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

882 
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

883 
case next (maxsizeminsize) 0 0 diffs of 
15531  884 
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

885 
(* merge with those types for which the size is fixed *) 
15531  886 
SOME (snd (foldl_map (fn (ds, (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

887 
case assoc (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

888 
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

889 
 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

890 
(diffs', xs))) 
15531  891 
 NONE => 
892 
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

893 
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

894 

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

895 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

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

898 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 

e8ccb13d7774
major code change: refute can now 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 
(* 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

901 

15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

902 
fun toTrue (Leaf [fm, _]) = fm 
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

903 
 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

904 

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

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

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

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

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

909 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 

e8ccb13d7774
major code change: refute can now 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 
(* 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

912 

15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

913 
fun toFalse (Leaf [_, fm]) = fm 
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15611
diff
changeset

914 
 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

915 

e8ccb13d7774
major code change: refute can now 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 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

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

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

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

921 
(* {...} : 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

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

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

924 
(* Note: exception 'TimeOut' is raised if the algorithm does not terminate *) 
e8ccb13d7774
major code change: refute can now 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 
(* within 'maxtime' seconds (if 'maxtime' >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

926 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 

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

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

929 

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

930 
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

931 
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

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

933 
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

934 
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

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

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

937 
(* Term.typ list *) 
15570  938 
val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: 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

939 
val _ = writeln ("Ground 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

940 
^ (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

941 
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

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

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

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

945 
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

946 
Type (s, _) => 
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

947 
(case DatatypePackage.datatype_info thy s 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

948 
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

949 
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

950 
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

951 
val descr = #descr info 
15570  952 
val (_, _, constrs) = (valOf o assoc) (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

953 
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

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

955 
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

956 
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

957 
 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

958 
 _ => 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

959 
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

960 
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

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

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

963 
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

964 
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

965 
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

966 
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True} 
14984  967 
val _ = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") 
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

968 
(* translate 't' and all axioms *) 
e8ccb13d7774
major code change: refute can now 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 
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

970 
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

971 
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

972 
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

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

974 
((m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'}), i) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

975 
end) ((init_model, init_args), t :: axioms) 
e8ccb13d7774
major code change: refute can now 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 
(* make 't' either true or false, and make all axioms true, and *) 
e8ccb13d7774
major code change: refute can now 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 
(* add the wellformedness side condition *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

978 
val fm_t = (if negate then toFalse else toTrue) (hd intrs) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

979 
val fm_ax = PropLogic.all (map toTrue (tl intrs)) 
e8ccb13d7774
major code change: refute can now 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 
val fm = PropLogic.all [#wellformed args, fm_ax, fm_t] 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

981 
in 
14984  982 
immediate_output " invoking SAT solver..."; 
14965  983 
(case SatSolver.invoke_solver satsolver fm of 
984 
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

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

986 
writeln ("*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b  NONE => 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

987 
 SatSolver.UNSATISFIABLE => 
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

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

989 
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

990 
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

991 
 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

992 
 SatSolver.UNKNOWN => 
14984  993 
(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

994 
case next_universe universe sizes minsize maxsize of 
15531  995 
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

996 
 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

997 
) handle SatSolver.NOT_CONFIGURED => 
14965  998 
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

999 
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

1000 
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

1001 
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

1002 
find_model_loop (first_universe types sizes minsize) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1003 
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

1004 
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

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

1006 
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

1007 
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

1008 
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

1009 
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

1010 
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

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

1012 
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

1013 
^ 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

1014 
if maxtime>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

1015 
TimeLimit.timeLimit (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

1016 
wrapper () 
14965  1017 
handle TimeLimit.TimeOut => 
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

1018 
writeln ("\nSearch terminated, time limit (" 
14965  1019 
^ 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

1020 
^ ") 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

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

1022 
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

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

1024 

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

1025 

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

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

1027 
(* INTERFACE, PART 2: FINDING A MODEL *) 
14350  1028 
(*  *) 
1029 

1030 
(*  *) 

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

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

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

1033 
(* parameters *) 
14350  1034 
(*  *) 
1035 

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

1036 
(* theory > (string * string) list > Term.term > unit *) 
14350  1037 

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

1038 
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

1039 
find_model thy (actual_params thy params) t false; 
14350  1040 

1041 
(*  *) 

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

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

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

1044 
(* parameters *) 
14350  1045 
(*  *) 
1046 

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

1047 
(* theory > (string * string) list > Term.term > unit *) 
14350  1048 

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

1049 
fun refute_term thy params t = 
14350  1050 
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

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

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

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

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

1055 
val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables" 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1056 
(* existential closure over schematic variables *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1057 
(* (Term.indexname * Term.typ) list *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1058 
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

1059 
(* Term.term *) 
15570  1060 
val ex_closure = Library.foldl 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

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

1062 
(t, vars) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1063 
(* If 't' is of type 'propT' (rather than 'boolT'), applying *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1064 
(* 'HOLogic.exists_const' is not typecorrect. However, 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

1065 
(* is not really a problem as long as 'find_model' still *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1066 
(* interprets the resulting term correctly, without checking *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1067 
(* its type. *) 
14350  1068 
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

1069 
find_model thy (actual_params thy params) ex_closure true 
14350  1070 
end; 
1071 

1072 
(*  *) 

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

1073 
(* refute_subgoal: calls 'refute_term' on a specific subgoal *) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

1076 
(* subgoal : 0based index specifying the subgoal number *) 
14350  1077 
(*  *) 
1078 

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

1079 
(* theory > (string * string) list > Thm.thm > int > unit *) 
14350  1080 

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

1081 
fun refute_subgoal thy params thm subgoal = 
15570  1082 
refute_term thy params (List.nth (prems_of thm, subgoal)); 
14350  1083 

1084 

1085 
(*  *) 

15292  1086 
(* INTERPRETERS: Auxiliary Functions *) 
14350  1087 
(*  *) 
1088 

1089 
(*  *) 

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

1090 
(* make_constants: returns all interpretations that have the same tree *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1091 
(* structure as 'intr', but consist of unit vectors with *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1092 
(* 'True'/'False' only (no Boolean variables) *) 
14350  1093 
(*  *) 
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 
(* interpretation > interpretation list *) 
14350  1096 

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

1097 
fun make_constants intr = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1098 
let 
14350  1099 
(* returns a list with all unit vectors of length n *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1100 
(* int > interpretation list *) 
14350  1101 
fun unit_vectors n = 
1102 
let 

1103 
(* returns the kth unit vector of length n *) 

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

1104 
(* int * int > interpretation *) 
14350  1105 
fun unit_vector (k,n) = 
1106 
Leaf ((replicate (k1) False) @ (True :: (replicate (nk) False))) 

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

1107 
(* int > interpretation list > interpretation list *) 
14350  1108 
fun unit_vectors_acc k vs = 
1109 
if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs) 

1110 
in 

1111 
unit_vectors_acc 1 [] 

1112 
end 

1113 
(* concatenates 'x' with every list in 'xss', returning a new list of lists *) 

1114 
(* 'a > 'a list list > 'a list list *) 

1115 
fun cons_list x xss = 

1116 
map (fn xs => x::xs) xss 

1117 
(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *) 

1118 
(* int > 'a list > 'a list list *) 

1119 
fun pick_all 1 xs = 

1120 
map (fn x => [x]) xs 

1121 
 pick_all n xs = 

1122 
let val rec_pick = pick_all (n1) xs in 

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

1123 
Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs) 
14350  1124 
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

1125 
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

1126 
case intr 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

1127 
Leaf xs => unit_vectors (length 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

1128 
 Node xs => map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd 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

1129 
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

1130 

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

1131 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 
(* size_of_type: returns the number of constants in a type (i.e. 'length *) 
e8ccb13d7774
major code change: refute can now 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 
(* (make_constants intr)', but implemented more efficiently) *) 
e8ccb13d7774
major code change: refute can now 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 
(*  *) 
e8ccb13d7774
major code change: refute can now 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 

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

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

1137 

e8ccb13d7774
major code change: refute can now 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 
fun size_of_type intr = 
e8ccb13d7774
major code change: refute can now 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 
let 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

1140 
(* power (a, b) computes a^b, for a>=0, b>=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

1141 
(* int * int > int *) 
15611
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

1142 
fun power (a, 0) = 1 
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

1143 
 power (a, 1) = a 
c01f11cd08f9
Bugfix related to the interpretation of IDT constructors
webertj
parents:
15574
diff
changeset

1144 
 power (a, b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) 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

1145 
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

1146 
case intr 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

1147 
Leaf xs => length 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

1148 
 Node xs => power (size_of_type (hd xs), length 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

1149 
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

1150 

e8ccb13d7774
major code change: refute can now 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 
(*  *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1152 
(* TT/FF: interpretations that denote "true" or "false", respectively *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

1154 

e8ccb13d7774
major code change: refute can now 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 
(* 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

1156 

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

1157 
val TT = Leaf [True, 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

1158 

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

1159 
val FF = Leaf [False, 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

1160 

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

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

1162 
(* make_equality: returns an interpretation that denotes (extensional) *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1163 
(* equality of two interpretations *) 
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

1164 
(*  two interpretations are 'equal' iff they are both defined and denote *) 
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

1165 
(* the same value *) 
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

1166 
(*  two interpretations are 'not_equal' iff they are both defined at least *) 
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

1167 
(* partially, and a defined part denotes different values *) 
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

1168 
(*  a completely undefined interpretation is neither 'equal' nor *) 
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

1169 
(* 'not_equal' to another 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

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

1171 

e8ccb13d7774
major code change: refute can now 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 
(* We could in principle represent '=' on a type T by a particular *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1173 
(* interpretation. However, the size of that interpretation is quadratic *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1174 
(* in the size of T. Therefore comparing the interpretations 'i1' and *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1175 
(* 'i2' directly is more efficient than constructing 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

1176 
(* for equality on T first, and "applying" this interpretation to 'i1' *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1177 
(* and 'i2' in the usual way (cf. 'interpretation_apply') 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

1178 

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

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

1180 

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

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

1182 
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

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

1184 
fun equal (i1, i2) = 
e8ccb13d7774
major code change: refute can now 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 
(case i1 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

1186 
Leaf 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

1187 
(case i2 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

1188 
Leaf ys => PropLogic.dot_product (xs, ys) (* defined and equal *) 
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

1189 
 Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1190 
 Node 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

1191 
(case i2 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

1192 
Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1193 
 Node ys => PropLogic.all (map equal (xs ~~ ys)))) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and c 