author  paulson 
Tue, 27 May 1997 13:22:30 +0200  
changeset 3353  9112a2efb9a3 
parent 3332  3921ebbd9cf0 
child 3388  dbf61e36f8e9 
permissions  rwrr 
3302  1 
(* Title: TFL/thry 
2 
ID: $Id$ 

3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 
*) 

6 

2112  7 
structure Thry : Thry_sig (* LThry_sig *) = 
8 
struct 

9 

10 
structure USyntax = USyntax; 

11 
structure S = USyntax; 

12 

13 
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg}; 

14 

15 
(* 

16 
* Matching 

17 
**) 

18 

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

19 
local fun tybind (x,y) = (TVar (x,["term"]) , y) 
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

20 
fun tmbind (x,y) = (Var (x,type_of y), y) 
2112  21 
in 
22 
fun match_term thry pat ob = 

23 
let val tsig = #tsig(Sign.rep_sg(sign_of thry)) 

24 
val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) 

25 
in (map tmbind tm_theta, map tybind ty_theta) 

26 
end 

27 

28 
fun match_type thry pat ob = 

29 
map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob))) 

30 
end; 

31 

32 

33 
(* 

34 
* Typing 

35 
**) 

36 

37 
fun typecheck thry = cterm_of (sign_of thry); 

38 

39 

40 

41 
(* 

42 
* Making a definition. The argument "tm" looks like "f = WFREC R M". This 

43 
* entrypoint is specialized for interactive use, since it closes the theory 

44 
* after making the definition. This allows later interactive definitions to 

45 
* refer to previous ones. The name for the new theory is automatically 

46 
* generated from the name of the argument theory. 

47 
**) 

3191  48 

49 

50 
(* 

51 
* TFL attempts to make definitions where the lhs is a variable. Isabelle 

52 
* wants it to be a constant, so here we map it to a constant. Moreover, the 

53 
* theory should already have the constant, so we refrain from adding the 

54 
* constant to the theory. We just add the axiom and return the theory. 

55 
**) 

2112  56 
local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) 
57 
val Const(eeq_name, ty) = eeq 

58 
val prop = #2 (S.strip_type ty) 

59 
in 

60 
fun make_definition parent s tm = 

61 
let val {lhs,rhs} = S.dest_eq tm 

3332  62 
val (Name,Ty) = dest_Free lhs 
2112  63 
val lhs1 = S.mk_const{Name = Name, Ty = Ty} 
64 
val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty > Ty > prop} 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

65 
val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) 
3191  66 
val (_, tm', _) = Sign.infer_types (sign_of parent) 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

67 
(K None) (K None) [] true ([dtm],propT) 
3191  68 
val new_thy = add_defs_i [(s,tm')] parent 
2112  69 
in 
3191  70 
(freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) 
71 
end; 

2112  72 
end; 
73 

74 
(* 

75 
* Utility routine. Insert into list ordered by the key (a string). If two 

76 
* keys are equal, the new element replaces the old. A more efficient option 

77 
* for the future is needed. In fact, having the list of datatype facts be 

78 
* ordered is useless, since the lookup should never fail! 

79 
**) 

80 
fun insert (el as (x:string, _)) = 

81 
let fun canfind[] = [el] 

82 
 canfind(alist as ((y as (k,_))::rst)) = 

83 
if (x<k) then el::alist 

84 
else if (x=k) then el::rst 

85 
else y::canfind rst 

86 
in canfind 

87 
end; 

88 

89 

90 
(* 

91 
* A collection of facts about datatypes 

92 
**) 

93 
val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac) 

94 
val prod_record = 

95 
let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 

96 
(fn s => res_inst_tac [("p",s)] PairE_lemma) 

97 
fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s)) 

98 
in ("*", 

99 
{constructors = [const "Pair"], 

100 
case_const = const "split", 

101 
case_rewrites = [split RS eq_reflection], 

102 
case_cong = #case_cong prod_case_thms, 

103 
nchotomy = #nchotomy prod_case_thms}) 

104 
end; 

105 

106 
(* 

107 
* Hacks to make interactive mode work. Referring to "datatypes" directly 

108 
* is temporary, I hope! 

109 
**) 

110 
val match_info = fn thy => 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

111 
fn "*" => Some({case_const = #case_const (#2 prod_record), 
2112  112 
constructors = #constructors (#2 prod_record)}) 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

113 
 "nat" => Some({case_const = #case_const (#2 nat_record), 
2112  114 
constructors = #constructors (#2 nat_record)}) 
115 
 ty => case assoc(!datatypes,ty) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

116 
of None => None 
2112  117 
 Some{case_const,constructors, ...} => 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

118 
Some{case_const=case_const, constructors=constructors} 
2112  119 

120 
val induct_info = fn thy => 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

121 
fn "*" => Some({nchotomy = #nchotomy (#2 prod_record), 
2112  122 
constructors = #constructors (#2 prod_record)}) 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

123 
 "nat" => Some({nchotomy = #nchotomy (#2 nat_record), 
2112  124 
constructors = #constructors (#2 nat_record)}) 
125 
 ty => case assoc(!datatypes,ty) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

126 
of None => None 
2112  127 
 Some{nchotomy,constructors, ...} => 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

128 
Some{nchotomy=nchotomy, constructors=constructors} 
2112  129 

130 
val extract_info = fn thy => 

131 
let val case_congs = map (#case_cong o #2) (!datatypes) 

132 
val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes)) 

133 
in {case_congs = #case_cong (#2 prod_record):: 

134 
#case_cong (#2 nat_record)::case_congs, 

135 
case_rewrites = #case_rewrites(#2 prod_record)@ 

136 
#case_rewrites(#2 nat_record)@case_rewrites} 

137 
end; 

138 

139 
end; (* Thry *) 