# HG changeset patch # User blanchet # Date 1348646459 -7200 # Node ID 557302525778ae6a832d84375dd12b88cc07bf99 # Parent 4e5bd3883429f32d05254558418aff0c2ef19d76 renamed "dtor_rel_coinduct" etc. to "dtor_coinduct" diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Wed Sep 26 10:00:59 2012 +0200 @@ -130,7 +130,7 @@ \\ (NNode n1 as1) (NNode n2 as2)\ \ n1 = n2 \ llift2 \ as1 as2" shows "tr1 = tr2" -apply(rule mp[OF Tree.dtor_rel_coinduct[of \ tr1 tr2] phi]) proof clarify +apply(rule mp[OF Tree.dtor_coinduct[of \ tr1 tr2] phi]) proof clarify fix tr1 tr2 assume \: "\ tr1 tr2" show "pre_Tree_rel \ (Tree_dtor tr1) (Tree_dtor tr2)" apply(cases rule: Tree.ctor_exhaust[of tr1], cases rule: Tree.ctor_exhaust[of tr2]) diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Examples/Process.thy --- a/src/HOL/BNF/Examples/Process.thy Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Examples/Process.thy Wed Sep 26 10:00:59 2012 +0200 @@ -45,7 +45,7 @@ Act: "\ a a' p p'. \ (Action a p) (Action a' p') \ a = a' \ \ p p'" and Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ \ p p' \ \ q q'" shows "p = p'" -proof(intro mp[OF process.dtor_rel_coinduct, of \, OF _ phi], clarify) +proof(intro mp[OF process.dtor_coinduct, of \, OF _ phi], clarify) fix p p' assume \: "\ p p'" show "pre_process_rel (op =) \ (process_dtor p) (process_dtor p')" proof(cases rule: process.exhaust[of p]) diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Wed Sep 26 10:00:59 2012 +0200 @@ -122,7 +122,7 @@ unfolding prod_rel_def by auto lemmas stream_coind = - mp[OF stream.dtor_rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def] + mp[OF stream.dtor_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def] definition plus :: "nat stream \ nat stream \ nat stream" (infixr "\" 66) where [simp]: "plus xs ys = diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Examples/TreeFsetI.thy --- a/src/HOL/BNF/Examples/TreeFsetI.thy Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy Wed Sep 26 10:00:59 2012 +0200 @@ -50,7 +50,7 @@ apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def) done -lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_rel_coinduct] +lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_coinduct] lemma "tmap (f o g) x = tmap f (tmap g x)" by (intro treeFsetI_coind[where P="%x1 x2. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"]) diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200 @@ -44,6 +44,7 @@ val disc_corec_iffN: string val disc_corecsN: string val dtorN: string + val dtor_coinductN: string val dtor_corecN: string val dtor_corecsN: string val dtor_ctorN: string @@ -54,13 +55,12 @@ val dtor_map_strong_coinductN: string val dtor_map_uniqueN: string val dtor_relN: string - val dtor_rel_coinductN: string - val dtor_rel_strong_coinductN: string val dtor_set_inclN: string val dtor_set_set_inclN: string val dtor_srelN: string val dtor_srel_coinductN: string val dtor_srel_strong_coinductN: string + val dtor_strong_coinductN: string val dtor_unfoldN: string val dtor_unfold_uniqueN: string val dtor_unfoldsN: string @@ -244,11 +244,11 @@ val ctor_inductN = ctorN ^ "_" ^ inductN val ctor_induct2N = ctor_inductN ^ "2" val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN -val dtor_rel_coinductN = dtor_relN ^ "_" ^ coinductN +val dtor_coinductN = dtorN ^ "_" ^ coinductN val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN val strongN = "strong_" val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN -val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN +val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" val hset_recN = hsetN ^ "_rec" diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200 @@ -2180,9 +2180,8 @@ val timer = time (timer "corec definitions & thms"); - val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm, - dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, - dtor_rel_strong_coinduct_thm) = + val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_coinduct_thm, + dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_strong_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2276,12 +2275,11 @@ val rel_of_srel_thms = srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; - val dtor_rel_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct; - val dtor_rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct; + val dtor_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct; + val dtor_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct; in (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct, - dtor_rel_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, - dtor_rel_strong_coinduct) + dtor_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, dtor_strong_coinduct) end; val timer = time (timer "coinduction"); @@ -2963,8 +2961,8 @@ end; val common_notes = - [(dtor_rel_coinductN, [dtor_rel_coinduct_thm]), - (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm])] @ + [(dtor_coinductN, [dtor_coinduct_thm]), + (dtor_strong_coinductN, [dtor_strong_coinduct_thm])] @ (if note_all then [(dtor_map_coinductN, [dtor_map_coinduct_thm]), (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),