# HG changeset patch # User blanchet # Date 1347132631 -7200 # Node ID cbe8c859817c4b8fc0f796c325a1e297e3da3edf # Parent 6d8d5fe9f3a205b41c95ff4d3e9385e0818ad7aa for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Sat Sep 08 21:30:31 2012 +0200 @@ -50,11 +50,11 @@ lemma hfset_fld_rec: "hfset_fld_rec R (Fold hs) = R (map_fset hs)" -using hfset.fld_rec unfolding Fold_def . +using hfset.fld_recs unfolding Fold_def . (* The iterator has a simpler form: *) lemma hfset_fld_iter: "hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)" -using hfset.fld_iter unfolding Fold_def . +using hfset.fld_iters unfolding Fold_def . end diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:30:31 2012 +0200 @@ -177,7 +177,7 @@ theorem TTree_coit: "root (TTree_coit rt ct b) = rt b" "ccont (TTree_coit rt ct b) = map_fset (id \ TTree_coit rt ct) (ct b)" -using Tree.unf_coiter[of "" b] unfolding Tree_coit_coit fst_convol snd_convol +using Tree.unf_coiters[of "" b] unfolding Tree_coit_coit fst_convol snd_convol unfolding pre_Tree_map' fst_convol' snd_convol' unfolding Tree_unf_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.unf_corec[of "" b] unfolding Tree_unf_corec_corec fst_convol snd_convol +using Tree.unf_corecs[of "" b] unfolding Tree_unf_corec_corec fst_convol snd_convol unfolding pre_Tree_map' fst_convol' snd_convol' unfolding Tree_unf_root_ccont by simp_all diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:30:31 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.fld_rec pre_trm_map(1) by simp +unfolding trmrec_def Var_def trm.fld_recs 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.fld_rec pre_trm_map(2) convol_def by simp +unfolding trmrec_def App_def trm.fld_recs 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.fld_rec pre_trm_map(3) convol_def by simp +unfolding trmrec_def Lam_def trm.fld_recs 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.fld_rec pre_trm_map(4) convol_def by simp +unfolding trmrec_def Lt_def trm.fld_recs pre_trm_map(4) convol_def by simp definition "sumJoinI4 f1 f2 f3 f4 \ @@ -178,21 +178,21 @@ lemma trmiter_Var[simp]: "trmiter var app lam lt (Var x) = var x" -unfolding trmiter_def Var_def trm.fld_iter pre_trm_map(1) by simp +unfolding trmiter_def Var_def trm.fld_iters pre_trm_map(1) by simp lemma trmiter_App[simp]: "trmiter var app lam lt (App t1 t2) = app (trmiter var app lam lt t1) (trmiter var app lam lt t2)" -unfolding trmiter_def App_def trm.fld_iter pre_trm_map(2) by simp +unfolding trmiter_def App_def trm.fld_iters pre_trm_map(2) by simp lemma trmiter_Lam[simp]: "trmiter var app lam lt (Lam x t) = lam x (trmiter var app lam lt t)" -unfolding trmiter_def Lam_def trm.fld_iter pre_trm_map(3) by simp +unfolding trmiter_def Lam_def trm.fld_iters pre_trm_map(3) by simp lemma trmiter_Lt[simp]: "trmiter var app lam lt (Lt xts t) = lt (map_fset (\ (x,t). (x,trmiter var app lam lt t)) xts) (trmiter var app lam lt t)" -unfolding trmiter_def Lt_def trm.fld_iter pre_trm_map(4) by simp +unfolding trmiter_def Lt_def trm.fld_iters pre_trm_map(4) by simp subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *} diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Sat Sep 08 21:30:31 2012 +0200 @@ -18,27 +18,27 @@ definition "Conss a as \ listF_fld (Inr (a, as))" lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" -unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iter by simp +unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iters 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.fld_iter by simp +unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iters by simp lemma listF_set_NilF[simp]: "listF_set NilF = {}" -unfolding listF_set_def NilF_def listF.fld_iter pre_listF_set1_def pre_listF_set2_def +unfolding listF_set_def NilF_def listF.fld_iters 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.fld_iter pre_listF_set1_def pre_listF_set2_def +unfolding listF_set_def Conss_def listF.fld_iters 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 iter_sum_case_NilF: "listF_fld_iter (sum_case f g) NilF = f ()" -unfolding NilF_def listF.fld_iter pre_listF_map_def by simp +unfolding NilF_def listF.fld_iters pre_listF_map_def by simp lemma iter_sum_case_Conss: "listF_fld_iter (sum_case f g) (Conss y ys) = g (y, listF_fld_iter (sum_case f g) ys)" -unfolding Conss_def listF.fld_iter pre_listF_map_def by simp +unfolding Conss_def listF.fld_iters pre_listF_map_def by simp (* familiar induction principle *) lemma listF_induct: diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:30:31 2012 +0200 @@ -326,7 +326,7 @@ let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2" assume isA: "isA P" have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))" - using process.unf_coiter[of ?s P] + using process.unf_coiters[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] pre_process_map id_apply pcoiter_def . thus "?f P = Action (pr P) (?f (co P))" @@ -336,7 +336,7 @@ let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2" assume isA: "\ isA P" and isC: "isC P" have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))" - using process.unf_coiter[of ?s P] + using process.unf_coiters[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] pre_process_map id_apply pcoiter_def . thus "?f P = Choice (?f (c1 P)) (?f (c2 P))" @@ -367,14 +367,14 @@ proof(cases "co P") case (Inl p) have "process_unf (process_unf_corec ?s P) = Inl (pr P, p)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] pre_process_map id_apply pcorec_def Inl by simp thus ?thesis unfolding Inl pcorec_def Action_def using process.fld_unf by (simp, metis) next case (Inr Q) have "process_unf (process_unf_corec ?s P) = Inl (pr P, ?f Q)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] pre_process_map id_apply pcorec_def Inr by simp thus ?thesis unfolding Inr pcorec_def Action_def using process.fld_unf by (simp, metis) @@ -405,14 +405,14 @@ proof(cases "c2 P") case (Inl p2) note c2 = Inl have "process_unf (process_unf_corec ?s P) = Inr (p1, p2)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] pre_process_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) next case (Inr Q2) note c2 = Inr have "process_unf (process_unf_corec ?s P) = Inr (p1, ?f Q2)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] pre_process_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) @@ -423,14 +423,14 @@ proof(cases "c2 P") case (Inl p2) note c2 = Inl have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, p2)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] pre_process_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) next case (Inr Q2) note c2 = Inr have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, ?f Q2)" - using process.unf_corec[of ?s P] + using process.unf_corecs[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] pre_process_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:30:31 2012 +0200 @@ -19,11 +19,11 @@ definition "tll as \ snd (stream_unf as)" lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \ g) t) = f t" -unfolding hdd_def pair_fun_def stream.unf_coiter by simp +unfolding hdd_def pair_fun_def stream.unf_coiters by simp lemma coiter_pair_fun_tll[simp]: "tll (stream_unf_coiter (f \ g) t) = stream_unf_coiter (f \ g) (g t)" -unfolding tll_def pair_fun_def stream.unf_coiter by simp +unfolding tll_def pair_fun_def stream.unf_coiters by simp (* infinite trees: *) coinductive infiniteTr where diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:30:31 2012 +0200 @@ -31,10 +31,10 @@ "f \ g \ \x. (f x, g x)" lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \ g) t) = f t" -unfolding lab_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp +unfolding lab_def pair_fun_def treeFI.unf_coiters pre_treeFI_map_def by simp lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \ g) t) = listF_map (treeFI_unf_coiter (f \ g)) (g t)" -unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp +unfolding sub_def pair_fun_def treeFI.unf_coiters pre_treeFI_map_def by simp (* Tree reverse:*) definition "trev \ treeFI_unf_coiter (lab \ lrev o sub)" diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:30:31 2012 +0200 @@ -27,10 +27,10 @@ unfolding lab_def sub_def by simp lemma coiter_pair_fun_lab: "lab (treeFsetI_unf_coiter (f \ g) t) = f t" -unfolding lab_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp +unfolding lab_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp lemma coiter_pair_fun_sub: "sub (treeFsetI_unf_coiter (f \ g) t) = map_fset (treeFsetI_unf_coiter (f \ g)) (g t)" -unfolding sub_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp +unfolding sub_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp (* tree map (contrived example): *) definition "tmap f \ treeFsetI_unf_coiter (f o lab \ sub)" diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:30:31 2012 +0200 @@ -28,7 +28,9 @@ val fld_inductN: string val fld_injectN: string val fld_iterN: string + val fld_itersN: string val fld_recN: string + val fld_recsN: string val fld_unfN: string val hsetN: string val hset_recN: string @@ -59,7 +61,9 @@ val unf_coinductN: string val unf_coinduct_uptoN: string val unf_coiterN: string + val unf_coitersN: string val unf_corecN: string + val unf_corecsN: string val unf_exhaustN: string val unf_fldN: string val unf_injectN: string @@ -146,7 +150,9 @@ val fldN = "fld" val unfN = "unf" val fld_iterN = fldN ^ "_" ^ iterN +val fld_itersN = fld_iterN ^ "s" val unf_coiterN = unfN ^ "_" ^ coiterN +val unf_coitersN = unf_coiterN ^ "s" val fld_iter_uniqueN = fld_iterN ^ uniqueN val unf_coiter_uniqueN = unf_coiterN ^ uniqueN val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN @@ -172,7 +178,9 @@ val recN = "rec" val corecN = coN ^ recN val fld_recN = fldN ^ "_" ^ recN +val fld_recsN = fld_recN ^ "s" val unf_corecN = unfN ^ "_" ^ corecN +val unf_corecsN = unf_corecN ^ "s" val fld_unfN = fldN ^ "_" ^ unfN val unf_fldN = unfN ^ "_" ^ fldN diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Sat Sep 08 21:30:31 2012 +0200 @@ -2984,9 +2984,9 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(unf_coiterN, coiter_thms), + [(unf_coitersN, coiter_thms), (unf_coiter_uniqueN, coiter_unique_thms), - (unf_corecN, corec_thms), + (unf_corecsN, corec_thms), (unf_fldN, unf_fld_thms), (fld_unfN, fld_unf_thms), (unf_injectN, unf_inject_thms), diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Sat Sep 08 21:21:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Sat Sep 08 21:30:31 2012 +0200 @@ -1808,9 +1808,9 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(fld_iterN, iter_thms), + [(fld_itersN, iter_thms), (fld_iter_uniqueN, iter_unique_thms), - (fld_recN, rec_thms), + (fld_recsN, rec_thms), (unf_fldN, unf_fld_thms), (fld_unfN, fld_unf_thms), (unf_injectN, unf_inject_thms),