adapted to qualified names;
authorwenzelm
Mon Oct 20 11:14:55 1997 +0200 (1997-10-20)
changeset 3945ae9c61d69888
parent 3944 8988ba66c62b
child 3946 34152864655c
adapted to qualified names;
src/HOL/TLA/Action.ML
src/HOL/TLA/Intensional.ML
src/HOL/TLA/ROOT.ML
src/HOL/TLA/hypsubst.ML
src/HOL/add_ind_def.ML
src/HOL/datatype.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/TLA/Action.ML	Mon Oct 20 11:14:16 1997 +0200
     1.2 +++ b/src/HOL/TLA/Action.ML	Mon Oct 20 11:14:55 1997 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  *)
     1.5  fun maybe_unlift th =
     1.6      (case concl_of th of
     1.7 -         Const("TrueInt",_) $ p 
     1.8 +         Const("Intensional.TrueInt",_) $ p 
     1.9             => (action_unlift th
    1.10                    handle _ => int_unlift th)
    1.11         | _ => th);
     2.1 --- a/src/HOL/TLA/Intensional.ML	Mon Oct 20 11:14:16 1997 +0200
     2.2 +++ b/src/HOL/TLA/Intensional.ML	Mon Oct 20 11:14:55 1997 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4  *)
     2.5  fun maybe_unlift th =
     2.6      (case concl_of th of
     2.7 -	 Const("TrueInt",_) $ p => int_unlift th
     2.8 +	 Const("Intensional.TrueInt",_) $ p => int_unlift th
     2.9         | _ => th);
    2.10  
    2.11  simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
     3.1 --- a/src/HOL/TLA/ROOT.ML	Mon Oct 20 11:14:16 1997 +0200
     3.2 +++ b/src/HOL/TLA/ROOT.ML	Mon Oct 20 11:14:55 1997 +0200
     3.3 @@ -12,6 +12,8 @@
     3.4  *)
     3.5  Syntax.ambiguity_level := 10000;
     3.6  
     3.7 +reset global_names;
     3.8 +
     3.9  use_thy "TLA";
    3.10  
    3.11  val TLA_build_completed = ();
     4.1 --- a/src/HOL/TLA/hypsubst.ML	Mon Oct 20 11:14:16 1997 +0200
     4.2 +++ b/src/HOL/TLA/hypsubst.ML	Mon Oct 20 11:14:55 1997 +0200
     4.3 @@ -88,7 +88,7 @@
     4.4     Is type ty the type of a state variable? Only then do we substitute
     4.5     in applications. This function either returns true or raises Match.
     4.6  *)
     4.7 -fun is_stvar (Type("fun", Type("state",[])::_)) = true;
     4.8 +fun is_stvar (Type("fun", Type("Stfun.state",[])::_)) = true;
     4.9  
    4.10  
    4.11  (*If novars then we forbid Vars in the equality.
     5.1 --- a/src/HOL/add_ind_def.ML	Mon Oct 20 11:14:16 1997 +0200
     5.2 +++ b/src/HOL/add_ind_def.ML	Mon Oct 20 11:14:55 1997 +0200
     5.3 @@ -68,8 +68,9 @@
     5.4      val rec_names = map (#1 o dest_Const) rec_hds
     5.5      and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
     5.6  
     5.7 -    val _ = assert_all Syntax.is_identifier rec_names
     5.8 -       (fn a => "Name of recursive set not an identifier: " ^ a);
     5.9 +    val rec_base_names = map Sign.base_name rec_names;
    5.10 +    val _ = assert_all Syntax.is_identifier rec_base_names
    5.11 +       (fn a => "Base name of recursive set not an identifier: " ^ a);
    5.12  
    5.13      local (*Checking the introduction rules*)
    5.14        val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
    5.15 @@ -136,7 +137,8 @@
    5.16      (*A key definition:
    5.17        If no mutual recursion then it equals the one recursive set.
    5.18        If mutual recursion then it differs from all the recursive sets. *)
    5.19 -    val big_rec_name = space_implode "_" rec_names;
    5.20 +    val big_rec_base_name = space_implode "_" rec_base_names;
    5.21 +    val big_rec_name = Sign.full_name sign big_rec_base_name;
    5.22  
    5.23      (*Big_rec... is the union of the mutually recursive sets*)
    5.24      val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
    5.25 @@ -160,86 +162,4 @@
    5.26    in  thy |> Theory.add_defs_i axpairs  end
    5.27  
    5.28  
    5.29 -(****************************************************************OMITTED
    5.30 -
    5.31 -(*Expects the recursive sets to have been defined already.
    5.32 -  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
    5.33 -fun add_constructs_def (rec_names, con_ty_lists) thy = 
    5.34 -* let
    5.35 -*   val _ = writeln"  Defining the constructor functions...";
    5.36 -*   val case_name = "f";                (*name for case variables*)
    5.37 -
    5.38 -*   (** Define the constructors **)
    5.39 -
    5.40 -*   (*The empty tuple is 0*)
    5.41 -*   fun mk_tuple [] = Const("0",iT)
    5.42 -*     | mk_tuple args = foldr1 mk_Pair args;
    5.43 -
    5.44 -*   fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
    5.45 -
    5.46 -*   val npart = length rec_names;       (*total # of mutually recursive parts*)
    5.47 -
    5.48 -*   (*Make constructor definition; kpart is # of this mutually recursive part*)
    5.49 -*   fun mk_con_defs (kpart, con_ty_list) = 
    5.50 -*     let val ncon = length con_ty_list    (*number of constructors*)
    5.51 -          fun mk_def (((id,T,syn), name, args, prems), kcon) =
    5.52 -                (*kcon is index of constructor*)
    5.53 -              mk_defpair (list_comb (Const(name,T), args),
    5.54 -                          mk_inject npart kpart
    5.55 -                          (mk_inject ncon kcon (mk_tuple args)))
    5.56 -*     in  ListPair.map mk_def (con_ty_list, (1 upto ncon))  end;
    5.57 -
    5.58 -*   (** Define the case operator **)
    5.59 -
    5.60 -*   (*Combine split terms using case; yields the case operator for one part*)
    5.61 -*   fun call_case case_list = 
    5.62 -*     let fun call_f (free,args) = 
    5.63 -              ap_split T free (map (#2 o dest_Free) args)
    5.64 -*     in  fold_bal (app sum_case) (map call_f case_list)  end;
    5.65 -
    5.66 -*   (** Generating function variables for the case definition
    5.67 -        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
    5.68 -
    5.69 -*   (*Treatment of a single constructor*)
    5.70 -*   fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
    5.71 -        if Syntax.is_identifier id
    5.72 -        then (opno,   
    5.73 -              (Free(case_name ^ "_" ^ id, T), args) :: cases)
    5.74 -        else (opno+1, 
    5.75 -              (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
    5.76 -              cases)
    5.77 -
    5.78 -*   (*Treatment of a list of constructors, for one part*)
    5.79 -*   fun add_case_list (con_ty_list, (opno,case_lists)) =
    5.80 -        let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
    5.81 -        in (opno', case_list :: case_lists) end;
    5.82 -
    5.83 -*   (*Treatment of all parts*)
    5.84 -*   val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
    5.85 -
    5.86 -*   val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
    5.87 -
    5.88 -*   val big_rec_name = space_implode "_" rec_names;
    5.89 -
    5.90 -*   val big_case_name = big_rec_name ^ "_case";
    5.91 -
    5.92 -*   (*The list of all the function variables*)
    5.93 -*   val big_case_args = flat (map (map #1) case_lists);
    5.94 -
    5.95 -*   val big_case_tm = 
    5.96 -        list_comb (Const(big_case_name, big_case_typ), big_case_args); 
    5.97 -
    5.98 -*   val big_case_def = mk_defpair  
    5.99 -        (big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); 
   5.100 -
   5.101 -*   (** Build the new theory **)
   5.102 -
   5.103 -*   val const_decs =
   5.104 -        (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
   5.105 -
   5.106 -*   val axpairs =
   5.107 -        big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
   5.108 -
   5.109 -*   in  thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs  end;
   5.110 -****************************************************************)
   5.111  end;
     6.1 --- a/src/HOL/datatype.ML	Mon Oct 20 11:14:16 1997 +0200
     6.2 +++ b/src/HOL/datatype.ML	Mon Oct 20 11:14:55 1997 +0200
     6.3 @@ -4,8 +4,6 @@
     6.4                  Konrad Slind
     6.5     Copyright 1995 TU Muenchen
     6.6  
     6.7 -TODO:
     6.8 -  - handle internal / external names
     6.9  *)
    6.10  
    6.11  (** Information about datatypes **)
    6.12 @@ -129,7 +127,7 @@
    6.13        | subst (funct $ body) = 
    6.14          let val (f,b) = strip_comb (funct$body)
    6.15          in 
    6.16 -          if is_Const f andalso fst(dest_Const f) = fname 
    6.17 +          if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname 
    6.18              then 
    6.19                let val (ls,rest) = (take(rpos,b), drop(rpos,b));
    6.20                  val (xk,rs) = (hd rest,tl rest)
    6.21 @@ -181,9 +179,9 @@
    6.22        raise RecError "more than one non-variable in pattern"
    6.23      else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
    6.24        raise RecError "repeated variable name in pattern" 
    6.25 -         else (fst(dest_Const name) handle TERM _ => 
    6.26 +         else (Sign.base_name (fst(dest_Const name)) handle TERM _ => 
    6.27                 raise RecError "function is not declared as constant in theory"
    6.28 -                 ,rpos,ls,fst( dest_Const c),cargs,rs,rhs)
    6.29 +                 ,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs)
    6.30    end; 
    6.31  
    6.32  (* check function specified for all constructors and sort function terms *)
    6.33 @@ -506,7 +504,7 @@
    6.34                           Logic.mk_equals (Const(fname,dummyT), rhs))
    6.35            val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
    6.36            val varT = Type.varifyT T;
    6.37 -          val ftyp = the (Sign.const_type sg fname);
    6.38 +          val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname));
    6.39          in Theory.add_defs_i [defpairT] thy end;
    6.40  
    6.41      in
    6.42 @@ -962,7 +960,10 @@
    6.43  in
    6.44  fun build_record (thy,(ty,cl),itac) =
    6.45   let val sign = sign_of thy
    6.46 -     fun const s = Const(s, the(Sign.const_type sign s))
    6.47 +     val intern_const = Sign.intern_const sign;
    6.48 +     fun const s =
    6.49 +       let val s' = intern_const s
    6.50 +       in Const(s', the (Sign.const_type sign s')) end
    6.51       val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
    6.52       val {nchotomy,case_cong} = case_thms sign case_rewrites itac
    6.53       val exhaustion = mk_exhaust nchotomy
     7.1 --- a/src/HOL/thy_syntax.ML	Mon Oct 20 11:14:16 1997 +0200
     7.2 +++ b/src/HOL/thy_syntax.ML	Mon Oct 20 11:14:55 1997 +0200
     7.3 @@ -143,7 +143,8 @@
     7.4      \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
     7.5      \end;\n\
     7.6      \val dummy = datatypes := Dtype.build_record (thy, " ^
     7.7 -      mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
     7.8 +      mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
     7.9 +        mk_list (map (fst o fst) cons)) ^
    7.10        ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
    7.11      \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
    7.12      \val dummy = AddIffs " ^ tname ^ ".inject;\n\