paulson@3302: (*  Title:      TFL/thry
paulson@3302:     ID:         $Id$
paulson@3302:     Author:     Konrad Slind, Cambridge University Computer Laboratory
paulson@3302:     Copyright   1997  University of Cambridge
paulson@3302: *)
paulson@3302: 
paulson@2112: structure Thry : Thry_sig (* LThry_sig *) = 
paulson@2112: struct
paulson@2112: 
paulson@2112: structure USyntax  = USyntax;
paulson@2112: structure S = USyntax;
paulson@2112: 
paulson@2112: fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
paulson@2112: 
paulson@2112: (*---------------------------------------------------------------------------
paulson@2112:  *    Matching 
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@2112: 
paulson@3353: local fun tybind (x,y) = (TVar (x,["term"]) , y)
paulson@3353:       fun tmbind (x,y) = (Var  (x,type_of y), y)
paulson@2112: in
paulson@2112:  fun match_term thry pat ob = 
paulson@2112:     let val tsig = #tsig(Sign.rep_sg(sign_of thry))
paulson@2112:         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
paulson@2112:     in (map tmbind tm_theta, map tybind ty_theta)
paulson@2112:     end
paulson@2112: 
paulson@2112:  fun match_type thry pat ob = 
paulson@2112:     map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
paulson@2112: end;
paulson@2112: 
paulson@2112: 
paulson@2112: (*---------------------------------------------------------------------------
paulson@2112:  * Typing 
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@2112: 
paulson@2112: fun typecheck thry = cterm_of (sign_of thry);
paulson@2112: 
paulson@2112: 
paulson@2112: 
paulson@2112: (*----------------------------------------------------------------------------
paulson@2112:  * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
paulson@2112:  * entrypoint is specialized for interactive use, since it closes the theory
paulson@2112:  * after making the definition. This allows later interactive definitions to
paulson@2112:  * refer to previous ones. The name for the new theory is automatically 
paulson@2112:  * generated from the name of the argument theory.
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@3191: 
paulson@3191: 
paulson@3191: (*---------------------------------------------------------------------------
paulson@3191:  * TFL attempts to make definitions where the lhs is a variable. Isabelle
paulson@3191:  * wants it to be a constant, so here we map it to a constant. Moreover, the
paulson@3191:  * theory should already have the constant, so we refrain from adding the
paulson@3191:  * constant to the theory. We just add the axiom and return the theory.
paulson@3191:  *---------------------------------------------------------------------------*)
paulson@2112: local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
paulson@2112:       val Const(eeq_name, ty) = eeq
paulson@2112:       val prop = #2 (S.strip_type ty)
paulson@2112: in
paulson@2112: fun make_definition parent s tm = 
paulson@2112:    let val {lhs,rhs} = S.dest_eq tm
paulson@3332:        val (Name,Ty) = dest_Free lhs
paulson@2112:        val lhs1 = S.mk_const{Name = Name, Ty = Ty}
paulson@2112:        val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
paulson@3245:        val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
paulson@3191:        val (_, tm', _) = Sign.infer_types (sign_of parent)
paulson@3245:                      (K None) (K None) [] true ([dtm],propT)
paulson@3191:        val new_thy = add_defs_i [(s,tm')] parent
paulson@2112:    in 
paulson@3191:    (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
paulson@3191:    end;
paulson@2112: end;
paulson@2112: 
paulson@2112: (*---------------------------------------------------------------------------
paulson@2112:  * Utility routine. Insert into list ordered by the key (a string). If two 
paulson@2112:  * keys are equal, the new element replaces the old. A more efficient option 
paulson@2112:  * for the future is needed. In fact, having the list of datatype facts be 
paulson@2112:  * ordered is useless, since the lookup should never fail!
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@2112: fun insert (el as (x:string, _)) = 
paulson@2112:  let fun canfind[] = [el] 
paulson@2112:        | canfind(alist as ((y as (k,_))::rst)) = 
paulson@2112:            if (x<k) then el::alist
paulson@2112:            else if (x=k) then el::rst
paulson@2112:            else y::canfind rst 
paulson@2112:  in canfind
paulson@2112:  end;
paulson@2112: 
paulson@2112: 
paulson@2112: (*---------------------------------------------------------------------------
paulson@2112:  *     A collection of facts about datatypes
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@2112: val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
paulson@2112: val prod_record =
paulson@2112:     let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
paulson@2112:                                  (fn s => res_inst_tac [("p",s)] PairE_lemma)
paulson@2112:          fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
paulson@2112:      in ("*", 
paulson@2112:          {constructors = [const "Pair"],
paulson@2112:             case_const = const "split",
paulson@2112:          case_rewrites = [split RS eq_reflection],
paulson@2112:              case_cong = #case_cong prod_case_thms,
paulson@2112:               nchotomy = #nchotomy prod_case_thms}) 
paulson@2112:      end;
paulson@2112: 
paulson@2112: (*---------------------------------------------------------------------------
paulson@2112:  * Hacks to make interactive mode work. Referring to "datatypes" directly
paulson@2112:  * is temporary, I hope!
paulson@2112:  *---------------------------------------------------------------------------*)
paulson@2112: val match_info = fn thy =>
paulson@3245:     fn "*" => Some({case_const = #case_const (#2 prod_record),
paulson@2112:                      constructors = #constructors (#2 prod_record)})
paulson@3245:      | "nat" => Some({case_const = #case_const (#2 nat_record),
paulson@2112:                        constructors = #constructors (#2 nat_record)})
paulson@2112:      | ty => case assoc(!datatypes,ty)
paulson@3245:                of None => None
paulson@2112:                 | Some{case_const,constructors, ...} =>
paulson@3245:                    Some{case_const=case_const, constructors=constructors}
paulson@2112: 
paulson@2112: val induct_info = fn thy =>
paulson@3245:     fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
paulson@2112:                      constructors = #constructors (#2 prod_record)})
paulson@3245:      | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
paulson@2112:                        constructors = #constructors (#2 nat_record)})
paulson@2112:      | ty => case assoc(!datatypes,ty)
paulson@3245:                of None => None
paulson@2112:                 | Some{nchotomy,constructors, ...} =>
paulson@3245:                   Some{nchotomy=nchotomy, constructors=constructors}
paulson@2112: 
paulson@2112: val extract_info = fn thy => 
paulson@2112:  let val case_congs = map (#case_cong o #2) (!datatypes)
paulson@2112:          val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
paulson@2112:  in {case_congs = #case_cong (#2 prod_record)::
paulson@2112:                   #case_cong (#2 nat_record)::case_congs,
paulson@2112:      case_rewrites = #case_rewrites(#2 prod_record)@
paulson@2112:                      #case_rewrites(#2 nat_record)@case_rewrites}
paulson@2112:  end;
paulson@2112: 
paulson@2112: end; (* Thry *)