# HG changeset patch
# User hoelzl
# Date 1262882615 -3600
# Node ID 1edf0f223c6ea5475ad02dddc2b4a84670547962
# Parent  c9c14c72d035bb4e17f176b27d0b97e3ad36bd7a
added syntax translation to automatically add finite typeclass to index type of cartesian product type

diff -r c9c14c72d035 -r 1edf0f223c6e src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Jan 06 13:07:30 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 07 17:43:35 2010 +0100
@@ -19,6 +19,26 @@
 
 notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
 
+(*
+  Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n needs more than one
+  type class write "cart 'b ('n::{finite, ...})"
+*)
+
+syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
+
+parse_translation {*
+let
+  fun cart t u = Syntax.const @{type_name cart} $ t $ u
+  fun finite_cart_tr [t, u as Free (x, _)] =
+        if Syntax.is_tid x
+        then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite}))
+        else cart t u
+    | finite_cart_tr [t, u] = cart t u
+in
+  [("_finite_cart", finite_cart_tr)]
+end
+*}
+
 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
   apply auto
   apply (rule ext)