desharna@57471: blanchet@55059: (* Title: HOL/BNF_LFP.thy blanchet@48975: Author: Dmitriy Traytel, TU Muenchen blanchet@53305: Author: Lorenz Panny, TU Muenchen blanchet@53305: Author: Jasmin Blanchette, TU Muenchen blanchet@53305: Copyright 2012, 2013 blanchet@48975: blanchet@48975: Least fixed point operation on bounded natural functors. blanchet@48975: *) blanchet@48975: blanchet@48975: header {* Least Fixed Point Operation on Bounded Natural Functors *} blanchet@48975: blanchet@48975: theory BNF_LFP blanchet@53311: imports BNF_FP_Base blanchet@48975: keywords blanchet@53305: "datatype_new" :: thy_decl and blanchet@55575: "datatype_compat" :: thy_decl blanchet@48975: begin blanchet@48975: blanchet@49312: lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" blanchet@49312: by blast blanchet@49312: blanchet@56346: lemma image_Collect_subsetI: "(\x. P x \ f x \ B) \ f ` {x. P x} \ B" blanchet@49312: by blast blanchet@49312: blanchet@49312: lemma Collect_restrict: "{x. x \ X \ P x} \ X" blanchet@49312: by auto blanchet@49312: blanchet@49312: lemma prop_restrict: "\x \ Z; Z \ {x. x \ X \ P x}\ \ P x" blanchet@49312: by auto blanchet@49312: blanchet@55023: lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ underS R j" blanchet@55023: unfolding underS_def by simp blanchet@49312: blanchet@55023: lemma underS_E: "i \ underS R j \ i \ j \ (i, j) \ R" blanchet@55023: unfolding underS_def by simp blanchet@49312: blanchet@55023: lemma underS_Field: "i \ underS R j \ i \ Field R" blanchet@55023: unfolding underS_def Field_def by auto blanchet@49312: blanchet@49312: lemma FieldI2: "(i, j) \ R \ j \ Field R" blanchet@49312: unfolding Field_def by auto blanchet@49312: wenzelm@57641: lemma fst_convol': "fst (\f, g\ x) = f x" blanchet@49312: using fst_convol unfolding convol_def by simp blanchet@49312: wenzelm@57641: lemma snd_convol': "snd (\f, g\ x) = g x" blanchet@49312: using snd_convol unfolding convol_def by simp blanchet@49312: wenzelm@57641: lemma convol_expand_snd: "fst o f = g \ \g, snd o f\ = f" blanchet@49312: unfolding convol_def by auto blanchet@49312: traytel@55811: lemma convol_expand_snd': traytel@55811: assumes "(fst o f = g)" wenzelm@57641: shows "h = snd o f \ \g, h\ = f" traytel@55811: proof - wenzelm@57641: from assms have *: "\g, snd o f\ = f" by (rule convol_expand_snd) wenzelm@57641: then have "h = snd o f \ h = snd o \g, snd o f\" by simp traytel@55811: moreover have "\ \ h = snd o f" by (simp add: snd_convol) wenzelm@57641: moreover have "\ \ \g, h\ = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) traytel@55811: ultimately show ?thesis by simp traytel@55811: qed blanchet@49312: lemma bij_betwE: "bij_betw f A B \ \a\A. f a \ B" blanchet@49312: unfolding bij_betw_def by auto blanchet@49312: blanchet@49312: lemma bij_betw_imageE: "bij_betw f A B \ f ` A = B" blanchet@49312: unfolding bij_betw_def by auto blanchet@49312: traytel@56237: lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \ traytel@56237: (bij_betw f A B \ x \ B) \ f (the_inv_into A f x) = x" traytel@56237: unfolding bij_betw_def by (blast intro: f_the_inv_into_f) blanchet@49312: traytel@56237: lemma ex_bij_betw: "|A| \o (r :: 'b rel) \ \f B :: 'b set. bij_betw f B A" traytel@56237: by (subst (asm) internalize_card_of_ordLeq) traytel@56237: (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric]) blanchet@49312: blanchet@49312: lemma bij_betwI': blanchet@49312: "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); blanchet@49312: \x. x \ X \ f x \ Y; blanchet@49312: \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" traytel@53695: unfolding bij_betw_def inj_on_def by blast blanchet@49312: blanchet@49312: lemma surj_fun_eq: blanchet@49312: assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" blanchet@49312: shows "g1 = g2" blanchet@49312: proof (rule ext) blanchet@49312: fix y blanchet@49312: from surj_on obtain x where "x \ X" and "y = f x" by blast blanchet@49312: thus "g1 y = g2 y" using eq_on by simp blanchet@49312: qed blanchet@49312: blanchet@49312: lemma Card_order_wo_rel: "Card_order r \ wo_rel r" blanchet@49514: unfolding wo_rel_def card_order_on_def by blast blanchet@49312: blanchet@49312: lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ blanchet@49312: \y \ Field r. x \ y \ (x, y) \ r" blanchet@49312: unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) blanchet@49312: blanchet@49312: lemma Card_order_trans: blanchet@49312: "\Card_order r; x \ y; (x, y) \ r; y \ z; (y, z) \ r\ \ x \ z \ (x, z) \ r" blanchet@49312: unfolding card_order_on_def well_order_on_def linear_order_on_def blanchet@49312: partial_order_on_def preorder_on_def trans_def antisym_def by blast blanchet@49312: blanchet@49312: lemma Cinfinite_limit2: blanchet@49312: assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r" blanchet@49312: shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)" blanchet@49312: proof - blanchet@49312: from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" blanchet@49312: unfolding card_order_on_def well_order_on_def linear_order_on_def blanchet@49312: partial_order_on_def preorder_on_def by auto blanchet@49312: obtain y1 where y1: "y1 \ Field r" "x1 \ y1" "(x1, y1) \ r" blanchet@49312: using Cinfinite_limit[OF x1 r] by blast blanchet@49312: obtain y2 where y2: "y2 \ Field r" "x2 \ y2" "(x2, y2) \ r" blanchet@49312: using Cinfinite_limit[OF x2 r] by blast blanchet@49312: show ?thesis blanchet@49312: proof (cases "y1 = y2") blanchet@49312: case True with y1 y2 show ?thesis by blast blanchet@49312: next blanchet@49312: case False blanchet@49312: with y1(1) y2(1) total have "(y1, y2) \ r \ (y2, y1) \ r" blanchet@49312: unfolding total_on_def by auto blanchet@49312: thus ?thesis blanchet@49312: proof blanchet@49312: assume *: "(y1, y2) \ r" blanchet@49312: with trans y1(3) have "(x1, y2) \ r" unfolding trans_def by blast blanchet@49312: with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def) blanchet@49312: next blanchet@49312: assume *: "(y2, y1) \ r" blanchet@49312: with trans y2(3) have "(x2, y1) \ r" unfolding trans_def by blast blanchet@49312: with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def) blanchet@49312: qed blanchet@49312: qed blanchet@49312: qed blanchet@49312: blanchet@49312: lemma Cinfinite_limit_finite: "\finite X; X \ Field r; Cinfinite r\ blanchet@49312: \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)" blanchet@49312: proof (induct X rule: finite_induct) blanchet@49312: case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto blanchet@49312: next blanchet@49312: case (insert x X) blanchet@49312: then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast blanchet@49312: then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r" blanchet@49312: using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast blanchet@49326: show ?case blanchet@49326: apply (intro bexI ballI) blanchet@49326: apply (erule insertE) blanchet@49326: apply hypsubst blanchet@49326: apply (rule z(2)) blanchet@49326: using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3) blanchet@49326: apply blast blanchet@49326: apply (rule z(1)) blanchet@49326: done blanchet@49312: qed blanchet@49312: blanchet@49312: lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" blanchet@49312: by auto blanchet@49312: blanchet@49312: (*helps resolution*) blanchet@49312: lemma well_order_induct_imp: blanchet@49312: "wo_rel r \ (\x. \y. y \ x \ (y, x) \ r \ y \ Field r \ P y \ x \ Field r \ P x) \ blanchet@49312: x \ Field r \ P x" blanchet@49312: by (erule wo_rel.well_order_induct) blanchet@49312: blanchet@49312: lemma meta_spec2: blanchet@49312: assumes "(\x y. PROP P x y)" blanchet@49312: shows "PROP P x y" blanchet@55084: by (rule assms) blanchet@49312: traytel@54841: lemma nchotomy_relcomppE: traytel@55811: assumes "\y. \x. y = f x" "(r OO s) a c" "\b. r a (f b) \ s (f b) c \ P" traytel@55811: shows P traytel@55811: proof (rule relcompp.cases[OF assms(2)], hypsubst) traytel@55811: fix b assume "r a b" "s b c" traytel@55811: moreover from assms(1) obtain b' where "b = f b'" by blast traytel@55811: ultimately show P by (blast intro: assms(3)) traytel@55811: qed traytel@54841: blanchet@55945: lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g" blanchet@55945: unfolding rel_fun_def vimage2p_def by auto traytel@52731: traytel@52731: lemma predicate2D_vimage2p: "\R \ vimage2p f g S; R x y\ \ S (f x) (g y)" traytel@52731: unfolding vimage2p_def by auto traytel@52731: blanchet@55945: lemma id_transfer: "rel_fun A A id id" blanchet@55945: unfolding rel_fun_def by simp blanchet@55084: traytel@55770: lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" blanchet@55851: by (rule ssubst) traytel@55770: blanchet@55062: ML_file "Tools/BNF/bnf_lfp_util.ML" blanchet@55062: ML_file "Tools/BNF/bnf_lfp_tactics.ML" blanchet@55062: ML_file "Tools/BNF/bnf_lfp.ML" blanchet@55062: ML_file "Tools/BNF/bnf_lfp_compat.ML" blanchet@55571: ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" blanchet@56643: blanchet@55084: hide_fact (open) id_transfer blanchet@55084: blanchet@48975: end