HOL/Tools/fundef_package: Cleanup
authorkrauss
Mon Jun 05 19:54:12 2006 +0200 (2006-06-05)
changeset 19773ebc3b67fbd2c
parent 19772 45897b49fdd2
child 19774 5fe7731d0836
HOL/Tools/fundef_package: Cleanup
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 19:09:40 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 19:54:12 2006 +0200
     1.3 @@ -9,12 +9,8 @@
     1.4  
     1.5  signature FUNDEF_PREP =
     1.6  sig
     1.7 -    val prepare_fundef_curried : thm list -> term list -> theory
     1.8 -				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
     1.9 -
    1.10 -    val prepare_fundef_new : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
    1.11 -			          -> FundefCommon.prep_result * theory
    1.12 -
    1.13 +    val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
    1.14 +			 -> FundefCommon.prep_result * theory
    1.15  
    1.16  end
    1.17  
    1.18 @@ -302,25 +298,7 @@
    1.19   * Defines the function, the graph and the termination relation, synthesizes completeness
    1.20   * and comatibility conditions and returns everything.
    1.21   *)
    1.22 -fun prepare_fundef congs eqs defname thy =
    1.23 -    let
    1.24 -	val (names, thy) = setup_context (analyze_eqs eqs) defname congs thy
    1.25 -	val Names {G, R, glrs, trees, ...} = names
    1.26 -
    1.27 -	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
    1.28 -
    1.29 -	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
    1.30 -	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
    1.31 -
    1.32 -	val n = length glrs
    1.33 -	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
    1.34 -    in
    1.35 -	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
    1.36 -	 thy) 
    1.37 -    end
    1.38 -
    1.39 -
    1.40 -fun prepare_fundef_new thy congs defname f glrs used =
    1.41 +fun prepare_fundef thy congs defname f glrs used =
    1.42      let
    1.43  	val (names, thy) = setup_context (f, glrs, used) defname congs thy
    1.44  	val Names {G, R, glrs, trees, ...} = names
    1.45 @@ -340,49 +318,4 @@
    1.46  
    1.47  
    1.48  
    1.49 -
    1.50 -
    1.51 -
    1.52 -
    1.53 -fun prepare_fundef_curried congs eqs thy =
    1.54 -    let
    1.55 -	val lhs1 = hd eqs
    1.56 -		   |> dest_implies_list |> snd
    1.57 -		   |> HOLogic.dest_Trueprop
    1.58 -		   |> HOLogic.dest_eq |> fst
    1.59 -
    1.60 -	val (f, args) = strip_comb lhs1
    1.61 -	val Const(fname, fT) = f
    1.62 -	val fxname = Sign.extern_const thy fname
    1.63 -    in
    1.64 -	if (length args < 2)
    1.65 -	then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
    1.66 -	else
    1.67 -	    let
    1.68 -		val (caTs, uaTs) = chop (length args) (binder_types fT)
    1.69 -		val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
    1.70 -		val gxname = fxname ^ "_tupled"
    1.71 -			     
    1.72 -    		val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
    1.73 -		val gc = Const (Sign.intern_const thy gxname, newtype)
    1.74 -			 
    1.75 -		val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
    1.76 -				(1 upto (length caTs)) caTs
    1.77 -
    1.78 -		val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
    1.79 -			       
    1.80 -		val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
    1.81 -					   gc $ foldr1 HOLogic.mk_prod vars)
    1.82 -			  
    1.83 -		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
    1.84 -				      
    1.85 -		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
    1.86 -		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
    1.87 -	    in
    1.88 -		(SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy)
    1.89 -	    end
    1.90 -    end
    1.91 -
    1.92 -
    1.93 -
    1.94  end
    1.95 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 19:09:40 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 19:54:12 2006 +0200
     2.3 @@ -12,9 +12,6 @@
     2.4  
     2.5      val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result 
     2.6  			   -> thm -> thm list -> FundefCommon.fundef_result
     2.7 -
     2.8 -    val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result 
     2.9 -				   -> thm -> thm list -> FundefCommon.fundef_result
    2.10  end
    2.11  
    2.12  
    2.13 @@ -541,39 +538,6 @@
    2.14      end
    2.15  
    2.16  
    2.17 -fun curry_induct_rule thy argTs induct =
    2.18 -    let
    2.19 -	val vnums = (1 upto (length argTs))
    2.20 -	val avars = map2 (fn T => fn i => Var (("a",i), T)) argTs vnums
    2.21 -	val atup = foldr1 HOLogic.mk_prod avars
    2.22 -	val Q = Var (("P",1),argTs ---> HOLogic.boolT)
    2.23 -	val P = tupled_lambda atup (list_comb (Q, avars))
    2.24 -    in
    2.25 -	induct |> freezeT
    2.26 -	       |> instantiate' [] [SOME (cterm_of thy atup), SOME (cterm_of thy P)]
    2.27 -	       |> zero_var_indexes
    2.28 -	       |> full_simplify (HOL_basic_ss addsimps [split_apply])
    2.29 -	       |> varifyT
    2.30 -    end
    2.31 -
    2.32 -
    2.33 -
    2.34 -fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
    2.35 -    mk_partial_rules thy congs data complete_thm compat_thms 
    2.36 -  | mk_partial_rules_curried thy congs (SOME (Curry {curry_ss, argTs})) data complete_thm compat_thms =
    2.37 -    let
    2.38 -	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
    2.39 -	    mk_partial_rules thy congs data complete_thm compat_thms 
    2.40 -	val cpsimps = map (simplify curry_ss) psimps
    2.41 -	val cpinduct = full_simplify curry_ss simple_pinduct
    2.42 -				     |> curry_induct_rule thy argTs
    2.43 -	val cdom_intros = map (full_simplify curry_ss) dom_intros
    2.44 -	val ctotal_intro = full_simplify curry_ss total_intro
    2.45 -    in
    2.46 -	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
    2.47 -	 psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
    2.48 -    end
    2.49 -
    2.50  end
    2.51  
    2.52  
     3.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Jun 05 19:09:40 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jun 05 19:54:12 2006 +0200
     3.3 @@ -129,7 +129,7 @@
     3.4  	val global_glrs = flat qglrss
     3.5  	val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs []
     3.6      in
     3.7 -	(mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used)
     3.8 +	(mutual, name, FundefPrep.prepare_fundef thy congs name (Const sum_const) global_glrs used)
     3.9      end
    3.10  
    3.11