Now checks the name of the function being defined;
authorpaulson
Mon May 26 12:29:55 1997 +0200 (1997-05-26)
changeset 33330bbf06e86c06
parent 3332 3921ebbd9cf0
child 3334 ec558598ee1d
Now checks the name of the function being defined;
More de-HOL-ification
TFL/tfl.sig
TFL/tfl.sml
     1.1 --- a/TFL/tfl.sig	Mon May 26 12:29:10 1997 +0200
     1.2 +++ b/TFL/tfl.sig	Mon May 26 12:29:55 1997 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4                         -> {functional:term,
     1.5                             pats: pattern list}
     1.6  
     1.7 -   val wfrec_definition0 : theory -> term -> term -> thm * theory
     1.8 +   val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
     1.9  
    1.10     val post_definition : theory * (thm * pattern list)
    1.11                                -> {theory : theory,
     2.1 --- a/TFL/tfl.sml	Mon May 26 12:29:10 1997 +0200
     2.2 +++ b/TFL/tfl.sml	Mon May 26 12:29:55 1997 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4   * function contains embedded refs!
     2.5   *---------------------------------------------------------------------------*)
     2.6  fun gvvariant vlist =
     2.7 -  let val slist = ref (map (#Name o S.dest_var) vlist)
     2.8 +  let val slist = ref (map (#1 o dest_Free) vlist)
     2.9        val vname = ref "u"
    2.10        fun new() = 
    2.11           if !vname mem_string (!slist)
    2.12 @@ -213,7 +213,7 @@
    2.13   val divide = partition fresh_var ty_match
    2.14   fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
    2.15     | expand constructors ty (row as ((prefix, p::rst), rhs)) = 
    2.16 -       if (S.is_var p) 
    2.17 +       if (is_Free p) 
    2.18         then let val fresh = fresh_constr ty_match ty fresh_var
    2.19                  fun expnd (c,gvs) = 
    2.20                    let val capp = list_comb(c,gvs)
    2.21 @@ -234,7 +234,7 @@
    2.22       let val (pat_rectangle,rights) = ListPair.unzip rows
    2.23           val col0 = map(hd o #2) pat_rectangle
    2.24       in 
    2.25 -     if (forall S.is_var col0) 
    2.26 +     if (forall is_Free col0) 
    2.27       then let val rights' = map (fn(v,e) => psubst[v|->u] e)
    2.28                                  (ListPair.zip (col0, rights))
    2.29                val pat_rectangle' = map v_to_prefix pat_rectangle
    2.30 @@ -285,11 +285,11 @@
    2.31  fun no_repeat_vars thy pat =
    2.32   let fun check [] = true
    2.33         | check (v::rst) =
    2.34 -         if (U.mem S.aconv v rst) 
    2.35 -         then raise TFL_ERR{func = "no_repeat_vars",
    2.36 -             mesg = U.concat(U.quote(#Name(S.dest_var v)))
    2.37 -                     (U.concat" occurs repeatedly in the pattern "
    2.38 -                         (U.quote(S.Term_to_string (Thry.typecheck thy pat))))}
    2.39 +         if mem_term (v,rst) then
    2.40 +	    raise TFL_ERR{func = "no_repeat_vars",
    2.41 +			  mesg = quote(#1(dest_Free v)) ^
    2.42 +			  " occurs repeatedly in the pattern " ^
    2.43 +			  quote (string_of_cterm (Thry.typecheck thy pat))}
    2.44           else check rst
    2.45   in check (FV_multiset pat)
    2.46   end;
    2.47 @@ -308,7 +308,7 @@
    2.48                           clauses)
    2.49       val (funcs,pats) = ListPair.unzip(map (paired2 o S.dest_comb) L)
    2.50       val f = single (U.mk_set (S.aconv) funcs)
    2.51 -     val fvar = if (S.is_var f) then f else S.mk_var(S.dest_const f)
    2.52 +     val fvar = if (is_Free f) then f else S.mk_var(S.dest_const f)
    2.53       val dummy = map (no_repeat_vars thy) pats
    2.54       val rows = ListPair.zip (map (fn x => ([],[x])) pats,
    2.55                                map GIVEN (enumerate R))
    2.56 @@ -349,17 +349,29 @@
    2.57  local val f_eq_wfrec_R_M = 
    2.58             #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
    2.59        val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
    2.60 -      val fname = #Name(S.dest_var f)
    2.61 +      val (fname,_) = dest_Free f
    2.62        val (wfrec,_) = S.strip_comb rhs
    2.63  in
    2.64 -fun wfrec_definition0 thy R functional =
    2.65 +fun wfrec_definition0 thy fid R functional =
    2.66   let val {Bvar,...} = S.dest_abs functional
    2.67 -     val {Name, Ty} = S.dest_var Bvar  
    2.68 -     val def_name = U.concat Name "_def"
    2.69 +     val (Name, Ty) = dest_Free Bvar  
    2.70 +     val def_name = if Name<>fid then 
    2.71 +			raise TFL_ERR{func = "wfrec_definition0",
    2.72 +				      mesg = "Expected a definition of " ^ 
    2.73 +					     quote fid ^ " but found one of " ^
    2.74 +				      quote Name}
    2.75 +		    else Name ^ "_def"
    2.76       val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty})
    2.77       val wfrec' = S.inst ty_theta wfrec
    2.78       val wfrec_R_M' = list_comb(wfrec',[R,functional])
    2.79       val def_term = HOLogic.mk_eq(Bvar, wfrec_R_M')
    2.80 +(****************????????????????
    2.81 +     val wfrec_R_M = wfrec $ R $ functional
    2.82 +     val (_, def_term, _) = 
    2.83 +	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
    2.84 +	           ([HOLogic.mk_eq(Bvar, wfrec_R_M)], HOLogic.boolT)
    2.85 +		    
    2.86 +****************)
    2.87    in 
    2.88    Thry.make_definition thy def_name def_term
    2.89    end
    2.90 @@ -445,7 +457,7 @@
    2.91       val given_pats = givens pats
    2.92       val {Bvar = f, Body} = S.dest_abs functional
    2.93       val {Bvar = x, ...} = S.dest_abs Body
    2.94 -     val {Name, Ty = Type("fun", [f_dty, f_rty])} = S.dest_var f
    2.95 +     val (Name, Type("fun", [f_dty, f_rty])) = dest_Free f
    2.96       val (case_rewrites,context_congs) = extraction_thms thy
    2.97       val tych = Thry.typecheck thy
    2.98       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
    2.99 @@ -478,13 +490,13 @@
   2.100   let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
   2.101       val R1 = S.rand WFR
   2.102       val f = S.lhs proto_def
   2.103 -     val {Name,...} = S.dest_var f
   2.104 +     val (Name,_) = dest_Free f
   2.105       val (extractants,TCl) = ListPair.unzip extracta
   2.106       val TCs = foldr (gen_union (op aconv)) (TCl, [])
   2.107       val full_rqt = WFR::TCs
   2.108       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   2.109       val R'abs = S.rand R'
   2.110 -     val (def,theory) = Thry.make_definition thy (U.concat Name "_def") 
   2.111 +     val (def,theory) = Thry.make_definition thy (Name ^ "_def") 
   2.112                                                   (S.subst[R1 |-> R'] proto_def)
   2.113       val fconst = #lhs(S.dest_eq(concl def)) 
   2.114       val tych = Thry.typecheck theory
   2.115 @@ -569,7 +581,7 @@
   2.116           val col0 = map hd pat_rectangle
   2.117           val pat_rectangle' = map tl pat_rectangle
   2.118       in 
   2.119 -     if (forall S.is_var col0) (* column 0 is all variables *)
   2.120 +     if (forall is_Free col0) (* column 0 is all variables *)
   2.121       then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
   2.122                                  (ListPair.zip (rights, col0))
   2.123            in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}