author  paulson 
Thu, 22 May 1997 15:13:16 +0200  
changeset 3302  404fe31fd8d2 
parent 3245  241838c01caf 
child 3332  3921ebbd9cf0 
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 

12 
open Mask; 

13 
structure S = USyntax; 

14 

15 

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

17 

18 
(* 

19 
* Matching 

20 
**) 

21 

22 
local open Utils 

23 
infix 3 > 

24 
fun tybind (x,y) = TVar (x,["term"]) > y 

25 
fun tmbind (x,y) = Var (x,type_of y) > y 

26 
in 

27 
fun match_term thry pat ob = 

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

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

30 
in (map tmbind tm_theta, map tybind ty_theta) 

31 
end 

32 

33 
fun match_type thry pat ob = 

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

35 
end; 

36 

37 

38 
(* 

39 
* Typing 

40 
**) 

41 

42 
fun typecheck thry = cterm_of (sign_of thry); 

43 

44 

45 

46 
(* 

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

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

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

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

51 
* generated from the name of the argument theory. 

52 
**) 

3191  53 

54 

55 
(* 

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

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

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

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

60 
**) 

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

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

64 
in 

65 
fun make_definition parent s tm = 

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

67 
val {Name,Ty} = S.dest_var lhs 

68 
val lhs1 = S.mk_const{Name = Name, Ty = Ty} 

69 
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

70 
val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) 
3191  71 
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

72 
(K None) (K None) [] true ([dtm],propT) 
3191  73 
val new_thy = add_defs_i [(s,tm')] parent 
2112  74 
in 
3191  75 
(freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) 
76 
end; 

2112  77 
end; 
78 

79 
(* 

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

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

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

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

84 
**) 

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

86 
let fun canfind[] = [el] 

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

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

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

90 
else y::canfind rst 

91 
in canfind 

92 
end; 

93 

94 

95 
(* 

96 
* A collection of facts about datatypes 

97 
**) 

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

99 
val prod_record = 

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

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

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

103 
in ("*", 

104 
{constructors = [const "Pair"], 

105 
case_const = const "split", 

106 
case_rewrites = [split RS eq_reflection], 

107 
case_cong = #case_cong prod_case_thms, 

108 
nchotomy = #nchotomy prod_case_thms}) 

109 
end; 

110 

111 
(* 

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

113 
* is temporary, I hope! 

114 
**) 

115 
val match_info = fn thy => 

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

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

118 
 "nat" => Some({case_const = #case_const (#2 nat_record), 
2112  119 
constructors = #constructors (#2 nat_record)}) 
120 
 ty => case assoc(!datatypes,ty) 

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

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

123 
Some{case_const=case_const, constructors=constructors} 
2112  124 

125 
val induct_info = fn thy => 

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

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

128 
 "nat" => Some({nchotomy = #nchotomy (#2 nat_record), 
2112  129 
constructors = #constructors (#2 nat_record)}) 
130 
 ty => case assoc(!datatypes,ty) 

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

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

133 
Some{nchotomy=nchotomy, constructors=constructors} 
2112  134 

135 
val extract_info = fn thy => 

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

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

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

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

140 
case_rewrites = #case_rewrites(#2 prod_record)@ 

141 
#case_rewrites(#2 nat_record)@case_rewrites} 

142 
end; 

143 

144 
end; (* Thry *) 