TFL/thry.sml
changeset 2112 3902e9af752f
child 3191 14bd6e5985f1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/thry.sml	Fri Oct 18 12:41:04 1996 +0200
     1.3 @@ -0,0 +1,139 @@
     1.4 +structure Thry : Thry_sig (* LThry_sig *) = 
     1.5 +struct
     1.6 +
     1.7 +structure USyntax  = USyntax;
     1.8 +type Type = USyntax.Type
     1.9 +type Preterm = USyntax.Preterm
    1.10 +type Term = USyntax.Term
    1.11 +type Thm = Thm.thm
    1.12 +type Thry = theory;
    1.13 +
    1.14 +open Mask;
    1.15 +structure S = USyntax;
    1.16 +
    1.17 +
    1.18 +fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    1.19 +
    1.20 +(*---------------------------------------------------------------------------
    1.21 + *    Matching 
    1.22 + *---------------------------------------------------------------------------*)
    1.23 +
    1.24 +local open Utils
    1.25 +      infix 3 |->
    1.26 +      fun tybind (x,y) = TVar (x,["term"])  |-> y
    1.27 +      fun tmbind (x,y) = Var  (x,type_of y) |-> y
    1.28 +in
    1.29 + fun match_term thry pat ob = 
    1.30 +    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
    1.31 +        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    1.32 +    in (map tmbind tm_theta, map tybind ty_theta)
    1.33 +    end
    1.34 +
    1.35 + fun match_type thry pat ob = 
    1.36 +    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
    1.37 +end;
    1.38 +
    1.39 +
    1.40 +(*---------------------------------------------------------------------------
    1.41 + * Typing 
    1.42 + *---------------------------------------------------------------------------*)
    1.43 +
    1.44 +fun typecheck thry = cterm_of (sign_of thry);
    1.45 +
    1.46 +
    1.47 +
    1.48 +(*----------------------------------------------------------------------------
    1.49 + * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
    1.50 + * entrypoint is specialized for interactive use, since it closes the theory
    1.51 + * after making the definition. This allows later interactive definitions to
    1.52 + * refer to previous ones. The name for the new theory is automatically 
    1.53 + * generated from the name of the argument theory.
    1.54 + *---------------------------------------------------------------------------*)
    1.55 +local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
    1.56 +      val Const(eeq_name, ty) = eeq
    1.57 +      val prop = #2 (S.strip_type ty)
    1.58 +in
    1.59 +fun make_definition parent s tm = 
    1.60 +   let val {lhs,rhs} = S.dest_eq tm
    1.61 +       val {Name,Ty} = S.dest_var lhs
    1.62 +       val lhs1 = S.mk_const{Name = Name, Ty = Ty}
    1.63 +       val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
    1.64 +       val dtm = S.list_mk_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
    1.65 +       val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent
    1.66 +       val thry2 = add_defs_i [(s,dtm)] thry1
    1.67 +       val parent_names = map ! (stamps_of_thy parent)
    1.68 +       val newthy_name = variant parent_names (hd parent_names)
    1.69 +       val new_thy = add_thyname newthy_name thry2
    1.70 +   in 
    1.71 +   ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy)
    1.72 +   end
    1.73 +end;
    1.74 +
    1.75 +
    1.76 +(*---------------------------------------------------------------------------
    1.77 + * Utility routine. Insert into list ordered by the key (a string). If two 
    1.78 + * keys are equal, the new element replaces the old. A more efficient option 
    1.79 + * for the future is needed. In fact, having the list of datatype facts be 
    1.80 + * ordered is useless, since the lookup should never fail!
    1.81 + *---------------------------------------------------------------------------*)
    1.82 +fun insert (el as (x:string, _)) = 
    1.83 + let fun canfind[] = [el] 
    1.84 +       | canfind(alist as ((y as (k,_))::rst)) = 
    1.85 +           if (x<k) then el::alist
    1.86 +           else if (x=k) then el::rst
    1.87 +           else y::canfind rst 
    1.88 + in canfind
    1.89 + end;
    1.90 +
    1.91 +
    1.92 +(*---------------------------------------------------------------------------
    1.93 + *     A collection of facts about datatypes
    1.94 + *---------------------------------------------------------------------------*)
    1.95 +val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
    1.96 +val prod_record =
    1.97 +    let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
    1.98 +                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
    1.99 +         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
   1.100 +     in ("*", 
   1.101 +         {constructors = [const "Pair"],
   1.102 +            case_const = const "split",
   1.103 +         case_rewrites = [split RS eq_reflection],
   1.104 +             case_cong = #case_cong prod_case_thms,
   1.105 +              nchotomy = #nchotomy prod_case_thms}) 
   1.106 +     end;
   1.107 +
   1.108 +(*---------------------------------------------------------------------------
   1.109 + * Hacks to make interactive mode work. Referring to "datatypes" directly
   1.110 + * is temporary, I hope!
   1.111 + *---------------------------------------------------------------------------*)
   1.112 +val match_info = fn thy =>
   1.113 +    fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),
   1.114 +                     constructors = #constructors (#2 prod_record)})
   1.115 +     | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),
   1.116 +                       constructors = #constructors (#2 nat_record)})
   1.117 +     | ty => case assoc(!datatypes,ty)
   1.118 +               of None => Utils.NONE
   1.119 +                | Some{case_const,constructors, ...} =>
   1.120 +                   Utils.SOME{case_const=case_const, constructors=constructors}
   1.121 +
   1.122 +val induct_info = fn thy =>
   1.123 +    fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),
   1.124 +                     constructors = #constructors (#2 prod_record)})
   1.125 +     | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),
   1.126 +                       constructors = #constructors (#2 nat_record)})
   1.127 +     | ty => case assoc(!datatypes,ty)
   1.128 +               of None => Utils.NONE
   1.129 +                | Some{nchotomy,constructors, ...} =>
   1.130 +                  Utils.SOME{nchotomy=nchotomy, constructors=constructors}
   1.131 +
   1.132 +val extract_info = fn thy => 
   1.133 + let val case_congs = map (#case_cong o #2) (!datatypes)
   1.134 +         val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
   1.135 + in {case_congs = #case_cong (#2 prod_record)::
   1.136 +                  #case_cong (#2 nat_record)::case_congs,
   1.137 +     case_rewrites = #case_rewrites(#2 prod_record)@
   1.138 +                     #case_rewrites(#2 nat_record)@case_rewrites}
   1.139 + end;
   1.140 +
   1.141 +
   1.142 +end; (* Thry *)