TFL/thry.sml
author paulson
Thu May 15 12:29:59 1997 +0200 (1997-05-15)
changeset 3191 14bd6e5985f1
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
TFL now integrated with HOL (more work needed)
     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  *---------------------------------------------------------------------------*)
    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  *---------------------------------------------------------------------------*)
    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 "==" *)
    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
    73    in 
    74    (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
    75    end;
    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 *)