# HG changeset patch # User blanchet # Date 1348646460 -7200 # Node ID 55e798614c452e25966319d3bec63930fd2846f5 # Parent c958f282b3822d43419870bc3fed097ad293f8c0 tweaked theorem names (in particular, dropped s's) diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/HFset.thy --- 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 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 diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy --- 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 \ TTree_unfold rt ct) (ct b)" -using Tree.dtor_unfolds[of "" b] unfolding Tree_unfold_unfold fst_convol snd_convol +using Tree.dtor_unfold[of "" 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 \ ([[id, TTree_corec rt ct]]) ) (ct b)" -using Tree.dtor_corecs[of "" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol +using Tree.dtor_corec[of "" 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 diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/Lambda_Term.thy --- 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 (\ (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 \ @@ -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 (\ (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: *} diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/ListF.thy --- 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 \ 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} \ 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: diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/Process.thy --- 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 "\ P. True" "()" "\ P. ''a''" "\ P. P"] by simp +using process.unfold(1)[of "\ P. True" "()" "\ P. ''a''" "\ 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 "\ 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: diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/Stream.thy --- 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 \ snd (stream_dtor as)" lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \ 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 \ g) t) = stream_dtor_unfold (f \ 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 diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/TreeFI.thy --- 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 \ g \ \x. (f x, g x)" lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \ 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 \ g) t) = listF_map (treeFI_dtor_unfold (f \ 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 \ treeFI_dtor_unfold (lab \ lrev o sub)" diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/TreeFsetI.thy --- 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 \ 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 \ g) t) = map_fset (treeFsetI_dtor_unfold (f \ 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 \ treeFsetI_dtor_unfold (f o lab \ sub)" diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_def.ML --- 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)]), diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_fp.ML --- 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 "_"; diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_fp_sugar.ML --- 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), diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_gfp.ML --- 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 => diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_lfp.ML --- 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)] diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_wrap.ML --- 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, []), diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Tools/bnf_wrap_tactics.ML --- 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])