TFL/tfl.ML
changeset 16505 c4b2e3cd84ab
parent 15574 b1d1b5bfc464
child 16853 33b886cbdc8f
     1.1 --- a/TFL/tfl.ML	Mon Jun 20 22:14:19 2005 +0200
     1.2 +++ b/TFL/tfl.ML	Mon Jun 20 22:14:20 2005 +0200
     1.3 @@ -101,13 +101,13 @@
     1.4          | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
     1.5          | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
     1.6          | part {constrs = c::crst, rows,     A} =
     1.7 -          let val (Name,Ty) = dest_Const c
     1.8 -              val L = binder_types Ty
     1.9 +          let val (c, T) = dest_Const c
    1.10 +              val L = binder_types T
    1.11                val (in_group, not_in_group) =
    1.12                 U.itlist (fn (row as (p::rst, rhs)) =>
    1.13                           fn (in_group,not_in_group) =>
    1.14                    let val (pc,args) = S.strip_comb p
    1.15 -                  in if (#1(dest_Const pc) = Name)
    1.16 +                  in if (#1(dest_Const pc) = c)
    1.17                       then ((args@rst, rhs)::in_group, not_in_group)
    1.18                       else (in_group, row::not_in_group)
    1.19                    end)      rows ([],[])
    1.20 @@ -157,13 +157,13 @@
    1.21  
    1.22  (*---------------------------------------------------------------------------
    1.23   * Goes through a list of rows and picks out the ones beginning with a
    1.24 - * pattern with constructor = Name.
    1.25 + * pattern with constructor = name.
    1.26   *---------------------------------------------------------------------------*)
    1.27 -fun mk_group Name rows =
    1.28 +fun mk_group name rows =
    1.29    U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
    1.30              fn (in_group,not_in_group) =>
    1.31                 let val (pc,args) = S.strip_comb p
    1.32 -               in if ((#1 (Term.dest_Const pc) = Name) handle TERM _ => false)
    1.33 +               in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
    1.34                    then (((prfx,args@rst), rhs)::in_group, not_in_group)
    1.35                    else (in_group, row::not_in_group) end)
    1.36        rows ([],[]);
    1.37 @@ -178,8 +178,7 @@
    1.38       fun part {constrs = [],      rows, A} = rev A
    1.39         | part {constrs = c::crst, rows, A} =
    1.40           let val (c',gvars) = fresh c
    1.41 -             val (Name,Ty) = dest_Const c'
    1.42 -             val (in_group, not_in_group) = mk_group Name rows
    1.43 +             val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
    1.44               val in_group' =
    1.45                   if (null in_group)  (* Constructor not given *)
    1.46                   then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
    1.47 @@ -290,7 +289,7 @@
    1.48  (* Repeated variable occurrences in a pattern are not allowed. *)
    1.49  fun FV_multiset tm =
    1.50     case (S.dest_term tm)
    1.51 -     of S.VAR{Name,Ty} => [Free(Name,Ty)]
    1.52 +     of S.VAR{Name = c, Ty = T} => [Free(c, T)]
    1.53        | S.CONST _ => []
    1.54        | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
    1.55        | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
    1.56 @@ -370,9 +369,9 @@
    1.57  
    1.58  
    1.59  (*For Isabelle, the lhs of a definition must be a constant.*)
    1.60 -fun mk_const_def sign (Name, Ty, rhs) =
    1.61 +fun mk_const_def sign (c, Ty, rhs) =
    1.62      Sign.infer_types (Sign.pp sign) sign (K NONE) (K NONE) [] false
    1.63 -               ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
    1.64 +               ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
    1.65      |> #1;
    1.66  
    1.67  (*Make all TVars available for instantiation by adding a ? to the front*)
    1.68 @@ -386,17 +385,17 @@
    1.69        val (fname,_) = dest_Free f
    1.70        val (wfrec,_) = S.strip_comb rhs
    1.71  in
    1.72 -fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) =
    1.73 - let val def_name = if Name<>fid then
    1.74 +fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
    1.75 + let val def_name = if x<>fid then
    1.76                          raise TFL_ERR "wfrec_definition0"
    1.77                                        ("Expected a definition of " ^
    1.78                                               quote fid ^ " but found one of " ^
    1.79 -                                      quote Name)
    1.80 -                    else Name ^ "_def"
    1.81 +                                      quote x)
    1.82 +                    else x ^ "_def"
    1.83       val wfrec_R_M =  map_term_types poly_tvars
    1.84                            (wfrec $ map_term_types poly_tvars R)
    1.85                        $ functional
    1.86 -     val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
    1.87 +     val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
    1.88       val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
    1.89   in (thy', def) end;
    1.90  end;
    1.91 @@ -449,7 +448,7 @@
    1.92                             given_pats
    1.93       val (case_rewrites,context_congs) = extraction_thms theory
    1.94       (*case_ss causes minimal simplification: bodies of case expressions are
    1.95 -       not simplified. Otherwise large examples (Red-Black trees) are too 
    1.96 +       not simplified. Otherwise large examples (Red-Black trees) are too
    1.97         slow.*)
    1.98       val case_ss = HOL_basic_ss addcongs
    1.99         DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
   1.100 @@ -485,15 +484,15 @@
   1.101       val g = list_comb(f,SV)
   1.102       val h = Free(fname,type_of g)
   1.103       val eqns1 = map (subst_free[(g,h)]) eqns
   1.104 -     val {functional as Abs(Name, Ty, _),  pats} = mk_functional thy eqns1
   1.105 +     val {functional as Abs(x, Ty, _),  pats} = mk_functional thy eqns1
   1.106       val given_pats = givens pats
   1.107 -     (* val f = Free(Name,Ty) *)
   1.108 +     (* val f = Free(x,Ty) *)
   1.109       val Type("fun", [f_dty, f_rty]) = Ty
   1.110 -     val dummy = if Name<>fid then
   1.111 +     val dummy = if x<>fid then
   1.112                          raise TFL_ERR "wfrec_eqns"
   1.113                                        ("Expected a definition of " ^
   1.114                                        quote fid ^ " but found one of " ^
   1.115 -                                      quote Name)
   1.116 +                                      quote x)
   1.117                   else ()
   1.118       val (case_rewrites,context_congs) = extraction_thms thy
   1.119       val tych = Thry.typecheck thy
   1.120 @@ -551,9 +550,9 @@
   1.121                             else ()
   1.122       val {lhs,rhs} = S.dest_eq proto_def'
   1.123       val (c,args) = S.strip_comb lhs
   1.124 -     val (Name,Ty) = dest_atom c
   1.125 +     val (name,Ty) = dest_atom c
   1.126       val defn = mk_const_def (Theory.sign_of thy)
   1.127 -                 (Name, Ty, S.list_mk_abs (args,rhs))
   1.128 +                 (name, Ty, S.list_mk_abs (args,rhs))
   1.129       val (theory, [def0]) =
   1.130         thy
   1.131         |> PureThy.add_defs_i false
   1.132 @@ -580,7 +579,7 @@
   1.133       val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
   1.134       val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
   1.135                         theory Hilbert_Choice*)
   1.136 -         thm "Hilbert_Choice.tfl_some" 
   1.137 +         thm "Hilbert_Choice.tfl_some"
   1.138           handle ERROR => error
   1.139      "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
   1.140       val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th