# HG changeset patch # User berghofe # Date 899232101 -7200 # Node ID 84b00be693b4b42284c33f13ba48af56781ff2ba # Parent 4436c62efcebda1b68a14de71a26586b5d3781af Moved most of the Prod_Syntax - stuff to HOLogic. diff -r 4436c62efceb -r 84b00be693b4 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Tue Jun 30 20:40:29 1998 +0200 +++ b/src/HOL/Prod.ML Tue Jun 30 20:41:41 1998 +0200 @@ -428,59 +428,39 @@ Addsimps [unit_abs_eta_conv]; -structure Prod_Syntax = (* FIXME eliminate (use HOLogic instead!) *) -struct - -val unitT = Type("unit",[]); - -fun mk_prod (T1,T2) = Type("*", [T1,T2]); +(*Attempts to remove occurrences of split, and pair-valued parameters*) +val remove_split = rewrite_rule [split RS eq_reflection] o + rule_by_tactic (TRYALL split_all_tac); -(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*) -fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2 - | factors T = [T]; - -(*Make a correctly typed ordered pair*) -fun mk_Pair (t1,t2) = - let val T1 = fastype_of t1 - and T2 = fastype_of t2 - in Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2 end; - -fun split_const(Ta,Tb,Tc) = - Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc); +local (*In ap_split S T u, term u expects separate arguments for the factors of S, with result type T. The call creates a new term expecting one argument of type S.*) -fun ap_split (Type("*", [T1,T2])) T3 u = - split_const(T1,T2,T3) $ +fun ap_split (Type ("*", [T1, T2])) T3 u = + HOLogic.split_const (T1, T2, T3) $ Abs("v", T1, ap_split T2 T3 - ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ + ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ Bound 0)) | ap_split T T3 u = u; -(*Makes a nested tuple from a list, following the product type structure*) -fun mk_tuple (Type("*", [T1,T2])) tms = - mk_Pair (mk_tuple T1 tms, - mk_tuple T2 (drop (length (factors T1), tms))) - | mk_tuple T (t::_) = t; - -(*Attempts to remove occurrences of split, and pair-valued parameters*) -val remove_split = rewrite_rule [split RS eq_reflection] o - rule_by_tactic (TRYALL split_all_tac); +(*Curries any Var of function type in the rule*) +fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = + let val T' = HOLogic.prodT_factors T1 ---> T2 + val newt = ap_split T1 T2 (Var (v, T')) + val cterm = Thm.cterm_of (#sign (rep_thm rl)) + in + instantiate ([], [(cterm t, cterm newt)]) rl + end + | split_rule_var' (t, rl) = rl; -(*Uncurries any Var of function type in the rule*) -fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) = - let val T' = factors T1 ---> T2 - val newt = ap_split T1 T2 (Var(v,T')) - val cterm = Thm.cterm_of (#sign(rep_thm rl)) - in - remove_split (instantiate ([], [(cterm t, cterm newt)]) rl) - end - | split_rule_var (t,rl) = rl; +in -(*Uncurries ALL function variables occurring in a rule's conclusion*) -fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl) +val split_rule_var = standard o remove_split o split_rule_var'; + +(*Curries ALL function variables occurring in a rule's conclusion*) +fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)) |> standard; end; diff -r 4436c62efceb -r 84b00be693b4 src/HOL/hologic.ML --- a/src/HOL/hologic.ML Tue Jun 30 20:40:29 1998 +0200 +++ b/src/HOL/hologic.ML Tue Jun 30 20:41:41 1998 +0200 @@ -47,6 +47,9 @@ val dest_prod: term -> term * term val mk_fst: term -> term val mk_snd: term -> term + val prodT_factors: typ -> typ list + val split_const: typ * typ * typ -> term + val mk_tuple: typ -> term list -> term end; @@ -182,5 +185,17 @@ Const ("snd", pT --> snd (dest_prodT pT)) $ p end; +(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) +fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2 + | prodT_factors T = [T]; + +fun split_const (Ta, Tb, Tc) = + Const ("split", [[Ta, Tb] ---> Tc, mk_prodT (Ta, Tb)] ---> Tc); + +(*Makes a nested tuple from a list, following the product type structure*) +fun mk_tuple (Type ("*", [T1, T2])) tms = + mk_prod (mk_tuple T1 tms, + mk_tuple T2 (drop (length (prodT_factors T1), tms))) + | mk_tuple T (t::_) = t; end;