# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# 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 = (\<lambda>p\<Colon>'A \<times> 'B. SOME y\<Colon>'B. \<exists>x\<Colon>'A. p = (x, y))"
   by auto
 
-(*lemma [import_const CURRY]:
+lemma CURRY_DEF[import_const CURRY]:
   "curry = (\<lambda>(f\<Colon>'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
-  using curry_def .*)
+  using curry_def .
 
 lemma [import_const ONE_ONE : Fun.inj]:
   "inj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
@@ -200,16 +200,16 @@
   "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> 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:
-  "\<forall>P. (\<forall>a. P (Inl a)) \<and> (\<forall>a. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
+  "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
   by (auto intro: sum.induct)
 
 lemma sum_RECURSION:
-  "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a. fn (Inl a) = Inl' a) \<and> (\<forall>a. fn (Inr a) = Inr' a)"
+  "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>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 \<and> (\<forall>(h\<Colon>'A) t. length (h # t) = Suc (length t))"
+  "length ([] :: 'A list) = id 0 \<and> (\<forall>(h\<Colon>'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 \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
+  "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
 proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
   fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
   assume a: "xa \<in> Q"