# HG changeset patch
# User blanchet
# Date 1384866686 -3600
# Node ID 930409d4321149246e040c6e4f4b766e700e49fc
# Parent  03ff4d1e6784108a12513b344a628c1f6fc5b131
use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package

diff -r 03ff4d1e6784 -r 930409d43211 src/HOL/BNF/Examples/Koenig.thy
--- a/src/HOL/BNF/Examples/Koenig.thy	Tue Nov 19 10:05:53 2013 +0100
+++ b/src/HOL/BNF/Examples/Koenig.thy	Tue Nov 19 14:11:26 2013 +0100
@@ -12,44 +12,33 @@
 imports TreeFI Stream
 begin
 
-(* selectors for streams *)
-lemma shd_def': "shd as = fst (stream_dtor as)"
-apply (case_tac as)
-apply (auto simp add: shd_def)
-by (simp add: Stream_def stream.dtor_ctor)
-
-lemma stl_def': "stl as = snd (stream_dtor as)"
-apply (case_tac as)
-apply (auto simp add: stl_def)
-by (simp add: Stream_def stream.dtor_ctor)
-
 (* infinite trees: *)
 coinductive infiniteTr where
-"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
+"\<lbrakk>tr' \<in> set_listF (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
 
 lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
 assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr' \<or> infiniteTr tr'"
 shows "infiniteTr tr"
 using assms by (elim infiniteTr.coinduct) blast
 
 lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
 assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr'"
 shows "infiniteTr tr"
 using assms by (elim infiniteTr.coinduct) blast
 
 lemma infiniteTr_sub[simp]:
-"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
+"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set_listF (sub tr). infiniteTr tr')"
 by (erule infiniteTr.cases) blast
 
 primcorec konigPath where
   "shd (konigPath t) = lab t"
-| "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
+| "stl (konigPath t) = konigPath (SOME tr. tr \<in> set_listF (sub t) \<and> infiniteTr tr)"
 
 (* proper paths in trees: *)
 coinductive properPath where
-"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
+"\<lbrakk>shd as = lab tr; tr' \<in> set_listF (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
  properPath as tr"
 
 lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
@@ -57,7 +46,7 @@
 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
 ***: "\<And> as tr.
          phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+         \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
 shows "properPath as tr"
 using assms by (elim properPath.coinduct) blast
 
@@ -66,7 +55,7 @@
 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
 ***: "\<And> as tr.
          phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
+         \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr'"
 shows "properPath as tr"
 using properPath_strong_coind[of phi, OF * **] *** by blast
 
@@ -76,7 +65,7 @@
 
 lemma properPath_sub:
 "properPath as tr \<Longrightarrow>
- \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+ \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
 by (erule properPath.cases) blast
 
 (* prove the following by coinduction *)
@@ -88,10 +77,10 @@
    assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
    proof (coinduction arbitrary: tr as rule: properPath_coind)
      case (sub tr as)
-     let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'"
-     from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp
-     then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast
-     then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
+     let ?t = "SOME t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'"
+     from sub have "\<exists>t' \<in> set_listF (sub tr). infiniteTr t'" by simp
+     then have "\<exists>t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'" by blast
+     then have "?t \<in> set_listF (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
      moreover have "stl (konigPath tr) = konigPath ?t" by simp
      ultimately show ?case using sub by blast
    qed simp
diff -r 03ff4d1e6784 -r 930409d43211 src/HOL/BNF/Examples/ListF.thy
--- a/src/HOL/BNF/Examples/ListF.thy	Tue Nov 19 10:05:53 2013 +0100
+++ b/src/HOL/BNF/Examples/ListF.thy	Tue Nov 19 14:11:26 2013 +0100
@@ -62,7 +62,7 @@
   "i < lengthh xs \<Longrightarrow> nthh (mapF f xs) i = f (nthh xs i)"
   by (induct rule: nthh.induct) auto
 
-lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> listF_set xs"
+lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs"
   by (induct rule: nthh.induct) auto
 
 lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)"
@@ -105,7 +105,7 @@
 qed simp
 
 lemma list_set_nthh[simp]:
-  "(x \<in> listF_set xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
+  "(x \<in> set_listF xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
   by (induct xs) (auto, induct rule: nthh.induct, auto)
 
 end
diff -r 03ff4d1e6784 -r 930409d43211 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Tue Nov 19 10:05:53 2013 +0100
+++ b/src/HOL/BNF/Examples/Process.thy	Tue Nov 19 14:11:26 2013 +0100
@@ -22,7 +22,7 @@
 subsection {* Basic properties *}
 
 declare
