# HG changeset patch # User blanchet # Date 1347131067 -7200 # Node ID a6260b4fb4103aab9cf5cf7c16c473c3179d4502 # Parent c28dd8326f9a3d6c24b991b6ea63ab02101a10ec imported patch debugging diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:04:27 2012 +0200 @@ -24,14 +24,14 @@ (* These should be eventually inferred from compositionality *) -lemma TreeBNF_map: -"TreeBNF_map f (n, as) = (n, map_fset (id \ f) as)" -unfolding TreeBNF_map_def id_apply +lemma pre_Tree_map: +"pre_Tree_map f (n, as) = (n, map_fset (id \ f) as)" +unfolding pre_Tree_map_def id_apply sum_map_def by simp -lemma TreeBNF_map': -"TreeBNF_map f n_as = (fst n_as, map_fset (id \ f) (snd n_as))" -using TreeBNF_map by(cases n_as, simp) +lemma pre_Tree_map': +"pre_Tree_map f n_as = (fst n_as, map_fset (id \ f) (snd n_as))" +using pre_Tree_map by(cases n_as, simp) definition @@ -40,8 +40,8 @@ (\ tr1. Inr tr1 \ fset as1 \ (\ tr2. Inr tr2 \ fset as2 \ \ tr1 tr2)) \ (\ tr2. Inr tr2 \ fset as2 \ (\ tr1. Inr tr1 \ fset as1 \ \ tr1 tr2))" -lemma TreeBNF_pred: "TreeBNF_pred \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" -unfolding llift2_def TreeBNF.pred_unfold +lemma pre_Tree_pred: "pre_Tree_pred \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" +unfolding llift2_def pre_Tree.pred_unfold apply (auto split: sum.splits) apply (metis sumE) apply (metis sumE) @@ -132,11 +132,11 @@ shows "tr1 = tr2" apply(rule mp[OF Tree.pred_coinduct[of \ tr1 tr2] phi]) proof clarify fix tr1 tr2 assume \: "\ tr1 tr2" - show "TreeBNF_pred \ (Tree_unf tr1) (Tree_unf tr2)" + show "pre_Tree_pred \ (Tree_unf tr1) (Tree_unf tr2)" apply(cases rule: Tree.fld_exhaust[of tr1], cases rule: Tree.fld_exhaust[of tr2]) apply (simp add: Tree.unf_fld) apply(case_tac x, case_tac xa, simp) - unfolding TreeBNF_pred apply(rule NNode) using \ unfolding NNode_def by simp + unfolding pre_Tree_pred apply(rule NNode) using \ unfolding NNode_def by simp qed theorem TTree_coind[elim, consumes 1, case_names LLift]: @@ -178,7 +178,7 @@ "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 -unfolding TreeBNF_map' fst_convol' snd_convol' +unfolding pre_Tree_map' fst_convol' snd_convol' unfolding Tree_unf_root_ccont by simp_all (* Corecursion, stronger than coiteration *) @@ -195,7 +195,7 @@ "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 -unfolding TreeBNF_map' fst_convol' snd_convol' +unfolding pre_Tree_map' fst_convol' snd_convol' unfolding Tree_unf_root_ccont by simp_all diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:04:27 2012 +0200 @@ -22,26 +22,26 @@ subsection{* Set and map *} -lemma trmBNF_set2_Lt: "trmBNF_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \ {t}" -unfolding trmBNF_set2_def sum_set_defs prod_set_defs collect_def[abs_def] +lemma pre_trm_set2_Lt: "pre_trm_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \ {t}" +unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def] by auto -lemma trmBNF_set2_Var: "\x. trmBNF_set2 (Inl x) = {}" -and trmBNF_set2_App: -"\t1 t2. trmBNF_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}" -and trmBNF_set2_Lam: -"\x t. trmBNF_set2 (Inr (Inr (Inl (x, t)))) = {t}" -unfolding trmBNF_set2_def sum_set_defs prod_set_defs collect_def[abs_def] +lemma pre_trm_set2_Var: "\x. pre_trm_set2 (Inl x) = {}" +and pre_trm_set2_App: +"\t1 t2. pre_trm_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}" +and pre_trm_set2_Lam: +"\x t. pre_trm_set2 (Inr (Inr (Inl (x, t)))) = {t}" +unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def] by auto -lemma trmBNF_map: -"\ a1. trmBNF_map f1 f2 (Inl a1) = Inl (f1 a1)" -"\ a2 b2. trmBNF_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))" -"\ a1 a2. trmBNF_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))" +lemma pre_trm_map: +"\ a1. pre_trm_map f1 f2 (Inl a1) = Inl (f1 a1)" +"\ a2 b2. pre_trm_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))" +"\ a1 a2. pre_trm_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))" "\ a1a2s a2. - trmBNF_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) = + pre_trm_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) = Inr (Inr (Inr (map_fset (\ (a1', a2'). (f1 a1', f2 a2')) a1a2s, f2 a2)))" -unfolding trmBNF_map_def collect_def[abs_def] map_pair_def by auto +unfolding pre_trm_map_def collect_def[abs_def] map_pair_def by auto subsection{* Constructors *} @@ -87,7 +87,7 @@ shows "phi t" proof(induct rule: trm.fld_induct) fix u :: "'a + 'a trm \ 'a trm + 'a \ 'a trm + ('a \ 'a trm) fset \ 'a trm" - assume IH: "\t. t \ trmBNF_set2 u \ phi t" + assume IH: "\t. t \ pre_trm_set2 u \ phi t" show "phi (trm_fld u)" proof(cases u) case (Inl x) @@ -99,7 +99,7 @@ case (Inl t1t2) obtain t1 t2 where t1t2: "t1t2 = (t1,t2)" by (cases t1t2, blast) show ?thesis unfolding Inr1 Inl t1t2 App_def[symmetric] apply(rule App) - using IH unfolding Inr1 Inl trmBNF_set2_App t1t2 fst_conv snd_conv by blast+ + using IH unfolding Inr1 Inl pre_trm_set2_App t1t2 fst_conv snd_conv by blast+ next case (Inr uuu) note Inr2 = Inr show ?thesis @@ -107,12 +107,12 @@ case (Inl xt) obtain x t where xt: "xt = (x,t)" by (cases xt, blast) show ?thesis unfolding Inr1 Inr2 Inl xt Lam_def[symmetric] apply(rule Lam) - using IH unfolding Inr1 Inr2 Inl trmBNF_set2_Lam xt by blast + using IH unfolding Inr1 Inr2 Inl pre_trm_set2_Lam xt by blast next case (Inr xts_t) obtain xts t where xts_t: "xts_t = (xts,t)" by (cases xts_t, blast) show ?thesis unfolding Inr1 Inr2 Inr xts_t Lt_def[symmetric] apply(rule Lt) using IH - unfolding Inr1 Inr2 Inr trmBNF_set2_Lt xts_t fset_fset_member image_def by auto + unfolding Inr1 Inr2 Inr pre_trm_set2_Lt xts_t fset_fset_member image_def by auto qed qed qed @@ -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 trmBNF_map(1) by simp +unfolding trmrec_def Var_def trm.fld_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.fld_rec trmBNF_map(2) convol_def by simp +unfolding trmrec_def App_def trm.fld_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.fld_rec trmBNF_map(3) convol_def by simp +unfolding trmrec_def Lam_def trm.fld_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.fld_rec trmBNF_map(4) convol_def by simp +unfolding trmrec_def Lt_def trm.fld_rec 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 trmBNF_map(1) by simp +unfolding trmiter_def Var_def trm.fld_iter 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 trmBNF_map(2) by simp +unfolding trmiter_def App_def trm.fld_iter 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 trmBNF_map(3) by simp +unfolding trmiter_def Lam_def trm.fld_iter 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 trmBNF_map(4) by simp +unfolding trmiter_def Lt_def trm.fld_iter pre_trm_map(4) by simp subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *} diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Sat Sep 08 21:04:27 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 listFBNF_map_def NilF_def listF.fld_iter by simp +unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iter by simp lemma listF_map_Conss[simp]: "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" -unfolding listF_map_def listFBNF_map_def Conss_def listF.fld_iter by simp +unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iter by simp lemma listF_set_NilF[simp]: "listF_set NilF = {}" -unfolding listF_set_def NilF_def listF.fld_iter listFBNF_set1_def listFBNF_set2_def - sum_set_defs listFBNF_map_def collect_def[abs_def] by simp +unfolding listF_set_def NilF_def listF.fld_iter 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 listFBNF_set1_def listFBNF_set2_def - sum_set_defs prod_set_defs listFBNF_map_def collect_def[abs_def] by simp +unfolding listF_set_def Conss_def listF.fld_iter 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 listFBNF_map_def by simp +unfolding NilF_def listF.fld_iter 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 listFBNF_map_def by simp +unfolding Conss_def listF.fld_iter pre_listF_map_def by simp (* familiar induction principle *) lemma listF_induct: @@ -47,7 +47,7 @@ shows "P xs" proof (rule listF.fld_induct) fix xs :: "unit + 'a \ 'a listF" - assume raw_IH: "\a. a \ listFBNF_set2 xs \ P a" + assume raw_IH: "\a. a \ pre_listF_set2 xs \ P a" show "P (listF_fld xs)" proof (cases xs) case (Inl a) with IB show ?thesis unfolding NilF_def by simp @@ -55,8 +55,8 @@ case (Inr b) then obtain y ys where yys: "listF_fld xs = Conss y ys" unfolding Conss_def listF.fld_inject by (blast intro: prod.exhaust) - hence "ys \ listFBNF_set2 xs" - unfolding listFBNF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs + hence "ys \ pre_listF_set2 xs" + unfolding pre_listF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs collect_def[abs_def] by simp with raw_IH have "P ys" by blast with IH have "P (Conss y ys)" by blast diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:04:27 2012 +0200 @@ -25,17 +25,17 @@ (* These should be eventually inferred from compositionality *) -lemma processBNF_map[simp]: -"processBNF_map fa fp (Inl (a ,p)) = Inl (fa a, fp p)" -"processBNF_map fa fp (Inr (p1, p2)) = Inr (fp p1, fp p2)" -unfolding processBNF_map_def by auto +lemma pre_process_map[simp]: +"pre_process_map fa fp (Inl (a ,p)) = Inl (fa a, fp p)" +"pre_process_map fa fp (Inr (p1, p2)) = Inr (fp p1, fp p2)" +unfolding pre_process_map_def by auto -lemma processBNF_pred[simp]: -"processBNF_pred (op =) \ (Inl (a,p)) (Inl (a',p')) \ a = a' \ \ p p'" -"processBNF_pred (op =) \ (Inr (p,q)) (Inr (p',q')) \ \ p p' \ \ q q'" -"\ processBNF_pred (op =) \ (Inl ap) (Inr q1q2)" -"\ processBNF_pred (op =) \ (Inr q1q2) (Inl ap)" -by (auto simp: diag_def processBNF.pred_unfold) +lemma pre_process_pred[simp]: +"pre_process_pred (op =) \ (Inl (a,p)) (Inl (a',p')) \ a = a' \ \ p p'" +"pre_process_pred (op =) \ (Inr (p,q)) (Inr (p',q')) \ \ p p' \ \ q q'" +"\ pre_process_pred (op =) \ (Inl ap) (Inr q1q2)" +"\ pre_process_pred (op =) \ (Inr q1q2) (Inl ap)" +by (auto simp: diag_def pre_process.pred_unfold) subsection{* Constructors *} @@ -186,7 +186,7 @@ shows "p = p'" proof(intro mp[OF process.pred_coinduct, of \, OF _ phi], clarify) fix p p' assume \: "\ p p'" - show "processBNF_pred (op =) \ (process_unf p) (process_unf p')" + show "pre_process_pred (op =) \ (process_unf p) (process_unf p')" proof(cases rule: process_cases[of p]) case (Action a q) note p = Action hence "isAction p'" using iss[OF \] by (cases rule: process_cases[of p'], auto) @@ -216,7 +216,7 @@ shows "p = p'" proof(intro mp[OF process.pred_coinduct_upto, of \, OF _ phi], clarify) fix p p' assume \: "\ p p'" - show "processBNF_pred (op =) (\a b. \ a b \ a = b) (process_unf p) (process_unf p')" + show "pre_process_pred (op =) (\a b. \ a b \ a = b) (process_unf p) (process_unf p')" proof(cases rule: process_cases[of p]) case (Action a q) note p = Action hence "isAction p'" using iss[OF \] by (cases rule: process_cases[of p'], auto) @@ -328,7 +328,7 @@ have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))" using process.unf_coiter[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] - processBNF_map id_apply pcoiter_def . + pre_process_map id_apply pcoiter_def . thus "?f P = Action (pr P) (?f (co P))" unfolding pcoiter_def Action_def using process.fld_unf by metis next @@ -338,7 +338,7 @@ have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))" using process.unf_coiter[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] - processBNF_map id_apply pcoiter_def . + pre_process_map id_apply pcoiter_def . thus "?f P = Choice (?f (c1 P)) (?f (c2 P))" unfolding pcoiter_def Choice_def using process.fld_unf by metis qed @@ -369,14 +369,14 @@ have "process_unf (process_unf_corec ?s P) = Inl (pr P, p)" using process.unf_corec[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] - processBNF_map id_apply pcorec_def Inl by simp + 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] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] - processBNF_map id_apply pcorec_def Inr by simp + 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) qed qed @@ -407,14 +407,14 @@ have "process_unf (process_unf_corec ?s P) = Inr (p1, p2)" using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] - processBNF_map id_apply pcorec_def c1 c2 by simp + 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] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] - processBNF_map id_apply pcorec_def c1 c2 by simp + 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) qed next @@ -425,14 +425,14 @@ have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, p2)" using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] - processBNF_map id_apply pcorec_def c1 c2 by simp + 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] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] - processBNF_map id_apply pcorec_def c1 c2 by simp + 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) qed qed diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:04:27 2012 +0200 @@ -115,10 +115,10 @@ unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def] map_pair_def o_def prod_case_beta by simp -lemma streamBNF_pred[simp]: "streamBNF_pred \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" -by (auto simp: streamBNF.pred_unfold) +lemma pre_stream_pred[simp]: "pre_stream_pred \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" +by (auto simp: pre_stream.pred_unfold) -lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded streamBNF_pred[abs_def], +lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded pre_stream_pred[abs_def], folded hdd_def tll_def] definition plus :: "nat stream \ nat stream \ nat stream" (infixr "\" 66) where diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:27 2012 +0200 @@ -16,8 +16,8 @@ codata_raw treeFI: 'tree = "'a \ 'tree listF" -lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs" -unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs +lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" +unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs by (auto simp add: listF.set_natural') (* selectors for trees *) @@ -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 treeFIBNF_map_def by simp +unfolding lab_def pair_fun_def treeFI.unf_coiter 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 treeFIBNF_map_def by simp +unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp (* Tree reverse:*) definition "trev \ treeFI_unf_coiter (lab \ lrev o sub)" @@ -59,12 +59,12 @@ assume "phi a b" with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" "\i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto - hence "treeFIBNF_map id fst ?z = treeFI_unf a" "treeFIBNF_map id snd ?z = treeFI_unf b" - unfolding treeFIBNF_map_def by auto - moreover have "\(x, y) \ treeFIBNF_set2 ?z. phi x y" + hence "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b" + unfolding pre_treeFI_map_def by auto + moreover have "\(x, y) \ pre_treeFI_set2 ?z. phi x y" proof safe fix z1 z2 - assume "(z1, z2) \ treeFIBNF_set2 ?z" + assume "(z1, z2) \ pre_treeFI_set2 ?z" hence "(z1, z2) \ listF_set ?zs" by auto hence "\i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto with step'(2) obtain i where "i < lengthh (sub a)" @@ -72,9 +72,9 @@ with step'(3) show "phi z1 z2" by auto qed ultimately show "\z. - (treeFIBNF_map id fst z = treeFI_unf a \ - treeFIBNF_map id snd z = treeFI_unf b) \ - (\x y. (x, y) \ treeFIBNF_set2 z \ phi x y)" by blast + (pre_treeFI_map id fst z = treeFI_unf a \ + pre_treeFI_map id snd z = treeFI_unf b) \ + (\x y. (x, y) \ pre_treeFI_set2 z \ phi x y)" by blast qed lemma trev_trev: "trev (trev tr) = tr" diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:04:27 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 treeFsetIBNF_map_def by simp +unfolding lab_def pair_fun_def treeFsetI.unf_coiter 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 treeFsetIBNF_map_def by simp +unfolding sub_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp (* tree map (contrived example): *) definition "tmap f \ treeFsetI_unf_coiter (f o lab \ sub)" @@ -41,12 +41,12 @@ lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)" unfolding tmap_def by (simp add: coiter_pair_fun_sub) -lemma treeFsetIBNF_pred[simp]: "treeFsetIBNF_pred R1 R2 a b = (R1 (fst a) (fst b) \ +lemma pre_treeFsetI_pred[simp]: "pre_treeFsetI_pred R1 R2 a b = (R1 (fst a) (fst b) \ (\t \ fset (snd a). (\u \ fset (snd b). R2 t u)) \ (\t \ fset (snd b). (\u \ fset (snd a). R2 u t)))" apply (cases a) apply (cases b) -apply (simp add: treeFsetIBNF.pred_unfold) +apply (simp add: pre_treeFsetI.pred_unfold) done lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct] diff -r c28dd8326f9a -r a6260b4fb410 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:27 2012 +0200 @@ -173,9 +173,11 @@ fun mk_iter_like Ts Us t = let val (binders, body) = strip_type (fastype_of t); +val _ = tracing ("mk_iter_like: " ^ PolyML.makestring (binders, body, t)) (*###*) val (f_Us, prebody) = split_last binders; val Type (_, Ts0) = if lfp then prebody else body; val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us); +val _ = tracing (" Ts0 @ Us0 ...: " ^ PolyML.makestring (Ts0, Us0, Ts, Us)) (*###*) in Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; @@ -371,6 +373,7 @@ val [iter_def, rec_def] = map (Morphism.thm phi) defs; +val _ = tracing ("LFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*) val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; in ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy) @@ -414,6 +417,7 @@ val [coiter_def, corec_def] = map (Morphism.thm phi) defs; +val _ = tracing ("GFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*) val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts; in ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)