2112

1 
structure Thry : Thry_sig (* LThry_sig *) =


2 
struct


3 


4 
structure USyntax = USyntax;


5 
type Type = USyntax.Type


6 
type Preterm = USyntax.Preterm


7 
type Term = USyntax.Term


8 
type Thm = Thm.thm


9 
type Thry = theory;


10 


11 
open Mask;


12 
structure S = USyntax;


13 


14 


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


16 


17 
(*


18 
* Matching


19 
**)


20 


21 
local open Utils


22 
infix 3 >


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


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


25 
in


26 
fun match_term thry pat ob =


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


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


29 
in (map tmbind tm_theta, map tybind ty_theta)


30 
end


31 


32 
fun match_type thry pat ob =


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


34 
end;


35 


36 


37 
(*


38 
* Typing


39 
**)


40 


41 
fun typecheck thry = cterm_of (sign_of thry);


42 


43 


44 


45 
(*


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


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


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


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


50 
* generated from the name of the argument theory.


51 
**)

3191

52 


53 


54 
(*


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


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


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


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


59 
**)

2112

60 
local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))


61 
val Const(eeq_name, ty) = eeq


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


63 
in


64 
fun make_definition parent s tm =


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


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


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


68 
val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty > Ty > prop}


69 
val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *)

3191

70 
val (_, tm', _) = Sign.infer_types (sign_of parent)


71 
(K None) (K None) [] true ([dtm],propT)


72 
val new_thy = add_defs_i [(s,tm')] parent

2112

73 
in

3191

74 
(freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)


75 
end;

2112

76 
end;


77 


78 
(*


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


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


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


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


83 
**)


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


85 
let fun canfind[] = [el]


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


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


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


89 
else y::canfind rst


90 
in canfind


91 
end;


92 


93 


94 
(*


95 
* A collection of facts about datatypes


96 
**)


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


98 
val prod_record =


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


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


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


102 
in ("*",


103 
{constructors = [const "Pair"],


104 
case_const = const "split",


105 
case_rewrites = [split RS eq_reflection],


106 
case_cong = #case_cong prod_case_thms,


107 
nchotomy = #nchotomy prod_case_thms})


108 
end;


109 


110 
(*


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


112 
* is temporary, I hope!


113 
**)


114 
val match_info = fn thy =>


115 
fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),


116 
constructors = #constructors (#2 prod_record)})


117 
 "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),


118 
constructors = #constructors (#2 nat_record)})


119 
 ty => case assoc(!datatypes,ty)


120 
of None => Utils.NONE


121 
 Some{case_const,constructors, ...} =>


122 
Utils.SOME{case_const=case_const, constructors=constructors}


123 


124 
val induct_info = fn thy =>


125 
fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),


126 
constructors = #constructors (#2 prod_record)})


127 
 "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),


128 
constructors = #constructors (#2 nat_record)})


129 
 ty => case assoc(!datatypes,ty)


130 
of None => Utils.NONE


131 
 Some{nchotomy,constructors, ...} =>


132 
Utils.SOME{nchotomy=nchotomy, constructors=constructors}


133 


134 
val extract_info = fn thy =>


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


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


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


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


139 
case_rewrites = #case_rewrites(#2 prod_record)@


140 
#case_rewrites(#2 nat_record)@case_rewrites}


141 
end;


142 


143 


144 
end; (* Thry *)