-  pre_process_rel_def[simp]
+  rel_pre_process_def[simp]
   sum_rel_def[simp]
   prod_rel_def[simp]
 
diff -r 03ff4d1e6784 -r 930409d43211 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 10:05:53 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Tue Nov 19 14:11:26 2013 +0100
@@ -909,18 +909,18 @@
 by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   intro: mmap_cong wpull_mmap)
 
-inductive multiset_rel' where
-Zero: "multiset_rel' R {#} {#}"
+inductive rel_multiset' where
+Zero: "rel_multiset' R {#} {#}"
 |
-Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
+Plus: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
 
-lemma multiset_map_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
+lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
 by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
 
-lemma multiset_map_Zero[simp]: "mmap f {#} = {#}" by simp
+lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
 
-lemma multiset_rel_Zero: "multiset_rel R {#} {#}"
-unfolding multiset_rel_def Grp_def by auto
+lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
+unfolding rel_multiset_def Grp_def by auto
 
 declare multiset.count[simp]
 declare Abs_multiset_inverse[simp]
@@ -928,7 +928,7 @@
 declare union_preserves_multiset[simp]
 
 
-lemma multiset_map_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
+lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
 proof (intro multiset_eqI, transfer fixing: f)
   fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
   assume "M1 \<in> multiset" "M2 \<in> multiset"
@@ -941,12 +941,12 @@
     by (auto simp: setsum.distrib[symmetric])
 qed
 
-lemma multiset_map_singl[simp]: "mmap f {#a#} = {#f a#}"
+lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}"
   by transfer auto
 
-lemma multiset_rel_Plus:
-assumes ab: "R a b" and MN: "multiset_rel R M N"
-shows "multiset_rel R (M + {#a#}) (N + {#b#})"
+lemma rel_multiset_Plus:
+assumes ab: "R a b" and MN: "rel_multiset R M N"
+shows "rel_multiset R (M + {#a#}) (N + {#b#})"
 proof-
   {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
    hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
@@ -956,13 +956,13 @@
   }
   thus ?thesis
   using assms
-  unfolding multiset_rel_def Grp_def by force
+  unfolding rel_multiset_def Grp_def by force
 qed
 
