author  webertj 
Thu, 25 Nov 2004 19:25:03 +0100  
changeset 15334  d5a92997dc1b 
parent 15333  77b2bca7fcb5 
child 15335  f81e6e24351f 
permissions  rwrr 
14350  1 
(* Title: HOL/Tools/refute.ML 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

4 
Copyright 20032004 

5 

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

14965  9 
(* TODO: case, recursion, size for IDTs are not supported yet *) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

10 

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

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

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

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

16 
signature REFUTE = 

17 
sig 

18 

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

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

20 

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

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

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

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

24 

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

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

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

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

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

31 

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

32 
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

33 
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

34 

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

35 
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

36 

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

37 
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

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

39 

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

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

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

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

43 

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

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

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

46 
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

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

48 

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

49 
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

50 

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

51 
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

52 
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

53 
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

54 

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

55 
val setup : (theory > theory) list 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

57 

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

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

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

60 

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

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

62 

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

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

66 
(* 'error'. *) 

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

67 
exception REFUTE of string * string; (* ("in function", "cause") *) 
14350  68 

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

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

71 
exception MAXVARS_EXCEEDED; 
14350  72 

73 
(*  *) 

74 
(* TREES *) 

75 
(*  *) 

76 

77 
(*  *) 

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

79 
(* of (lists of ...) elements *) 

80 
(*  *) 

81 

82 
datatype 'a tree = 

83 
Leaf of 'a 

84 
 Node of ('a tree) list; 

85 

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

87 

88 
fun tree_map f tr = 

89 
case tr of 

90 
Leaf x => Leaf (f x) 

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

92 

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

94 

95 
fun tree_foldl f = 

96 
let 

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

98 
 itl (e, Node xs) = foldl (tree_foldl f) (e,xs) 

99 
in 

100 
itl 

101 
end; 

102 

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

104 

105 
fun tree_pair (t1,t2) = 

106 
case t1 of 

107 
Leaf x => 

108 
(case t2 of 

109 
Leaf y => Leaf (x,y) 

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

111 
 Node xs => 

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

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

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

117 

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

118 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 

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

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

141 
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

142 
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

143 
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

144 
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

145 
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

146 
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

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

148 

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

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

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

151 
(* 'interpretation' *) 
14350  152 
(*  *) 
153 

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

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

155 
prop_formula list tree; 
14350  156 

157 
(*  *) 

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

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

159 
(* terms *) 
14350  160 
(*  *) 
161 

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

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

163 
(Term.typ * int) list * (Term.term * interpretation) list; 
14350  164 

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

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

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

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

168 

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

169 
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

170 
{ 
e8ccb13d7774
major code change: refute can now 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 
(* just passed unchanged from '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

172 
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

173 
(* these may change during the translation *) 
e8ccb13d7774
major code change: refute can now 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 
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

175 
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

176 
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

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

178 

14350  179 

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

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

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

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

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

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

185 
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

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

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

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

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

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

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

192 
{interpreters = in2, printers = pr2, parameters = pa2}) = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

194 
printers = rev (merge_alists (rev pr1) (rev pr2)), 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

197 
Pretty.writeln (Pretty.chunks 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

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

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

202 

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

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

204 

14350  205 

206 
(*  *) 

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

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

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

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

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

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

213 

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

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

215 
(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of 
15334
d5a92997dc1b
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
webertj
parents:
15333
diff
changeset

216 
None => raise REFUTE ("interpret", "unable to interpret term " ^ quote (Sign.string_of_term (sign_of thy) t)) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

217 
 Some x => x); 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

218 

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

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

220 
(* print: tries to convert the constant denoted by the term 't' into a 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

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

222 
(*  *) 
14350  223 

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

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

225 

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

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

227 
(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) 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

228 
None => Const ("<<no printer available>>", fastype_of 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

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

230 

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

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

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

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

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

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

236 

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

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

238 

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

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

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

241 
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

242 
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

243 
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

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

245 
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

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

248 
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

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

250 
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

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

253 
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

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

255 
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

256 
space_implode "\n" (mapfilter (fn (t,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

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

258 
if (!show_consts) orelse not (is_Const t) 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

259 
Some (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment)) 
e8ccb13d7774
major code change: refute can now 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 
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

261 
None) terms) ^ "\n" 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

262 
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

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

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

265 

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

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

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

272 

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

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

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

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

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

277 
case assoc (interpreters, name) of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

278 
None => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

281 

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

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

283 

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

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

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

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

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

288 
case assoc (printers, name) of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

289 
None => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

292 

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

295 
(* parameter table *) 
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 

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

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

299 

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

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

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

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

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

304 
case Symtab.lookup (parameters, name) of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

305 
None => RefuteData.put 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

306 
{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

307 
 Some _ => RefuteData.put 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

308 
{interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy 
14350  309 
end; 
310 

311 
(*  *) 

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

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

313 
(* RefuteData's parameter table *) 
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 

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

316 
(* theory > string > string option *) 
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 
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

319 

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

322 
(* stored in RefuteData's parameter table *) 
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 

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

325 
(* theory > (string * string) list *) 
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 
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

328 

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

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

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

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

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

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

334 

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

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

336 

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

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

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

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

340 
fun read_int (parms, name) = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

341 
case assoc_string (parms, name) of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

342 
Some s => (case Int.fromString s of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

345 
 None => error ("parameter " ^ quote name ^ " must be assigned a value") 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

347 
fun read_string (parms, name) = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

348 
case assoc_string (parms, name) of 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

349 
Some s => s 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

350 
 None => error ("parameter " ^ quote name ^ " must be assigned a value") 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

352 
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

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

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

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

356 
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

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

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

359 
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

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

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

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

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

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

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

366 
(fn (name,value) => (case Int.fromString value of SOME i => Some (name, i)  NONE => 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

367 
(filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"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 
allparams) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

369 
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

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

371 
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

372 

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

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

377 

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

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

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

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

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

382 

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

383 
(* TODO: to make the collection of axioms more easily extensible, this *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

386 

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

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

388 

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

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

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

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

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

393 

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

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

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

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

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

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

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

400 

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

402 
let 
14984  403 
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

404 
(* (string * 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 
val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

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

408 
(* variables in 't' are instantiated to match the 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

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

410 
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

411 
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

412 
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

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

414 
Some (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

415 
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

416 
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

417 
handle Type.TYPE_MATCH => 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

418 
 find_typeSubs (Free _) = 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

419 
 find_typeSubs (Var _) = 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

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

421 
 find_typeSubs (Abs (_, _, body)) = find_typeSubs 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

422 
 find_typeSubs (t1 $ t2) = (case find_typeSubs t1 of Some x => Some x  None => find_typeSubs 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

423 
val typeSubs = (case find_typeSubs 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

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

425 
 None => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of 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

426 
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

427 
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

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

430 
case Vartab.lookup (typeSubs, v) 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

431 
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

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

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

434 
 Some 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

435 
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

436 
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

437 
end 
15280  438 
(* applies a type substitution 'typeSubs' for all type variables in a *) 
439 
(* term 't' *) 

440 
(* Term.typ Term.Vartab.table > Term.term > Term.term *) 

441 
fun monomorphic_term typeSubs t = 

442 
map_term_types (map_type_tvar 

443 
(fn (v,_) => 

444 
case Vartab.lookup (typeSubs, v) of 

445 
None => 

446 
(* schematic type variable not instantiated *) 

447 
raise ERROR 

448 
 Some typ => 

449 
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

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

451 
fun 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

452 
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

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

454 
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

455 
 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

456 
 Type ("set", [T1]) => collect_type_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

457 
 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

458 
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

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

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

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

462 
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

463 
 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

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

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

466 
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

467 
if s'="Typedef.type_definition" 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

468 
Some 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

469 
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

470 
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

471 
 type_of_type_definition (Free _) = 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

472 
 type_of_type_definition (Var _) = 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

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

474 
 type_of_type_definition (Abs (_, _, body)) = type_of_type_definition 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

475 
 type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of Some x => Some x  None => type_of_type_definition 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

476 
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

477 
case type_of_type_definition ax 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

478 
Some 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

479 
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

480 
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

481 
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

482 
in 
15280  483 
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

484 
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

485 
 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

486 
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

487 
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

488 
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

489 
 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

490 
 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

491 
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

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

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

494 
(* only collect relevant type axioms for the argument 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

495 
foldl collect_type_axioms (axs, 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

496 
 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

497 
(case get_typedefn axioms 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

498 
Some (axname, 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

499 
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

500 
(* collect relevant type axioms for the argument 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

501 
foldl collect_type_axioms (axs, 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

502 
else 
14984  503 
(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

504 
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

505 
 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

506 
(* at least collect relevant type axioms for the argument 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

507 
foldl collect_type_axioms (axs, 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

508 
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

509 
(* TODO: include sort axioms *) 
14984  510 
 TFree (_, sorts) => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs) 
511 
 TVar (_, sorts) => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs) 

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

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

513 
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

514 
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

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

516 
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

517 
 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

518 
 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

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

520 
 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

521 
 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

522 
 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

523 
 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

524 
 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

525 
 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

526 
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

527 
val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial")) 
e8ccb13d7774
major code change: refute can now 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 
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

529 
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

530 
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

531 
else 
14984  532 
(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

533 
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

534 
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

535 
 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

536 
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

537 
val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI")) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

538 
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

539 
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

540 
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

541 
else 
14984  542 
(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

543 
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

544 
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

545 
 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

546 
 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

547 
 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

548 
 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

549 
 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

550 
 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

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

552 
 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

553 
 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

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

555 
 Const ("Finite_Set.card", 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

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

557 
 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

558 
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

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

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

561 
fun get_defn [] = 
e8ccb13d7774
major code change: refute can now 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 
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

563 
 get_defn ((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

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

565 
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

566 
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

567 
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

568 
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

569 
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

570 
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

571 
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

572 
in 
15280  573 
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

574 
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

575 
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

576 
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

577 
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

578 
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

579 
 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

580 
 Type.TYPE_MATCH => 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

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

582 
fun is_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

583 
(case body_type 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

584 
Type (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

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

586 
Some 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

587 
Library.exists (fn 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

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

589 
Const (cname, ctype) => 
14810
4b4b97d29370
adjusted for different signature of Type.typ_instance
webertj
parents:
14807
diff
changeset

590 
cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype) 
14807
e8ccb13d7774
major code change: refute can now 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 
 _ => 
e8ccb13d7774
major code change: refute can now 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 
raise REFUTE ("collect_axioms", "IDT constructor is not a constant"))) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

593 
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

594 
 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

595 
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

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

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

599 
fun is_IDT_recursor () = 
e8ccb13d7774
major code change: refute can now 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 
(* the type of a recursion operator: [T1,...,Tn,IDT]>TResult (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

601 
(* the T1,...,Tn depend on the types of the datatype's 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

602 
((case last_elem (binder_types 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

603 
Type (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

604 
(case DatatypePackage.datatype_info thy s' of 
15333  605 
Some info => s mem (#rec_names info) 
606 
 None => false) (* not an 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

607 
 _ => (* a (free or schematic) type 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

608 
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

609 
handle LIST "last_elem" => false) (* not even a function 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

610 
in 
15125  611 
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

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

613 
collect_type_axioms (axs, T) 
15125  614 
else if is_IDT_recursor () then ( 
615 
(* TODO: we must add the definition of the recursion operator to the axioms, or *) 

616 
(* (better yet, since simply unfolding the definition won't work for *) 

617 
(* initial fragments of recursive IDTs) write an interpreter that *) 

618 
(* respects it *) 

619 
warning "Term contains recursion over a datatype; countermodel(s) may be spurious!"; 

620 
(* only collect relevant type axioms *) 

621 
collect_type_axioms (axs, T) 

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

623 
(case get_defn axioms 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

624 
Some (axname, 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

625 
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

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

627 
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

628 
else 
14984  629 
(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

630 
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

631 
 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

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

633 
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

634 
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

635 
 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

636 
 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

637 
 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

638 
 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

639 
 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

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

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

642 
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

643 
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

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

645 
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

646 
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

647 
foldl 
e8ccb13d7774
major code change: refute can now 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 
(fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),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

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

650 
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

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

652 
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

653 
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

654 
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

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

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

657 

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

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

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

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

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

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

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

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

665 

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

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

667 

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

668 
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

669 
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

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

671 
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

672 
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

673 
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

674 
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

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

676 
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

677 
 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

678 
 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

679 
 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

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

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

682 
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

683 
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

684 
val descr = #descr 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

685 
val (_, dtyps, constrs) = (the o assoc) (descr, index) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

686 
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

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

688 
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

689 
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

690 
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

691 
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

692 
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

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

694 
(* DatatypeAux.descr > (DatatypeAux.dtyp * Term.typ) list > DatatypeAux.dtyp > Term.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

695 
fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree 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

696 
(* replace a 'DtTFree' variable by the associated 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

697 
(the o assoc) (typ_assoc, DatatypeAux.DtTFree 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

698 
 typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

699 
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

700 
val (s, ds, _) = (the o assoc) (descr, i) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

701 
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

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

703 
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

704 
 typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

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

707 
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

708 
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

709 
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

710 
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

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

712 
val acc_args = foldr collect_types (Ts, 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

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

714 
val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

715 
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

716 
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

717 
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

718 
 None => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *) 
e8ccb13d7774
major code change: refute can now 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 
T ins (foldr collect_types (Ts, 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

720 
 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

721 
 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

722 
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

723 
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

724 
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

725 

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

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

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

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

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

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

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

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

734 

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

736 
 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

737 
 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

738 

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

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

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

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

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

746 

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

748 
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

749 
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

750 
case assoc (sizes, string_of_typ 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

751 
Some n => 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

752 
 None => 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

753 
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

754 
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

755 
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

756 

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

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

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

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

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

763 

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

765 

14807
e8ccb13d7774
major code change: refute can now 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 
fun next_universe xs sizes minsize maxsize = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

767 
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

768 
(* int > int list > int list 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

769 
fun add1 _ [] = 
e8ccb13d7774
major code change: refute can now 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 
None (* overflow *) 
e8ccb13d7774
major code change: refute can now 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 
 add1 max (x::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

772 
if x<max orelse max<0 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

773 
Some ((x+1)::xs) (* add 1 to the head *) 
e8ccb13d7774
major code change: refute can now 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 
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

775 
apsome (fn xs' => 0 :: xs') (add1 max xs) (* carryover *) 
e8ccb13d7774
major code change: refute can now 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 
(* int > int list * int list > int list 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

777 
fun shift _ (_, []) = 
e8ccb13d7774
major code change: refute can now 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 
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

779 
 shift max (zeros, x::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

780 
if x=0 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

781 
shift max (0::zeros, xs) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

782 
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

783 
apsome (fn xs' => (x1) :: (zeros @ xs')) (add1 max 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

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

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

786 
(* int > int > int > int list 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

787 
fun make_first 0 sum _ = 
e8ccb13d7774
major code change: refute can now 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 sum=0 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

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

791 
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

792 
 make_first len sum max = 
e8ccb13d7774
major code change: refute can now 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 
if sum<=max orelse max<0 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

794 
apsome (fn xs' => sum :: xs') (make_first (len1) 0 max) 
e8ccb13d7774
major code change: refute can now 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 
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

796 
apsome (fn xs' => max :: xs') (make_first (len1) (summax) max) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

798 
(* all list elements x (unless 'max'<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

799 
(* int > int list > int list 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

800 
fun next max 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

801 
(case shift max ([], xs) 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

802 
Some 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

803 
Some 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

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

805 
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

806 
val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs) 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

807 
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

808 
make_first len (sum+1) max (* increment 'sum' by 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

809 
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

810 
(* only consider those types for which the size is not fixed *) 
e8ccb13d7774
major code change: refute can now 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 
val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) 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

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

813 
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

814 
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

815 
case next (maxsizeminsize) diffs 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

816 
Some diffs' => 
e8ccb13d7774
major code change: refute can now 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 
(* merge with those types for which the size is fixed *) 
e8ccb13d7774
major code change: refute can now 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 
Some (snd (foldl_map (fn (ds, (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

819 
case assoc (sizes, string_of_typ 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

820 
Some n => (ds, (T, n)) (* return the fixed size *) 
e8ccb13d7774
major code change: refute can now 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 
 None => (tl ds, (T, minsize + (hd ds)))) (* consume the head of 'ds', add '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

822 
(diffs', 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

823 
 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

824 
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

825 
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

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

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

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

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

833 

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

834 
fun toTrue (Leaf [fm,_]) = fm 
e8ccb13d7774
major code change: refute can now 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 
 toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); 
e8ccb13d7774
major code change: refute can now 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 

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

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

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

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

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

844 

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

845 
fun toFalse (Leaf [_,fm]) = fm 
e8ccb13d7774
major code change: refute can now 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 
 toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

847 

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

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

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

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

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

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

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

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

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

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

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

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

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

861 

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

862 
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

863 
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

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

865 
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

866 
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

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

868 
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

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

870 
val types = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], 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

871 
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

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

873 
else commas (map (Sign.string_of_typ (sign_of thy)) 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

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

875 
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

876 
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

877 
val init_model = (universe, []) 
e8ccb13d7774
major code change: refute can now 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 
val init_args = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True} 
14984  879 
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

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

881 
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

882 
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

883 
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

884 
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

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

886 
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

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

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

889 
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

890 
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

891 
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

892 
in 
14984  893 
immediate_output " invoking SAT solver..."; 
14965  894 
(case SatSolver.invoke_solver satsolver fm of 
895 
SatSolver.SATISFIABLE assignment => 

896 
writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b  None => true)) 

897 
 _ => (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *) 

14984  898 
(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

899 
case next_universe universe sizes minsize maxsize 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

900 
Some universe' => find_model_loop universe' 
14965  901 
 None => writeln "Search terminated, no larger universe within the given limits.")) 
902 
handle SatSolver.NOT_CONFIGURED => 

903 
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

904 
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

905 
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

906 
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

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

908 
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

909 
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

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

911 
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

912 
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

913 
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

914 
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

915 
assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", 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

916 
(* enter loop with/without time limit *) 
e8ccb13d7774
major code change: refute can now 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 
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

918 
^ Sign.string_of_term (sign_of 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

919 
if maxtime>0 then 
14965  920 
(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

921 
wrapper () 
14965  922 
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

923 
writeln ("\nSearch terminated, time limit (" 
14965  924 
^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") 
925 
^ ") exceeded.")) 

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

927 
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

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

929 

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

930 

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

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

932 
(* INTERFACE, PART 2: FINDING A MODEL *) 
14350  933 
(*  *) 
934 

935 
(*  *) 

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

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

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

938 
(* parameters *) 
14350  939 
(*  *) 
940 

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

941 
(* theory > (string * string) list > Term.term > unit *) 
14350  942 

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

943 
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

944 
find_model thy (actual_params thy params) t false; 
14350  945 

946 
(*  *) 

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

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

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

949 
(* parameters *) 
14350  950 
(*  *) 
951 

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

952 
(* theory > (string * string) list > Term.term > unit *) 
14350  953 

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

954 
fun refute_term thy params t = 
14350  955 
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

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

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

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

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

960 
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

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

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

963 
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

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

965 
val ex_closure = foldl 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

966 
(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t'))) 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

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

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

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

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

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

972 
(* its type. *) 
14350  973 
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

974 
find_model thy (actual_params thy params) ex_closure true 
14350  975 
end; 
976 

977 
(*  *) 

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

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

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

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

981 
(* subgoal : 0based index specifying the subgoal number *) 
14350  982 
(*  *) 
983 

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

984 
(* theory > (string * string) list > Thm.thm > int > unit *) 
14350  985 

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

986 
fun refute_subgoal thy params thm subgoal = 
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

987 
refute_term thy params (nth_elem (subgoal, prems_of thm)); 
14350  988 

989 

990 
(*  *) 

15292  991 
(* INTERPRETERS: Auxiliary Functions *) 
14350  992 
(*  *) 
993 

994 
(*  *) 

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

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

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

997 
(* 'True'/'False' only (no Boolean variables) *) 
14350  998 
(*  *) 
999 

14807
e8ccb13d7774
major code change: refute can now 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 
(* interpretation > interpretation list *) 
14350  1001 

14807
e8ccb13d7774
major code change: refute can now 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 
fun make_constants intr = 
14456
cca28ec5f9a6
support for nonrecursive IDTs, The, arbitrary, Hilbert_Choice.Eps
webertj
parents:
14351
diff
changeset

1003 
let 
14350  1004 
(* 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

1005 
(* int > interpretation list *) 
14350  1006 
fun unit_vectors n = 
1007 
let 

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

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

1009 
(* int * int > interpretation *) 
14350  1010 
fun unit_vector (k,n) = 
1011 
Leaf ((replicate (k1) False) @ (True :: (replicate (nk) False))) 

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

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

1015 
in 

1016 
unit_vectors_acc 1 [] 

1017 
end 

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

1019 
(* 'a > 'a list list > 'a list list *) 

1020 
fun cons_list x xss = 

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

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

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

1024 
fun pick_all 1 xs = 

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

1026 
 pick_all n xs = 

1027 
let val rec_pick = pick_all (n1) xs in 

1028 
foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs) 

1029 
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

1030 
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

1031 
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

1032 
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

1033 
 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

1034 
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

1035 

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

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

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

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

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

1040 

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

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

1042 

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

1043 
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

1044 
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

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

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

1047 
fun power (a,0) = 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

1048 
 power (a,1) = 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

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

1050 
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

1051 
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

1052 
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

1053 
 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

1054 
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

1055 

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

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

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

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

1059 

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

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

1061 

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

1062 
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

1063 

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

1064 
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

1065 

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

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

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

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

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

1070 

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

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

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

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

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

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

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

1077 

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

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

1079 

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

1080 
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

1081 
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

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

1083 
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

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

1085 
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

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

1087 
Leaf ys => PropLogic.dot_product (xs, ys) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1088 
 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

1089 
 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

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

1091 
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

1092 
 Node ys => PropLogic.all (map equal (xs ~~ ys)))) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

1094 
fun not_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

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

1096 
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

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

1098 
Leaf ys => PropLogic.all ((PropLogic.exists xs) :: (PropLogic.exists ys) :: 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1099 
(map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) (* defined and not equal *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1100 
 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

1101 
 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

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

1103 
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

1104 
 Node ys => PropLogic.exists (map not_equal (xs ~~ ys)))) 
14350  1105 
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

1106 
(* a value may be undefined; therefore 'not_equal' is not just the *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

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

1108 
(*  two interpretations are 'equal' iff they are both defined 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

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

1110 
(*  two interpretations are 'not_equal' iff they are both defined at *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1111 
(* least partially, and a defined part denotes different values *) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1112 
(*  an undefined interpretation is neither 'equal' nor 'not_equal' 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

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

1114 
Leaf [equal (i1, i2), not_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

1115 
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

1116 

15292  1117 
(*  *) 
1118 
(* eta_expand: etaexpands a term 't' by adding 'i' lambda abstractions *) 

1119 
(*  *) 

1120 

1121 
(* Term.term > int > Term.term *) 

1122 

1123 
fun eta_expand t i = 

1124 
let 

1125 
val Ts = binder_types (fastype_of t) 

1126 
in 

1127 
foldr (fn (T, t) => Abs ("<eta_expand>", T, t)) 

1128 
(take (i, Ts), list_comb (t, map Bound (i1 downto 0))) 

1129 
end; 

1130 

1131 

1132 
(*  *) 

1133 
(* INTERPRETERS: Actual Interpreters *) 

1134 
(*  *) 

14807
e8ccb13d7774
major code change: refute can now 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 
(* theory > model > arguments > Term.term > (interpretation * model * arguments) 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

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 
(* simply typed lambda calculus: Isabelle's basic term syntax, with 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

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

1140 

e8ccb13d7774
major code change: refute can now 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 
fun stlc_interpreter thy model args 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

1142 
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

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

1144 
val {maxvars, next_idx, bounds, wellformed} = args 
e8ccb13d7774
major code change: refute can now 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 
(* Term.typ > (interpretation * model * arguments) 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

1146 
fun interpret_groundterm 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

1147 
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

1148 
(* unit > (interpretation * model * arguments) 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

1149 
fun interpret_groundtype () = 
e8ccb13d7774
major code change: refute can now 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 
let 
15283  1151 
val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *) 
1152 
val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 1 or 2 *) 

1153 
val _ = (if next1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) 

14807
e8ccb13d7774
major code change: refute can now 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 
(* prop_formula list *) 
15283  1155 
val fms = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] 
14807
e8ccb13d7774
major code change: refute can now 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 
else (map BoolVar (next_idx upto (next_idx+size1)))) 
e8ccb13d7774
major code change: refute can now 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 
(* 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

1158 
val intr = Leaf fms 
e8ccb13d7774
major code change: refute can now 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 
(* prop_formula list > 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

1160 
fun one_of_two_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

1161 
 one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false 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

1162 
(* prop_formula list > 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

1163 
fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false 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

1164 
(* prop_formula *) 
15283  1165 
val wf = (if size=1 then True else if size=2 then True else exactly_one_true fms) 
14807
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1166 
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

1167 
(* extend the model, increase 'next_idx', add wellformedness 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

1168 
Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)}) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1169 
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

1170 
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

1171 
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

1172 
Type ("fun", [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

1173 
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

1174 
(* we create 'size_of_type (interpret (... T1))' different copies *) 
e8ccb13d7774
major code change: refute can now 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 
(* of the interpretation for 'T2', which are then combined into 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

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

1177 
val (i1, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1)) 
14807
e8ccb13d7774
major code change: refute can now 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 
(* make fresh copies, with different variable indices *) 
e8ccb13d7774
major code change: refute can now 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 
(* 'idx': next variable index *) 
e8ccb13d7774
major code change: refute can now 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 
(* 'n' : number of copies *) 
e8ccb13d7774
major code change: refute can now 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 
(* int > int > (int * interpretation list * 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

1182 
fun make_copies idx 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

1183 
(idx, [], 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

1184 
 make_copies idx 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

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

1186 
val (copy, _, new_args) = interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", 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

1187 
val (idx', copies, wf') = make_copies (#next_idx new_args) (n1) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1188 
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

1189 
(idx', copy :: copies, SAnd (#wellformed new_args, wf')) 
e8ccb13d7774
major code change: refute can now 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 
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

1191 
val (next, copies, wf) = make_copies next_idx (size_of_type 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

1192 
(* combine copies into a single 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

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

1194 
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

1195 
(* extend the model, increase 'next_idx', add wellformedness 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

1196 
Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)}) 
e8ccb13d7774
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
webertj
parents:
14604
diff
changeset

1197 
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

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

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

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

1201 
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
cha 