src/HOL/ex/FinFunPred.thy

--- a/src/HOL/ex/FinFunPred.thy	Wed May 30 08:48:14 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 09:13:39 2012 +0200
@@ -13,7 +13,7 @@
 instantiation "finfun" :: (type, ord) ord
 begin
 
-definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)"
+definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
 
 definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
 
@@ -36,7 +36,7 @@
 instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
 end
 
-lemma bot_finfun_apply [simp]: "bot\<^sub>f = (\<lambda>_. bot)"
+lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
 by(auto simp add: bot_finfun_def)
 
 instantiation "finfun" :: (type, top) top begin
@@ -44,7 +44,7 @@
 instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
 end
 
-lemma top_finfun_apply [simp]: "top\<^sub>f = (\<lambda>_. top)"
+lemma top_finfun_apply [simp]: "op $ top = (\<lambda>_. top)"
 by(auto simp add: top_finfun_def)
 
 instantiation "finfun" :: (type, inf) inf begin
@@ -52,7 +52,7 @@
 instance ..
 end
 
-lemma inf_finfun_apply [simp]: "(inf f g)\<^sub>f = inf f\<^sub>f g\<^sub>f"
+lemma inf_finfun_apply [simp]: "op $ (inf f g) = inf (op $ f) (op $ g)"
 by(auto simp add: inf_finfun_def o_def inf_fun_def)
 
 instantiation "finfun" :: (type, sup) sup begin
@@ -60,7 +60,7 @@
 instance ..
 end
 
-lemma sup_finfun_apply [simp]: "(sup f g)\<^sub>f = sup f\<^sub>f g\<^sub>f"
+lemma sup_finfun_apply [simp]: "op $ (sup f g) = sup (op $ f) (op $ g)"
 by(auto simp add: sup_finfun_def o_def sup_fun_def)
 
 instance "finfun" :: (type, semilattice_inf) semilattice_inf
@@ -82,7 +82,7 @@
 instance ..
 end
 
-lemma minus_finfun_apply [simp]: "(f - g)\<^sub>f = f\<^sub>f - g\<^sub>f"
+lemma minus_finfun_apply [simp]: "op $ (f - g) = op $ f - op $ g"
 by(simp add: minus_finfun_def o_def fun_diff_def)
 
 instantiation "finfun" :: (type, uminus) uminus begin
@@ -90,7 +90,7 @@
 instance ..
 end
 
-lemma uminus_finfun_apply [simp]: "(- g)\<^sub>f = - g\<^sub>f"
+lemma uminus_finfun_apply [simp]: "op $ (- g) = - op $ g"
 by(simp add: uminus_finfun_def o_def fun_Compl_def)
 
 instance "finfun" :: (type, boolean_algebra) boolean_algebra
@@ -111,7 +111,7 @@
 where [code]: "finfun_single x = finfun_empty(\<^sup>f x := True)"
 
 lemma finfun_single_apply [simp]:
-  "(finfun_single x)\<^sub>f y \<longleftrightarrow> x = y"
+  "finfun_single x $ y \<longleftrightarrow> x = y"
 by(simp add: finfun_single_def finfun_upd_apply)
 
 lemma [iff]:
@@ -119,10 +119,10 @@
   and bot_neq_finfun_single: "bot \<noteq> finfun_single x"
 by(simp_all add: expand_finfun_eq fun_eq_iff)
 
-lemma finfun_leI [intro!]: "(!!x. A\<^sub>f x \<Longrightarrow> B\<^sub>f x) \<Longrightarrow> A \<le> B"
+lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B"
 by(simp add: le_finfun_def)
 
-lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A\<^sub>f x \<rbrakk> \<Longrightarrow> B\<^sub>f x"
+lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x"
 by(simp add: le_finfun_def)
 
 text {* Bounded quantification.
@@ -130,7 +130,7 @@
 *}
 
 definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A\<^sub>f a \<longrightarrow> a \<in> set xs \<or> P a)"
+where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
 
 lemma finfun_Ball_except_const:
   "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
