src/HOL/Tools/function_package/fundef_prep.ML
changeset 19781 c62720b20e9a
parent 19773 ebc3b67fbd2c
child 19876 11d447d5d68c
     1.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 21:54:26 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jun 06 08:21:14 2006 +0200
     1.3 @@ -46,29 +46,6 @@
     1.4      end
     1.5  
     1.6  
     1.7 -fun analyze_eqs eqs =
     1.8 -    let
     1.9 -	fun dest_geq geq = 
    1.10 -	    let
    1.11 -		val qs = add_term_frees (geq, [])
    1.12 -	    in
    1.13 -		case dest_implies_list geq of
    1.14 -		    (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) => 
    1.15 -		    (f, (qs, gs, lhs, rhs))
    1.16 -		  | _ => raise ERROR "Not a guarded equation"
    1.17 -	    end
    1.18 -			       
    1.19 -	val (fs, glrs) = split_list (map dest_geq eqs)
    1.20 -			 
    1.21 -	val f = (hd fs) (* should be equal and a constant... check! *)
    1.22 -
    1.23 -	val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
    1.24 -		   (* Must check for recursive calls in guards and new vars in rhss *)
    1.25 -    in
    1.26 -	(f, glrs, used)
    1.27 -    end
    1.28 -
    1.29 -
    1.30  (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
    1.31  fun mk_primed_vars thy glrs =
    1.32      let
    1.33 @@ -162,8 +139,8 @@
    1.34  	val trees = map (build_tree thy f congs) glrs
    1.35  	val allused = fold FundefCtxTree.add_context_varnames trees used
    1.36  
    1.37 -	val Const (f_proper_name, fT) = f
    1.38 -	val fxname = Sign.extern_const thy f_proper_name
    1.39 +	val Const (f_fullname, fT) = f
    1.40 +	val fname = Sign.base_name f_fullname
    1.41  
    1.42  	val domT = domain_type fT 
    1.43  	val ranT = range_type fT
    1.44 @@ -188,15 +165,15 @@
    1.45  
    1.46  	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
    1.47  
    1.48 -	val G = Const (Sign.intern_const thy G_name, GT)
    1.49 -	val R = Const (Sign.intern_const thy R_name, RT)
    1.50 +	val G = Const (Sign.full_name thy G_name, GT)
    1.51 +	val R = Const (Sign.full_name thy R_name, RT)
    1.52  	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
    1.53  
    1.54  	val f_eq = Logic.mk_equals (f $ x, 
    1.55  				    Const ("The", (ranT --> boolT) --> ranT) $
    1.56  					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
    1.57  
    1.58 -	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
    1.59 +	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
    1.60      in
    1.61  	(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
    1.62      end
    1.63 @@ -262,7 +239,7 @@
    1.64  
    1.65  fun extract_conditions thy names trees congs =
    1.66      let
    1.67 -	val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
    1.68 +	val Names {f, R, glrs, glrs', ...} = names
    1.69  
    1.70  	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
    1.71  	val Gis = map2 (mk_GIntro thy names) glrs preRiss