use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package
--- 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
--- 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
--- 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]
--- 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
--- 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)) =