@@ -150,14 +150,14 @@
 by(simp add: finfun_Ball_except_update)
 
 definition finfun_Ball :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Ball A P = Ball {x. A\<^sub>f x} P"
+where [code del]: "finfun_Ball A P = Ball {x. A $ x} P"
 
 lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
 by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)
 
 
 definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A\<^sub>f a \<and> a \<notin> set xs \<and> P a)"
+where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
 
 lemma finfun_Bex_except_const:
   "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
@@ -177,7 +177,7 @@
 by(simp add: finfun_Bex_except_update)
 
 definition finfun_Bex :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Bex A P = Bex {x. A\<^sub>f x} P"
+where [code del]: "finfun_Bex A P = Bex {x. A $ x} P"
 
 lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
 by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)
@@ -186,54 +186,54 @@
 text {* Automatically replace predicate operations by finfun predicate operations where possible *}
 
 lemma iso_finfun_le [code_unfold]:
-  "A\<^sub>f \<le> B\<^sub>f \<longleftrightarrow> A \<le> B"
+  "op $ A \<le> op $ B \<longleftrightarrow> A \<le> B"
 by (metis le_finfun_def le_funD le_funI)
 
 lemma iso_finfun_less [code_unfold]:
-  "A\<^sub>f < B\<^sub>f \<longleftrightarrow> A < B"
+  "op $ A < op $ B \<longleftrightarrow> A < B"
 by (metis iso_finfun_le less_finfun_def less_fun_def)
 
 lemma iso_finfun_eq [code_unfold]:
-  "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B"
+  "op $ A = op $ B \<longleftrightarrow> A = B"
 by(simp only: expand_finfun_eq)
 
 lemma iso_finfun_sup [code_unfold]:
-  "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"
+  "sup (op $ A) (op $ B) = op $ (sup A B)"
 by(simp)
 
 lemma iso_finfun_disj [code_unfold]:
-  "A\<^sub>f x \<or> B\<^sub>f x \<longleftrightarrow> (sup A B)\<^sub>f x"
+  "A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x"
 by(simp add: sup_fun_def)
 
 lemma iso_finfun_inf [code_unfold]:
-  "inf A\<^sub>f B\<^sub>f = (inf A B)\<^sub>f"
+  "inf (op $ A) (op $ B) = op $ (inf A B)"
 by(simp)
 
 lemma iso_finfun_conj [code_unfold]:
-  "A\<^sub>f x \<and> B\<^sub>f x \<longleftrightarrow> (inf A B)\<^sub>f x"
+  "A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x"
 by(simp add: inf_fun_def)
 
 lemma iso_finfun_empty_conv [code_unfold]:
-  "(\<lambda>_. False) = {}\<^isub>f\<^sub>f"
+  "(\<lambda>_. False) = op $ {}\<^isub>f"
 by simp
 
 lemma iso_finfun_UNIV_conv [code_unfold]:
-  "(\<lambda>_. True) = finfun_UNIV\<^sub>f"
+  "(\<lambda>_. True) = op $ finfun_UNIV"
 by simp
 
 lemma iso_finfun_upd [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "A\<^sub>f(x := b) = (A(\<^sup>f x := b))\<^sub>f"
+  shows "(op $ A)(x := b) = op $ (A(\<^sup>f x := b))"
 by(simp add: fun_eq_iff)
 
 lemma iso_finfun_uminus [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "- A\<^sub>f = (- A)\<^sub>f"
+  shows "- op $ A = op $ (- A)"
 by(simp)
 
 lemma iso_finfun_minus [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "A\<^sub>f - B\<^sub>f = (A - B)\<^sub>f"
+  shows "op $ A - op $ B = op $ (A - B)"
 by(simp)
 
 text {*
@@ -243,11 +243,11 @@
 *}
 
 lemma iso_finfun_Ball_Ball:
-  "(\<forall>x. A\<^sub>f x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
+  "(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
 by(simp add: finfun_Ball_def)
 
 lemma iso_finfun_Bex_Bex:
-  "(\<exists>x. A\<^sub>f x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
+  "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
 by(simp add: finfun_Bex_def)
 
 text {* Test replacement setup *}