--- a/src/HOL/BNF/Examples/HFset.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/HFset.thy Wed Sep 26 10:01:00 2012 +0200
@@ -50,11 +50,11 @@
lemma hfset_ctor_rec:
"hfset_ctor_rec R (Fold hs) = R (map_fset <id, hfset_ctor_rec R> hs)"
-using hfset.ctor_recs unfolding Fold_def .
+using hfset.ctor_rec unfolding Fold_def .
(* The iterator has a simpler form: *)
lemma hfset_ctor_fold:
"hfset_ctor_fold R (Fold hs) = R (map_fset (hfset_ctor_fold R) hs)"
-using hfset.ctor_folds unfolding Fold_def .
+using hfset.ctor_fold unfolding Fold_def .
end
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Wed Sep 26 10:01:00 2012 +0200
@@ -177,7 +177,7 @@
theorem TTree_unfold:
"root (TTree_unfold rt ct b) = rt b"
"ccont (TTree_unfold rt ct b) = map_fset (id \<oplus> TTree_unfold rt ct) (ct b)"
-using Tree.dtor_unfolds[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol
+using Tree.dtor_unfold[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol
unfolding pre_Tree_map' fst_convol' snd_convol'
unfolding Tree_dtor_root_ccont by simp_all
@@ -194,7 +194,7 @@
theorem TTree_corec:
"root (TTree_corec rt ct b) = rt b"
"ccont (TTree_corec rt ct b) = map_fset (id \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)"
-using Tree.dtor_corecs[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol
+using Tree.dtor_corec[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol
unfolding pre_Tree_map' fst_convol' snd_convol'
unfolding Tree_dtor_root_ccont by simp_all
--- a/src/HOL/BNF/Examples/Lambda_Term.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy Wed Sep 26 10:01:00 2012 +0200
@@ -141,21 +141,21 @@
lemma trmrec_Var[simp]:
"trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.ctor_recs pre_trm_map(1) by simp
+unfolding trmrec_def Var_def trm.ctor_rec pre_trm_map(1) by simp
lemma trmrec_App[simp]:
"trmrec var app lam lt (App t1 t2) =
app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
-unfolding trmrec_def App_def trm.ctor_recs pre_trm_map(2) convol_def by simp
+unfolding trmrec_def App_def trm.ctor_rec pre_trm_map(2) convol_def by simp
lemma trmrec_Lam[simp]:
"trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
-unfolding trmrec_def Lam_def trm.ctor_recs pre_trm_map(3) convol_def by simp
+unfolding trmrec_def Lam_def trm.ctor_rec pre_trm_map(3) convol_def by simp
lemma trmrec_Lt[simp]:
"trmrec var app lam lt (Lt xts t) =
lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
-unfolding trmrec_def Lt_def trm.ctor_recs pre_trm_map(4) convol_def by simp
+unfolding trmrec_def Lt_def trm.ctor_rec pre_trm_map(4) convol_def by simp
definition
"sumJoinI4 f1 f2 f3 f4 \<equiv>
@@ -178,21 +178,21 @@
lemma trmfold_Var[simp]:
"trmfold var app lam lt (Var x) = var x"
-unfolding trmfold_def Var_def trm.ctor_folds pre_trm_map(1) by simp
+unfolding trmfold_def Var_def trm.ctor_fold pre_trm_map(1) by simp
lemma trmfold_App[simp]:
"trmfold var app lam lt (App t1 t2) =
app (trmfold var app lam lt t1) (trmfold var app lam lt t2)"
-unfolding trmfold_def App_def trm.ctor_folds pre_trm_map(2) by simp
+unfolding trmfold_def App_def trm.ctor_fold pre_trm_map(2) by simp
lemma trmfold_Lam[simp]:
"trmfold var app lam lt (Lam x t) = lam x (trmfold var app lam lt t)"
-unfolding trmfold_def Lam_def trm.ctor_folds pre_trm_map(3) by simp
+unfolding trmfold_def Lam_def trm.ctor_fold pre_trm_map(3) by simp
lemma trmfold_Lt[simp]:
"trmfold var app lam lt (Lt xts t) =
lt (map_fset (\<lambda> (x,t). (x,trmfold var app lam lt t)) xts) (trmfold var app lam lt t)"
-unfolding trmfold_def Lt_def trm.ctor_folds pre_trm_map(4) by simp
+unfolding trmfold_def Lt_def trm.ctor_fold pre_trm_map(4) by simp
subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
--- a/src/HOL/BNF/Examples/ListF.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/ListF.thy Wed Sep 26 10:01:00 2012 +0200
@@ -18,27 +18,27 @@
definition "Conss a as \<equiv> listF_ctor (Inr (a, as))"
lemma listF_map_NilF[simp]: "listF_map f NilF = NilF"
-unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_folds by simp
+unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_fold by simp
lemma listF_map_Conss[simp]:
"listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)"
-unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_folds by simp
+unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_fold by simp
lemma listF_set_NilF[simp]: "listF_set NilF = {}"
-unfolding listF_set_def NilF_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def
+unfolding listF_set_def NilF_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def
sum_set_defs pre_listF_map_def collect_def[abs_def] by simp
lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs"
-unfolding listF_set_def Conss_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def
+unfolding listF_set_def Conss_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def
sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp
lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()"
-unfolding NilF_def listF.ctor_folds pre_listF_map_def by simp
+unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp
lemma fold_sum_case_Conss:
"listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)"
-unfolding Conss_def listF.ctor_folds pre_listF_map_def by simp
+unfolding Conss_def listF.ctor_fold pre_listF_map_def by simp
(* familiar induction principle *)
lemma listF_induct:
--- a/src/HOL/BNF/Examples/Process.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/Process.thy Wed Sep 26 10:01:00 2012 +0200
@@ -135,7 +135,7 @@
lemma BX: "BX = Action ''a'' BX"
unfolding BX_def
-using process.unfolds(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
+using process.unfold(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
@@ -156,9 +156,9 @@
lemma X_Y_AX: "X = Choice AX Y" "Y = Action ''b'' X" "AX = Action ''a'' X"
unfolding X_def Y_def AX_def F_def
-using process.unfolds(2)[of isA x "pr" co c1 c2]
- process.unfolds(1)[of isA y "pr" co c1 c2]
- process.unfolds(1)[of isA ax "pr" co c1 c2]
+using process.unfold(2)[of isA x "pr" co c1 c2]
+ process.unfold(1)[of isA y "pr" co c1 c2]
+ process.unfold(1)[of isA ax "pr" co c1 c2]
unfolding Action_defs Choice_defs by simp_all
(* end product: *)
@@ -237,14 +237,14 @@
assumes "isACT sys T"
shows "solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
unfolding solution_def
-using process.unfolds(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
+using process.unfold(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
assms by simp
lemma solution_Choice:
assumes "\<not> isACT sys T"
shows "solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
unfolding solution_def
-using process.unfolds(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
+using process.unfold(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
assms by simp
lemma isACT_VAR:
--- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Wed Sep 26 10:01:00 2012 +0200
@@ -22,11 +22,11 @@
definition "tll as \<equiv> snd (stream_dtor as)"
lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding hdd_def pair_fun_def stream.dtor_unfolds by simp
+unfolding hdd_def pair_fun_def stream.dtor_unfold by simp
lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding tll_def pair_fun_def stream.dtor_unfolds by simp
+unfolding tll_def pair_fun_def stream.dtor_unfold by simp
(* infinite trees: *)
coinductive infiniteTr where
--- a/src/HOL/BNF/Examples/TreeFI.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy Wed Sep 26 10:01:00 2012 +0200
@@ -31,10 +31,10 @@
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp
+unfolding lab_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp
+unfolding sub_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
(* Tree reverse:*)
definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> lrev o sub)"
--- a/src/HOL/BNF/Examples/TreeFsetI.thy Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy Wed Sep 26 10:01:00 2012 +0200
@@ -28,10 +28,10 @@
unfolding lab_def sub_def by simp
lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp
+unfolding lab_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp
lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp
+unfolding sub_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp
(* tree map (contrived example): *)
definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)"
--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:01:00 2012 +0200
@@ -58,10 +58,10 @@
val map_id_of_bnf: BNF -> thm
val map_wppull_of_bnf: BNF -> thm
val map_wpull_of_bnf: BNF -> thm
- val rel_as_srel_of_bnf: BNF -> thm
val rel_def_of_bnf: BNF -> thm
val rel_eq_of_bnf: BNF -> thm
val rel_flip_of_bnf: BNF -> thm
+ val rel_srel_of_bnf: BNF -> thm
val set_bd_of_bnf: BNF -> thm list
val set_defs_of_bnf: BNF -> thm list
val set_natural'_of_bnf: BNF -> thm list
@@ -186,9 +186,9 @@
map_comp': thm lazy,
map_id': thm lazy,
map_wppull: thm lazy,
- rel_as_srel: thm lazy,
rel_eq: thm lazy,
rel_flip: thm lazy,
+ rel_srel: thm lazy,
set_natural': thm lazy list,
srel_cong: thm lazy,
srel_mono: thm lazy,
@@ -199,7 +199,7 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
- map_comp' map_id' map_wppull rel_as_srel rel_eq rel_flip set_natural' srel_cong srel_mono
+ map_comp' map_id' map_wppull rel_eq rel_flip rel_srel set_natural' srel_cong srel_mono
srel_Id srel_Gr srel_converse srel_O = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
@@ -211,9 +211,9 @@
map_comp' = map_comp',
map_id' = map_id',
map_wppull = map_wppull,
- rel_as_srel = rel_as_srel,
rel_eq = rel_eq,
rel_flip = rel_flip,
+ rel_srel = rel_srel,
set_natural' = set_natural',
srel_cong = srel_cong,
srel_mono = srel_mono,
@@ -233,9 +233,9 @@
map_comp',
map_id',
map_wppull,
- rel_as_srel,
rel_eq,
rel_flip,
+ rel_srel,
set_natural',
srel_cong,
srel_mono,
@@ -253,9 +253,9 @@
map_comp' = Lazy.map f map_comp',
map_id' = Lazy.map f map_id',
map_wppull = Lazy.map f map_wppull,
- rel_as_srel = Lazy.map f rel_as_srel,
rel_eq = Lazy.map f rel_eq,
rel_flip = Lazy.map f rel_flip,
+ rel_srel = Lazy.map f rel_srel,
set_natural' = map (Lazy.map f) set_natural',
srel_cong = Lazy.map f srel_cong,
srel_mono = Lazy.map f srel_mono,
@@ -374,10 +374,10 @@
val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
-val rel_as_srel_of_bnf = Lazy.force o #rel_as_srel o #facts o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
+val rel_srel_of_bnf = Lazy.force o #rel_srel o #facts o rep_bnf;
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
@@ -509,9 +509,9 @@
val map_comp'N = "map_comp'";
val map_congN = "map_cong";
val map_wpullN = "map_wpull";
-val rel_as_srelN = "rel_as_srel";
val rel_eqN = "rel_eq";
val rel_flipN = "rel_flip";
+val rel_srelN = "rel_srel";
val set_naturalN = "set_natural";
val set_natural'N = "set_natural'";
val set_bdN = "set_bd";
@@ -1115,13 +1115,13 @@
val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
val mem_Collect_etc' = @{thms fst_conv mem_Collect_eq pair_in_Id_conv snd_conv};
- fun mk_rel_as_srel () =
+ fun mk_rel_srel () =
unfold_thms lthy mem_Collect_etc
(funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq)
RS eqset_imp_iff_pair RS sym)
|> Drule.zero_var_indexes;
- val rel_as_srel = Lazy.lazy mk_rel_as_srel;
+ val rel_srel = Lazy.lazy mk_rel_srel;
fun mk_rel_eq () =
unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
@@ -1146,7 +1146,7 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
- in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_eq rel_flip set_natural'
+ in_mono in_srel map_comp' map_id' map_wppull rel_eq rel_flip rel_srel set_natural'
srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1193,9 +1193,9 @@
[(map_comp'N, [Lazy.force (#map_comp' facts)]),
(map_congN, [#map_cong axioms]),
(map_id'N, [Lazy.force (#map_id' facts)]),
- (rel_as_srelN, [Lazy.force (#rel_as_srel facts)]),
(rel_eqN, [Lazy.force (#rel_eq facts)]),
(rel_flipN, [Lazy.force (#rel_flip facts)]),
+ (rel_srelN, [Lazy.force (#rel_srel facts)]),
(set_natural'N, map Lazy.force (#set_natural' facts)),
(srel_O_GrN, srel_O_Grs),
(srel_IdN, [Lazy.force (#srel_Id facts)]),
--- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:01:00 2012 +0200
@@ -23,34 +23,30 @@
val coN: string
val coinductN: string
val corecN: string
- val corecsN: string
val ctorN: string
val ctor_dtorN: string
- val ctor_dtor_unfoldsN: string
- val ctor_dtor_corecsN: string
+ val ctor_dtor_corecN: string
+ val ctor_dtor_unfoldN: string
val ctor_exhaustN: string
val ctor_induct2N: string
val ctor_inductN: string
val ctor_injectN: string
val ctor_foldN: string
val ctor_fold_uniqueN: string
- val ctor_foldsN: string
val ctor_mapN: string
val ctor_map_uniqueN: string
val ctor_recN: string
- val ctor_recsN: string
val ctor_relN: string
val ctor_set_inclN: string
val ctor_set_set_inclN: string
val ctor_srelN: string
- val disc_unfold_iffsN: string
- val disc_unfoldsN: string
- val disc_corec_iffsN: string
- val disc_corecsN: string
+ val disc_unfoldN: string
+ val disc_unfold_iffN: string
+ val disc_corecN: string
+ val disc_corec_iffN: string
val dtorN: string
val dtor_coinductN: string
val dtor_corecN: string
- val dtor_corecsN: string
val dtor_ctorN: string
val dtor_exhaustN: string
val dtor_injectN: string
@@ -67,31 +63,27 @@
val dtor_strong_coinductN: string
val dtor_unfoldN: string
val dtor_unfold_uniqueN: string
- val dtor_unfoldsN: string
val exhaustN: string
val foldN: string
- val foldsN: string
val hsetN: string
val hset_recN: string
val inductN: string
val injectN: string
val isNodeN: string
val lsbisN: string
+ val mapN: string
val map_uniqueN: string
- val mapsN: string
val min_algN: string
val morN: string
val nchotomyN: string
val recN: string
- val recsN: string
val rel_injectN: string
val rel_distinctN: string
val rvN: string
- val sel_corecsN: string
- val sel_relsN: string
- val sel_unfoldsN: string
+ val sel_corecN: string
val set_inclN: string
val set_set_inclN: string
+ val sel_unfoldN: string
val setsN: string
val simpsN: string
val strTN: string
@@ -100,7 +92,6 @@
val sum_bdN: string
val sum_bdTN: string
val unfoldN: string
- val unfoldsN: string
val uniqueN: string
(* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
@@ -182,21 +173,16 @@
val algN = "alg"
val IITN = "IITN"
val foldN = "fold"
-val foldsN = foldN ^ "s"
val unfoldN = unN ^ foldN
-val unfoldsN = unfoldN ^ "s"
val uniqueN = "_unique"
val simpsN = "simps"
val ctorN = "ctor"
val dtorN = "dtor"
val ctor_foldN = ctorN ^ "_" ^ foldN
-val ctor_foldsN = ctor_foldN ^ "s"
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
-val dtor_unfoldsN = dtor_unfoldN ^ "s"
val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
-val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
-val mapsN = mapN ^ "s"
+val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
val ctor_mapN = ctorN ^ "_" ^ mapN
val dtor_mapN = dtorN ^ "_" ^ mapN
val map_uniqueN = mapN ^ uniqueN
@@ -222,14 +208,10 @@
val str_initN = "str_init"
val recN = "rec"
-val recsN = recN ^ "s"
val corecN = coN ^ recN
-val corecsN = corecN ^ "s"
val ctor_recN = ctorN ^ "_" ^ recN
-val ctor_recsN = ctor_recN ^ "s"
val dtor_corecN = dtorN ^ "_" ^ corecN
-val dtor_corecsN = dtor_corecN ^ "s"
-val ctor_dtor_corecsN = ctorN ^ "_" ^ dtor_corecN ^ "s"
+val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
val ctor_dtorN = ctorN ^ "_" ^ dtorN
val dtor_ctorN = dtorN ^ "_" ^ ctorN
@@ -266,20 +248,19 @@
val caseN = "case"
val discN = "disc"
-val disc_unfoldsN = discN ^ "_" ^ unfoldsN
-val disc_corecsN = discN ^ "_" ^ corecsN
-val iffsN = "_iffs"
-val disc_unfold_iffsN = discN ^ "_" ^ unfoldN ^ iffsN
-val disc_corec_iffsN = discN ^ "_" ^ corecN ^ iffsN
+val disc_unfoldN = discN ^ "_" ^ unfoldN
+val disc_corecN = discN ^ "_" ^ corecN
+val iffN = "_iff"
+val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
+val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
val distinctN = "distinct"
val rel_distinctN = relN ^ "_" ^ distinctN
val injectN = "inject"
val rel_injectN = relN ^ "_" ^ injectN
val relsN = relN ^ "s"
val selN = "sel"
-val sel_relsN = selN ^ "_" ^ relsN
-val sel_unfoldsN = selN ^ "_" ^ unfoldsN
-val sel_corecsN = selN ^ "_" ^ corecsN
+val sel_unfoldN = selN ^ "_" ^ unfoldN
+val sel_corecN = selN ^ "_" ^ corecN
val mk_common_name = space_implode "_";
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:01:00 2012 +0200
@@ -551,7 +551,7 @@
join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
val notes =
- [(mapsN, map_thms, code_simp_attrs),
+ [(mapN, map_thms, code_simp_attrs),
(rel_distinctN, rel_distinct_thms, code_simp_attrs),
(rel_injectN, rel_inject_thms, code_simp_attrs),
(setsN, flat set_thmss, code_simp_attrs)]
@@ -818,8 +818,8 @@
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (foldsN, fold_thmss, K (code_simp_attrs)),
- (recsN, rec_thmss, K (code_simp_attrs)),
+ (foldN, fold_thmss, K (code_simp_attrs)),
+ (recN, rec_thmss, K (code_simp_attrs)),
(simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
map3 (fn b => fn Type (T_name, _) => fn thms =>
@@ -1076,16 +1076,16 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
- (corecsN, corec_thmss, []),
- (disc_corec_iffsN, disc_corec_iff_thmss, simp_attrs),
- (disc_corecsN, disc_corec_thmss, simp_attrs),
- (disc_unfold_iffsN, disc_unfold_iff_thmss, simp_attrs),
- (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
- (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
- (sel_corecsN, sel_corec_thmss, simp_attrs),
+ (corecN, corec_thmss, []),
+ (disc_corecN, disc_corec_thmss, simp_attrs),
+ (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
+ (disc_unfoldN, disc_unfold_thmss, simp_attrs),
+ (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+ (sel_corecN, sel_corec_thmss, simp_attrs),
+ (sel_unfoldN, sel_unfold_thmss, simp_attrs),
(simpsN, simp_thmss, []),
(strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
- (unfoldsN, unfold_thmss, [])]
+ (unfoldN, unfold_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>
SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:01:00 2012 +0200
@@ -2980,16 +2980,16 @@
val notes =
[(ctor_dtorN, ctor_dtor_thms),
- (ctor_dtor_corecsN, ctor_dtor_corec_thms),
- (ctor_dtor_unfoldsN, ctor_dtor_unfold_thms),
+ (ctor_dtor_corecN, ctor_dtor_corec_thms),
+ (ctor_dtor_unfoldN, ctor_dtor_unfold_thms),
(ctor_exhaustN, ctor_exhaust_thms),
(ctor_injectN, ctor_inject_thms),
- (dtor_corecsN, dtor_corec_thms),
+ (dtor_corecN, dtor_corec_thms),
(dtor_ctorN, dtor_ctor_thms),
(dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms),
- (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
- (dtor_unfoldsN, dtor_unfold_thms)]
+ (dtor_unfoldN, dtor_unfold_thms),
+ (dtor_unfold_uniqueN, dtor_unfold_unique_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Sep 26 10:01:00 2012 +0200
@@ -1815,10 +1815,10 @@
val notes =
[(ctor_dtorN, ctor_dtor_thms),
(ctor_exhaustN, ctor_exhaust_thms),
+ (ctor_foldN, ctor_fold_thms),
(ctor_fold_uniqueN, ctor_fold_unique_thms),
- (ctor_foldsN, ctor_fold_thms),
(ctor_injectN, ctor_inject_thms),
- (ctor_recsN, ctor_rec_thms),
+ (ctor_recN, ctor_rec_thms),
(dtor_ctorN, dtor_ctor_thms),
(dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms)]
--- a/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:01:00 2012 +0200
@@ -35,9 +35,9 @@
fun mk_unN 1 1 suf = unN ^ suf
| mk_unN _ l suf = unN ^ suf ^ string_of_int l;
+val caseN = "case";
val case_congN = "case_cong";
-val case_eqN = "case_eq";
-val casesN = "cases";
+val case_convN = "case_conv";
val collapseN = "collapse";
val disc_excludeN = "disc_exclude";
val disc_exhaustN = "disc_exhaust";
@@ -382,7 +382,7 @@
end;
val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
- disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms) =
+ disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
if no_dests then
([], [], [], [], [], [], [], [], [], [])
else
@@ -539,18 +539,18 @@
|> Proof_Context.export names_lthy lthy
end;
- val case_eq_thms =
+ val case_conv_thms =
let
fun mk_body f usels = Term.list_comb (f, usels);
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
in
[Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_eq_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
+ mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
|> Proof_Context.export names_lthy lthy
end;
in
(all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
- [disc_exhaust_thm], collapse_thms, expand_thms, case_eq_thms)
+ [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
end;
val (case_cong_thm, weak_case_cong_thm) =
@@ -601,9 +601,9 @@
val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
val notes =
- [(case_congN, [case_cong_thm], []),
- (case_eqN, case_eq_thms, []),
- (casesN, case_thms, simp_attrs),
+ [(caseN, case_thms, simp_attrs),
+ (case_congN, [case_cong_thm], []),
+ (case_convN, case_conv_thms, []),
(collapseN, collapse_thms, simp_attrs),
(discsN, disc_thms, simp_attrs),
(disc_excludeN, disc_exclude_thms, []),
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Sep 26 10:01:00 2012 +0200
@@ -9,7 +9,7 @@
sig
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
val mk_case_cong_tac: thm -> thm list -> tactic
- val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
+ val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
tactic
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
@@ -95,7 +95,7 @@
ks ms disc_excludesss disc_excludesss' uncollapses)) 1
end;
-fun mk_case_eq_tac ctxt n uexhaust cases discss' selss =
+fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
(rtac uexhaust THEN'
EVERY' (map3 (fn casex => fn if_discs => fn sels =>
EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])