-lemma multiset_rel'_imp_multiset_rel:
-"multiset_rel' R M N \<Longrightarrow> multiset_rel R M N"
-apply(induct rule: multiset_rel'.induct)
-using multiset_rel_Zero multiset_rel_Plus by auto
+lemma rel_multiset'_imp_rel_multiset:
+"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
+apply(induct rule: rel_multiset'.induct)
+using rel_multiset_Zero rel_multiset_Plus by auto
 
 lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
 proof -
@@ -994,10 +994,10 @@
   then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
 qed
 
-lemma multiset_rel_mcard:
-assumes "multiset_rel R M N"
+lemma rel_multiset_mcard:
+assumes "rel_multiset R M N"
 shows "mcard M = mcard N"
-using assms unfolding multiset_rel_def Grp_def by auto
+using assms unfolding rel_multiset_def Grp_def by auto
 
 lemma multiset_induct2[case_names empty addL addR]:
 assumes empty: "P {#} {#}"
@@ -1052,67 +1052,67 @@
 qed
 
 lemma msed_rel_invL:
-assumes "multiset_rel R (M + {#a#}) N"
-shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> multiset_rel R M N1"
+assumes "rel_multiset R (M + {#a#}) N"
+shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
 proof-
   obtain K where KM: "mmap fst K = M + {#a#}"
   and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   using assms
-  unfolding multiset_rel_def Grp_def by auto
+  unfolding rel_multiset_def Grp_def by auto
   obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
   obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
   using msed_map_invL[OF KN[unfolded K]] by auto
   have Rab: "R a (snd ab)" using sK a unfolding K by auto
-  have "multiset_rel R M N1" using sK K1M K1N1
-  unfolding K multiset_rel_def Grp_def by auto
+  have "rel_multiset R M N1" using sK K1M K1N1
+  unfolding K rel_multiset_def Grp_def by auto
   thus ?thesis using N Rab by auto
 qed
 
 lemma msed_rel_invR:
-assumes "multiset_rel R M (N + {#b#})"
-shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> multiset_rel R M1 N"
+assumes "rel_multiset R M (N + {#b#})"
+shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
 proof-
   obtain K where KN: "mmap snd K = N + {#b#}"
   and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   using assms
-  unfolding multiset_rel_def Grp_def by auto
+  unfolding rel_multiset_def Grp_def by auto
   obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
   and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
   obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
   using msed_map_invL[OF KM[unfolded K]] by auto
   have Rab: "R (fst ab) b" using sK b unfolding K by auto
-  have "multiset_rel R M1 N" using sK K1N K1M1
-  unfolding K multiset_rel_def Grp_def by auto
+  have "rel_multiset R M1 N" using sK K1N K1M1
+  unfolding K rel_multiset_def Grp_def by auto
   thus ?thesis using M Rab by auto
 qed
 
-lemma multiset_rel_imp_multiset_rel':
-assumes "multiset_rel R M N"
-shows "multiset_rel' R M N"
+lemma rel_multiset_imp_rel_multiset':
+assumes "rel_multiset R M N"
+shows "rel_multiset' R M N"
 using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   case (less M)
-  have c: "mcard M = mcard N" using multiset_rel_mcard[OF less.prems] .
+  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
   show ?case
   proof(cases "M = {#}")
     case True hence "N = {#}" using c by simp
-    thus ?thesis using True multiset_rel'.Zero by auto
+    thus ?thesis using True rel_multiset'.Zero by auto
   next
     case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
-    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "multiset_rel R M1 N1"
+    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
     using msed_rel_invL[OF less.prems[unfolded M]] by auto
-    have "multiset_rel' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
-    thus ?thesis using multiset_rel'.Plus[of R a b, OF R] unfolding M N by simp
+    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
+    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
   qed
 qed
 
-lemma multiset_rel_multiset_rel':
-"multiset_rel R M N = multiset_rel' R M N"
-using  multiset_rel_imp_multiset_rel' multiset_rel'_imp_multiset_rel by auto
+lemma rel_multiset_rel_multiset':
+"rel_multiset R M N = rel_multiset' R M N"
+using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
 
-(* The main end product for multiset_rel: inductive characterization *)
-theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] =
-         multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]]
+(* The main end product for rel_multiset: inductive characterization *)
+theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
+         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
 
 
 
@@ -1183,5 +1183,4 @@
   qed
 qed
 
-
 end
diff -r 03ff4d1e6784 -r 930409d43211 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 19 10:05:53 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 19 14:11:26 2013 +0100
@@ -678,7 +678,7 @@
 
     val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
 
-    fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
+    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
 
     fun maybe_define user_specified (b, rhs) lthy =
       let
@@ -703,7 +703,7 @@
       lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
 
     val map_bind_def =
-      (fn () => def_qualify (if Binding.is_empty map_b then mk_suffix_binding mapN else map_b),
+      (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
          map_rhs);
     val set_binds_defs =
       let
@@ -711,10 +711,10 @@
           (case try (nth set_bs) (i - 1) of
             SOME b => if Binding.is_empty b then get_b else K b
           | NONE => get_b) #> def_qualify;
-        val bs = if live = 1 then [set_name 1 (fn () => mk_suffix_binding setN)]
-          else map (fn i => set_name i (fn () => mk_suffix_binding (mk_setN i))) (1 upto live);
+        val bs = if live = 1 then [set_name 1 (fn () => mk_prefix_binding setN)]
+          else map (fn i => set_name i (fn () => mk_prefix_binding (mk_setN i))) (1 upto live);
       in bs ~~ set_rhss end;
-    val bd_bind_def = (fn () => def_qualify (mk_suffix_binding bdN), bd_rhs);
+    val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs);
 
     val ((((bnf_map_term, raw_map_def),
       (bnf_set_terms, raw_set_defs)),
@@ -861,7 +861,7 @@
       | SOME raw_rel => prep_term no_defs_lthy raw_rel);
 
     val rel_bind_def =
-      (fn () => def_qualify (if Binding.is_empty rel_b then mk_suffix_binding relN else rel_b),
+      (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
          rel_rhs);
 
     val wit_rhss =
@@ -873,8 +873,8 @@
     val nwits = length wit_rhss;
     val wit_binds_defs =
       let
-        val bs = if nwits = 1 then [fn () => def_qualify (mk_suffix_binding witN)]
-          else map (fn i => fn () => def_qualify (mk_suffix_binding (mk_witN i))) (1 upto nwits);
+        val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
+          else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
       in bs ~~ wit_rhss end;
 
     val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =