eliminated remaining sub- and superscripts in FinFun syntax
authorAndreas Lochbihler
Wed May 30 09:54:53 2012 +0200 (2012-05-30)
changeset 4803872a8506dd59b
parent 48037 6c4b3e78f03e
child 48039 daab96c3e2a9
eliminated remaining sub- and superscripts in FinFun syntax
src/HOL/Library/FinFun.thy
src/HOL/ex/FinFunPred.thy
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 09:46:58 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:54:53 2012 +0200
     1.3 @@ -1045,8 +1045,8 @@
     1.4  
     1.5  subsection {* A diagonal operator for FinFuns *}
     1.6  
     1.7 -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.8 -where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
     1.9 +definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'($_,/ _$'))" [0, 0] 1000)
    1.10 +where [code del]: "($f, g$) = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
    1.11  
    1.12  interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
    1.13  by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
    1.14 @@ -1066,51 +1066,51 @@
    1.15      by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
    1.16  qed
    1.17  
    1.18 -lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>$ g"
    1.19 +lemma finfun_Diag_const1: "($K$ b, g$) = Pair b \<circ>$ g"
    1.20  by(simp add: finfun_Diag_def)
    1.21  
    1.22  text {*
    1.23 -  Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{text "\<circ>\<^isub>f"}.
    1.24 +  Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{term "op \<circ>$"}.
    1.25  *}
    1.26  
    1.27  lemma finfun_Diag_const_code [code]:
    1.28 -  "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
    1.29 -  "(K$ b, finfun_update_code g a c)\<^sup>f = finfun_update_code (K$ b, g)\<^sup>f a (b, c)"
    1.30 +  "($K$ b, K$ c$) = (K$ (b, c))"
    1.31 +  "($K$ b, finfun_update_code g a c$) = finfun_update_code ($K$ b, g$) a (b, c)"
    1.32  by(simp_all add: finfun_Diag_const1)
    1.33  
    1.34 -lemma finfun_Diag_update1: "(f(a $:= b), g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
    1.35 -  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
    1.36 +lemma finfun_Diag_update1: "($f(a $:= b), g$) = ($f, g$)(a $:= (b, g $ a))"
    1.37 +  and finfun_Diag_update1_code [code]: "($finfun_update_code f a b, g$) = ($f, g$)(a $:= (b, g $ a))"
    1.38  by(simp_all add: finfun_Diag_def)
    1.39  
    1.40 -lemma finfun_Diag_const2: "(f, K$ c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>$ f"
    1.41 +lemma finfun_Diag_const2: "($f, K$ c$) = (\<lambda>b. (b, c)) \<circ>$ f"
    1.42  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
    1.43  
    1.44 -lemma finfun_Diag_update2: "(f, g(a $:= c))\<^sup>f = (f, g)\<^sup>f(a $:= (f $ a, c))"
    1.45 +lemma finfun_Diag_update2: "($f, g(a $:= c)$) = ($f, g$)(a $:= (f $ a, c))"
    1.46  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
    1.47  
    1.48 -lemma finfun_Diag_const_const [simp]: "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
    1.49 +lemma finfun_Diag_const_const [simp]: "($K$ b, K$ c$) = (K$ (b, c))"
    1.50  by(simp add: finfun_Diag_const1)
    1.51  
    1.52  lemma finfun_Diag_const_update:
    1.53 -  "(K$ b, g(a $:= c))\<^sup>f = (K$ b, g)\<^sup>f(a $:= (b, c))"
    1.54 +  "($K$ b, g(a $:= c)$) = ($K$ b, g$)(a $:= (b, c))"
    1.55  by(simp add: finfun_Diag_const1)
    1.56  
    1.57  lemma finfun_Diag_update_const:
    1.58 -  "(f(a $:= b), K$ c)\<^sup>f = (f, K$ c)\<^sup>f(a $:= (b, c))"
    1.59 +  "($f(a $:= b), K$ c$) = ($f, K$ c$)(a $:= (b, c))"
    1.60  by(simp add: finfun_Diag_def)
    1.61  
    1.62  lemma finfun_Diag_update_update:
    1.63 -  "(f(a $:= b), g(a' $:= c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(a $:= (b, c)) else (f, g)\<^sup>f(a $:= (b, g $ a))(a' $:= (f $ a', c)))"
    1.64 +  "($f(a $:= b), g(a' $:= c)$) = (if a = a' then ($f, g$)(a $:= (b, c)) else ($f, g$)(a $:= (b, g $ a))(a' $:= (f $ a', c)))"
    1.65  by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
    1.66  
    1.67 -lemma finfun_Diag_apply [simp]: "op $ (f, g)\<^sup>f = (\<lambda>x. (f $ x, g $ x))"
    1.68 +lemma finfun_Diag_apply [simp]: "op $ ($f, g$) = (\<lambda>x. (f $ x, g $ x))"
    1.69  by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply)
    1.70  
    1.71  lemma finfun_Diag_conv_Abs_finfun:
    1.72 -  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
    1.73 +  "($f, g$) = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
    1.74    including finfun
    1.75  proof -
    1.76 -  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
    1.77 +  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. ($f, g$)) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
    1.78    proof(rule finfun_rec_unique)
    1.79      { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>$ g"
    1.80          by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
    1.81 @@ -1122,7 +1122,7 @@
    1.82    thus ?thesis by(auto simp add: fun_eq_iff)
    1.83  qed
    1.84  
    1.85 -lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
    1.86 +lemma finfun_Diag_eq: "($f, g$) = ($f', g'$) \<longleftrightarrow> f = f' \<and> g = g'"
    1.87  by(auto simp add: expand_finfun_eq fun_eq_iff)
    1.88  
    1.89  definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.90 @@ -1138,7 +1138,7 @@
    1.91  lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g"
    1.92  by(simp add: finfun_fst_def)
    1.93  
    1.94 -lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
    1.95 +lemma finfun_fst_conv [simp]: "finfun_fst ($f, g$) = f"
    1.96  by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update)
    1.97  
    1.98  lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))"
    1.99 @@ -1158,7 +1158,7 @@
   1.100  lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g"
   1.101  by(simp add: finfun_snd_def)
   1.102  
   1.103 -lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
   1.104 +lemma finfun_snd_conv [simp]: "finfun_snd ($f, g$) = g"
   1.105  apply(induct f rule: finfun_weak_induct)
   1.106  apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext)
   1.107  done
   1.108 @@ -1166,7 +1166,7 @@
   1.109  lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))"
   1.110  by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
   1.111  
   1.112 -lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
   1.113 +lemma finfun_Diag_collapse [simp]: "($finfun_fst f, finfun_snd f$) = f"
   1.114  by(induct f rule: finfun_weak_induct)(simp_all add: finfun_fst_const finfun_snd_const finfun_fst_update finfun_snd_update finfun_Diag_update_update)
   1.115  
   1.116  subsection {* Currying for FinFuns *}
   1.117 @@ -1244,11 +1244,11 @@
   1.118  
   1.119  subsection {* Executable equality for FinFuns *}
   1.120  
   1.121 -lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
   1.122 +lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
   1.123  by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
   1.124  
   1.125  instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
   1.126 -definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
   1.127 +definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
   1.128  instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
   1.129  end
   1.130  
     2.1 --- a/src/HOL/ex/FinFunPred.thy	Wed May 30 09:46:58 2012 +0200
     2.2 +++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 09:54:53 2012 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  instance ..
     2.5  
     2.6  lemma le_finfun_code [code]:
     2.7 -  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ (f, g)\<^sup>f)"
     2.8 +  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))"
     2.9  by(simp add: le_finfun_def finfun_All_All o_def)
    2.10  
    2.11  end
    2.12 @@ -48,7 +48,7 @@
    2.13  by(auto simp add: top_finfun_def)
    2.14  
    2.15  instantiation "finfun" :: (type, inf) inf begin
    2.16 -definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ (f, g)\<^sup>f"
    2.17 +definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ ($f, g$)"
    2.18  instance ..
    2.19  end
    2.20  
    2.21 @@ -56,7 +56,7 @@
    2.22  by(auto simp add: inf_finfun_def o_def inf_fun_def)
    2.23  
    2.24  instantiation "finfun" :: (type, sup) sup begin
    2.25 -definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ (f, g)\<^sup>f"
    2.26 +definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ ($f, g$)"
    2.27  instance ..
    2.28  end
    2.29  
    2.30 @@ -78,7 +78,7 @@
    2.31  by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
    2.32  
    2.33  instantiation "finfun" :: (type, minus) minus begin
    2.34 -definition "f - g = split (op -) \<circ>$ (f, g)\<^sup>f"
    2.35 +definition "f - g = split (op -) \<circ>$ ($f, g$)"
    2.36  instance ..
    2.37  end
    2.38