removed subscripts from FinFun type syntax
authorAndreas Lochbihler
Wed May 30 08:48:14 2012 +0200 (2012-05-30)
changeset 480341c5171abe5cc
parent 48033 65eb8910a779
child 48035 2f9584581cf2
removed subscripts from FinFun type syntax
src/HOL/Library/FinFun.thy
src/HOL/ex/FinFunPred.thy
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 08:34:14 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 08:48:14 2012 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5  definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
     1.6  
     1.7 -typedef (open) ('a,'b) finfun  ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
     1.8 +typedef (open) ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
     1.9    morphisms finfun_apply Abs_finfun
    1.10  proof -
    1.11    have "\<exists>f. finite {x. f x \<noteq> undefined}"
    1.12 @@ -93,6 +93,8 @@
    1.13    then show ?thesis unfolding finfun_def by auto
    1.14  qed
    1.15  
    1.16 +type_notation finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    1.17 +
    1.18  setup_lifting type_definition_finfun
    1.19  
    1.20  lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
    1.21 @@ -220,7 +222,7 @@
    1.22  
    1.23  lemma Abs_finfun_inj_finite:
    1.24    assumes fin: "finite (UNIV :: 'a set)"
    1.25 -  shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
    1.26 +  shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'b)"
    1.27  proof(rule inj_onI)
    1.28    fix x y :: "'a \<Rightarrow> 'b"
    1.29    assume "Abs_finfun x = Abs_finfun y"
    1.30 @@ -274,12 +276,13 @@
    1.31  qed
    1.32  
    1.33  
    1.34 -subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
    1.35 +subsection {* Kernel functions for type @{typ "'a \<Rightarrow>f 'b"} *}
    1.36  
    1.37 -lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
    1.38 +lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
    1.39  is "\<lambda> b x. b" by (rule const_finfun)
    1.40  
    1.41 -lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
    1.42 +lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd"
    1.43 +by (simp add: fun_upd_finfun)
    1.44  
    1.45  lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
    1.46  by transfer (simp add: fun_upd_twist)
    1.47 @@ -293,7 +296,7 @@
    1.48  
    1.49  subsection {* Code generator setup *}
    1.50  
    1.51 -definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
    1.52 +definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
    1.53  where [simp, code del]: "finfun_update_code = finfun_update"
    1.54  
    1.55  code_datatype finfun_const finfun_update_code
    1.56 @@ -309,7 +312,7 @@
    1.57  
    1.58  subsection {* Setup for quickcheck *}
    1.59  
    1.60 -quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
    1.61 +quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.62  
    1.63  subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
    1.64  
    1.65 @@ -414,7 +417,7 @@
    1.66    case True thus ?thesis by(simp add: finfun_default_aux_def)
    1.67  qed
    1.68  
    1.69 -lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
    1.70 +lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
    1.71  is "finfun_default_aux" ..
    1.72  
    1.73  lemma finfun_apply_transfer [transfer_rule]: 
    1.74 @@ -424,7 +427,7 @@
    1.75  lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
    1.76  by transfer (erule finite_finfun_default_aux)
    1.77  
    1.78 -lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
    1.79 +lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
    1.80  by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def)
    1.81  
    1.82  lemma finfun_default_update_const:
    1.83 @@ -432,7 +435,7 @@
    1.84  by transfer (simp add: finfun_default_aux_update_const)
    1.85  
    1.86  lemma finfun_default_const_code [code]:
    1.87 -  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
    1.88 +  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
    1.89  by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
    1.90  
    1.91  lemma finfun_default_update_code [code]:
    1.92 @@ -441,7 +444,7 @@
    1.93  
    1.94  subsection {* Recursion combinator and well-formedness conditions *}
    1.95  
    1.96 -definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
    1.97 +definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> 'c"
    1.98  where [code del]:
    1.99    "finfun_rec cnst upd f \<equiv>
   1.100     let b = finfun_default f;
   1.101 @@ -740,7 +743,7 @@
   1.102    "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
   1.103  proof(cases "finite (UNIV :: 'a set)")
   1.104    case False
   1.105 -  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
   1.106 +  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
   1.107    moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
   1.108    proof (rule the_equality)
   1.109      show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
   1.110 @@ -757,7 +760,7 @@
   1.111    ultimately show ?thesis by(simp add: finfun_rec_def)
   1.112  next
   1.113    case True
   1.114 -  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
   1.115 +  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
   1.116    let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   1.117    show ?thesis
   1.118    proof(cases "c = undefined")
   1.119 @@ -840,14 +843,14 @@
   1.120  by(atomize_elim)(rule finfun_exhaust_disj)
   1.121  
   1.122  lemma finfun_rec_unique:
   1.123 -  fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
   1.124 +  fixes f :: "'a \<Rightarrow>f 'b \<Rightarrow> 'c"
   1.125    assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
   1.126    and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
   1.127    and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
   1.128    and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
   1.129    shows "f = f'"
   1.130  proof
   1.131 -  fix g :: "'a \<Rightarrow>\<^isub>f 'b"
   1.132 +  fix g :: "'a \<Rightarrow>f 'b"
   1.133    show "f g = f' g"
   1.134      by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
   1.135  qed
   1.136 @@ -910,7 +913,7 @@
   1.137  
   1.138  subsection {* Function composition *}
   1.139  
   1.140 -definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
   1.141 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "\<circ>\<^isub>f" 55)
   1.142  where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
   1.143  
   1.144  interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
   1.145 @@ -968,7 +971,7 @@
   1.146    thus ?thesis by(auto simp add: fun_eq_iff)
   1.147  qed
   1.148  
   1.149 -definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
   1.150 +definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
   1.151  where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
   1.152  
   1.153  lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
   1.154 @@ -991,7 +994,7 @@
   1.155  
   1.156  subsection {* Universal quantification *}
   1.157  
   1.158 -definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
   1.159 +definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.160  where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
   1.161  
   1.162  lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
   1.163 @@ -1010,7 +1013,7 @@
   1.164    shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
   1.165  by(simp add: finfun_All_except_update)
   1.166  
   1.167 -definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
   1.168 +definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.169  where "finfun_All = finfun_All_except []"
   1.170  
   1.171  lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
   1.172 @@ -1023,7 +1026,7 @@
   1.173  by(simp add: finfun_All_def finfun_All_except_def)
   1.174  
   1.175  
   1.176 -definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
   1.177 +definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.178  where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
   1.179  
   1.180  lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
   1.181 @@ -1035,7 +1038,7 @@
   1.182  
   1.183  subsection {* A diagonal operator for FinFuns *}
   1.184  
   1.185 -definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
   1.186 +definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
   1.187  where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
   1.188  
   1.189  interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
   1.190 @@ -1100,7 +1103,7 @@
   1.191    "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
   1.192    including finfun
   1.193  proof -
   1.194 -  have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x))))"
   1.195 +  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x))))"
   1.196    proof(rule finfun_rec_unique)
   1.197      { fix c show "Abs_finfun (\<lambda>x. (finfun_apply (\<lambda>\<^isup>f c) x, finfun_apply g x)) = Pair c \<circ>\<^isub>f g"
   1.198          by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
   1.199 @@ -1115,7 +1118,7 @@
   1.200  lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
   1.201  by(auto simp add: expand_finfun_eq fun_eq_iff)
   1.202  
   1.203 -definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
   1.204 +definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.205  where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
   1.206  
   1.207  lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
   1.208 @@ -1135,7 +1138,7 @@
   1.209  by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
   1.210  
   1.211  
   1.212 -definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
   1.213 +definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
   1.214  where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
   1.215  
   1.216  lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
   1.217 @@ -1161,7 +1164,7 @@
   1.218  
   1.219  subsection {* Currying for FinFuns *}
   1.220  
   1.221 -definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
   1.222 +definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
   1.223  where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
   1.224  
   1.225  interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
   1.226 @@ -1211,22 +1214,23 @@
   1.227  qed
   1.228  
   1.229  lemma finfun_curry_conv_curry:
   1.230 -  fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
   1.231 +  fixes f :: "('a \<times> 'b) \<Rightarrow>f 'c"
   1.232    shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
   1.233    including finfun
   1.234  proof -
   1.235 -  have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
   1.236 +  have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
   1.237    proof(rule finfun_rec_unique)
   1.238 -    { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
   1.239 -    { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
   1.240 -        by(cases a) simp }
   1.241 -    { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.242 -        by(simp add: finfun_curry_def finfun_const_def curry_def) }
   1.243 -    { fix g a b
   1.244 -      show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
   1.245 -       (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
   1.246 -       fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
   1.247 -        by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_curry finfun_Abs_finfun_curry) }
   1.248 +    fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp
   1.249 +    fix f a
   1.250 +    show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
   1.251 +      by(cases a) simp
   1.252 +    show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.253 +      by(simp add: finfun_curry_def finfun_const_def curry_def)
   1.254 +    fix g b
   1.255 +    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
   1.256 +      (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
   1.257 +      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
   1.258 +      by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_curry finfun_Abs_finfun_curry)
   1.259    qed
   1.260    thus ?thesis by(auto simp add: fun_eq_iff)
   1.261  qed
   1.262 @@ -1242,12 +1246,12 @@
   1.263  end
   1.264  
   1.265  lemma [code nbe]:
   1.266 -  "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
   1.267 +  "HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True"
   1.268    by (fact equal_refl)
   1.269  
   1.270  subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
   1.271  
   1.272 -definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
   1.273 +definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.274  where [simp, code del]: "finfun_clearjunk = id"
   1.275  
   1.276  lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
   1.277 @@ -1258,11 +1262,11 @@
   1.278  
   1.279  subsection {* The domain of a FinFun as a FinFun *}
   1.280  
   1.281 -definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
   1.282 +definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
   1.283  where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
   1.284  
   1.285  lemma finfun_dom_const:
   1.286 -  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
   1.287 +  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
   1.288  unfolding finfun_dom_def finfun_default_const
   1.289  by(auto)(simp_all add: finfun_const_def)
   1.290  
   1.291 @@ -1272,7 +1276,7 @@
   1.292  *}
   1.293  
   1.294  lemma finfun_dom_const_code [code]:
   1.295 -  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = 
   1.296 +  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
   1.297     (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
   1.298  unfolding card_UNIV_eq_0_infinite_UNIV
   1.299  by(simp add: finfun_dom_const)
   1.300 @@ -1310,7 +1314,7 @@
   1.301  
   1.302  subsection {* The domain of a FinFun as a sorted list *}
   1.303  
   1.304 -definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
   1.305 +definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
   1.306  where
   1.307    "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
   1.308  
   1.309 @@ -1331,13 +1335,13 @@
   1.310  by auto
   1.311  
   1.312  lemma finfun_to_list_const:
   1.313 -  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) = 
   1.314 +  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
   1.315    (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
   1.316  by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
   1.317  
   1.318  lemma finfun_to_list_const_code [code]:
   1.319 -  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
   1.320 -   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
   1.321 +  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
   1.322 +   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>f 'b))))"
   1.323  unfolding card_UNIV_eq_0_infinite_UNIV
   1.324  by(auto simp add: finfun_to_list_const)
   1.325  
     2.1 --- a/src/HOL/ex/FinFunPred.thy	Wed May 30 08:34:14 2012 +0200
     2.2 +++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 08:48:14 2012 +0200
     2.3 @@ -8,14 +8,14 @@
     2.4  
     2.5  text {* Instantiate FinFun predicates just like predicates *}
     2.6  
     2.7 -type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>\<^isub>f bool"
     2.8 +type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>f bool"
     2.9  
    2.10  instantiation "finfun" :: (type, ord) ord
    2.11  begin
    2.12  
    2.13  definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)"
    2.14  
    2.15 -definition [code del]: "(f\<Colon>'a \<Rightarrow>\<^isub>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
    2.16 +definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
    2.17  
    2.18  instance ..
    2.19