# HG changeset patch # User Cezary Kaliszyk # Date 1333563021 -7200 # Node ID 637074507956b5f3e08809e7cc122c7b4d881507 # Parent c7fc95e722ff55492b986e860cad234ee8558f91 HOL/Import more precise map types diff -r c7fc95e722ff -r 637074507956 src/HOL/Import/HOL_Light_Maps.thy --- a/src/HOL/Import/HOL_Light_Maps.thy Wed Apr 04 20:09:56 2012 +0200 +++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Apr 04 20:10:21 2012 +0200 @@ -93,9 +93,9 @@ "snd = (\p\'A \ 'B. SOME y\'B. \x\'A. p = (x, y))" by auto -(*lemma [import_const CURRY]: +lemma CURRY_DEF[import_const CURRY]: "curry = (\(f\'A \ 'B \ 'C) x y. f (x, y))" - using curry_def .*) + using curry_def . lemma [import_const ONE_ONE : Fun.inj]: "inj = (\(f\'A \ 'B). \x1 x2. f x1 = f x2 \ x1 = x2)" @@ -200,16 +200,16 @@ "\m n\nat. if n = id 0 then m div n = id 0 \ m mod n = m else m = m div n * n + m mod n \ m mod n < n" by simp -lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum +lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"] import_const_map INL : Sum_Type.Inl import_const_map INR : Sum_Type.Inr lemma sum_INDUCT: - "\P. (\a. P (Inl a)) \ (\a. P (Inr a)) \ (\x. P x)" + "\P. (\a :: 'A. P (Inl a)) \ (\a :: 'B. P (Inr a)) \ (\x. P x)" by (auto intro: sum.induct) lemma sum_RECURSION: - "\Inl' Inr'. \fn. (\a. fn (Inl a) = Inl' a) \ (\a. fn (Inr a) = Inr' a)" + "\Inl' Inr'. \fn. (\a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \ (\a :: 'B. fn (Inr a) = Inr' a)" by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto lemma OUTL[import_const "OUTL" : "Sum_Type.Projl"]: @@ -249,7 +249,7 @@ by simp lemma LENGTH[import_const LENGTH : List.length]: - "length [] = id 0 \ (\(h\'A) t. length (h # t) = Suc (length t))" + "length ([] :: 'A list) = id 0 \ (\(h\'A) t. length (h # t) = Suc (length t))" by simp lemma MAP[import_const MAP : List.map]: @@ -307,7 +307,7 @@ by simp lemma WF[import_const WF : Wellfounded.wfP]: - "wfP u \ (\P. (\x :: 'A. P x) \ (\x. P x \ (\y. u y x \ \ P y)))" + "\u. wfP u \ (\P. (\x :: 'A. P x) \ (\x. P x \ (\y. u y x \ \ P y)))" proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred]) fix x :: "'a \ 'a \ bool" and xa :: "'a" and Q assume a: "xa \ Q"