# HG changeset patch # User Andreas Lochbihler # Date 1380271202 -7200 # Node ID 54b08afc03c762706e9d04f1552cee9448a6795f # Parent 5431e1392b142d1564f5543f963b3afb2d49fb1b# Parent fc631b2831d30f7376156040b88a15fd005f785c merged diff -r fc631b2831d3 -r 54b08afc03c7 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Fri Sep 27 09:17:25 2013 +0200 +++ b/src/HOL/Lifting.thy Fri Sep 27 10:40:02 2013 +0200 @@ -76,6 +76,16 @@ lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast +lemma [simp]: + shows left_unique_conversep: "left_unique A\\ \ right_unique A" + and right_unique_conversep: "right_unique A\\ \ left_unique A" +by(auto simp add: left_unique_def right_unique_def) + +lemma [simp]: + shows left_total_conversep: "left_total A\\ \ right_total A" + and right_total_conversep: "right_total A\\ \ left_total A" +by(simp_all add: left_total_def right_total_def) + subsection {* Quotient Predicate *} definition diff -r fc631b2831d3 -r 54b08afc03c7 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Fri Sep 27 09:17:25 2013 +0200 +++ b/src/HOL/Lifting_Set.thy Fri Sep 27 10:40:02 2013 +0200 @@ -23,7 +23,7 @@ and set_relD2: "\ set_rel R A B; y \ B \ \ \x \ A. R x y" by(simp_all add: set_rel_def) -lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)" +lemma set_rel_conversep [simp]: "set_rel A\\ = (set_rel A)\\" unfolding set_rel_def by auto lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" @@ -71,8 +71,7 @@ lemma right_total_set_rel [transfer_rule]: "right_total A \ right_total (set_rel A)" - unfolding right_total_def set_rel_def - by (rule allI, rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) +using left_total_set_rel[of "A\\"] by simp lemma right_unique_set_rel [transfer_rule]: "right_unique A \ right_unique (set_rel A)" @@ -80,11 +79,7 @@ lemma bi_total_set_rel [transfer_rule]: "bi_total A \ bi_total (set_rel A)" - unfolding bi_total_def set_rel_def - apply safe - apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) - apply (rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) - done +by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel) lemma bi_unique_set_rel [transfer_rule]: "bi_unique A \ bi_unique (set_rel A)" @@ -100,7 +95,7 @@ assumes "Quotient R Abs Rep T" shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" using assms unfolding Quotient_alt_def4 - apply (simp add: set_rel_OO[symmetric] set_rel_conversep) + apply (simp add: set_rel_OO[symmetric]) apply (simp add: set_rel_def, fast) done diff -r fc631b2831d3 -r 54b08afc03c7 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Fri Sep 27 09:17:25 2013 +0200 +++ b/src/HOL/Predicate.thy Fri Sep 27 10:40:02 2013 +0200 @@ -5,7 +5,7 @@ header {* Predicates as enumerations *} theory Predicate -imports List +imports String begin subsection {* The type of predicate enumerations (a monad) *} @@ -590,13 +590,8 @@ "(THE x. eval P x) = x \ the P = x" by (simp add: the_def) -definition not_unique :: "'a pred \ 'a" where - [code del]: "not_unique A = (THE x. eval A x)" - -code_abort not_unique - -lemma the_eq [code]: "the A = singleton (\x. not_unique A) A" - by (rule the_eqI) (simp add: singleton_def not_unique_def) +lemma the_eq [code]: "the A = singleton (\x. Code.abort (STR ''not_unique'') (\_. the A)) A" + by (rule the_eqI) (simp add: singleton_def the_def) code_reflect Predicate datatypes pred = Seq and seq = Empty | Insert | Join @@ -722,7 +717,7 @@ hide_type (open) pred seq hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds - Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the + Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map the iterate_upto hide_fact (open) null_def member_def diff -r fc631b2831d3 -r 54b08afc03c7 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Fri Sep 27 09:17:25 2013 +0200 +++ b/src/HOL/Topological_Spaces.thy Fri Sep 27 10:40:02 2013 +0200 @@ -2282,5 +2282,224 @@ using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff) qed +subsection {* Setup @{typ "'a filter"} for lifting and transfer *} + +context begin interpretation lifting_syntax . + +definition filter_rel :: "('a \ 'b \ bool) \ 'a filter \ 'b filter \ bool" +where "filter_rel R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" + +lemma filter_rel_eventually: + "filter_rel R F G \ + ((R ===> op =) ===> op =) (\P. eventually P F) (\P. eventually P G)" +by(simp add: filter_rel_def eventually_def) + +lemma filtermap_id [simp, id_simps]: "filtermap id = id" +by(simp add: fun_eq_iff id_def filtermap_ident) + +lemma filtermap_id' [simp]: "filtermap (\x. x) = (\F. F)" +using filtermap_id unfolding id_def . + +lemma Quotient_filter [quot_map]: + assumes Q: "Quotient R Abs Rep T" + shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)" +unfolding Quotient_alt_def +proof(intro conjI strip) + from Q have *: "\x y. T x y \ Abs x = y" + unfolding Quotient_alt_def by blast + + fix F G + assume "filter_rel T F G" + thus "filtermap Abs F = G" unfolding filter_eq_iff + by(auto simp add: eventually_filtermap filter_rel_eventually * fun_relI del: iffI elim!: fun_relD) +next + from Q have *: "\x. T (Rep x) x" unfolding Quotient_alt_def by blast + + fix F + show "filter_rel T (filtermap Rep F) F" + by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\P. eventually P F"] fun_relI + del: iffI simp add: eventually_filtermap filter_rel_eventually) +qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff filter_rel_eventually + fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def]) + +lemma eventually_parametric [transfer_rule]: + "((A ===> op =) ===> filter_rel A ===> op =) eventually eventually" +by(simp add: fun_rel_def filter_rel_eventually) + +lemma filter_rel_eq [relator_eq]: "filter_rel op = = op =" +by(auto simp add: filter_rel_eventually fun_rel_eq fun_eq_iff filter_eq_iff) + +lemma filter_rel_mono [relator_mono]: + "A \ B \ filter_rel A \ filter_rel B" +unfolding filter_rel_eventually[abs_def] +by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) + +lemma reflp_filter_rel [reflexivity_rule]: "reflp R \ reflp (filter_rel R)" +unfolding filter_rel_eventually[abs_def] +by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD) + +lemma filter_rel_conversep [simp]: "filter_rel A\\ = (filter_rel A)\\" +by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def) + +lemma is_filter_parametric_aux: + assumes "is_filter F" + assumes [transfer_rule]: "bi_total A" "bi_unique A" + and [transfer_rule]: "((A ===> op =) ===> op =) F G" + shows "is_filter G" +proof - + interpret is_filter F by fact + show ?thesis + proof + have "F (\_. True) = G (\x. True)" by transfer_prover + thus "G (\x. True)" by(simp add: True) + next + fix P' Q' + assume "G P'" "G Q'" + moreover + from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def] + obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast + have "F P = G P'" "F Q = G Q'" by transfer_prover+ + ultimately have "F (\x. P x \ Q x)" by(simp add: conj) + moreover have "F (\x. P x \ Q x) = G (\x. P' x \ Q' x)" by transfer_prover + ultimately show "G (\x. P' x \ Q' x)" by simp + next + fix P' Q' + assume "\x. P' x \ Q' x" "G P'" + moreover + from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def] + obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast + have "F P = G P'" by transfer_prover + moreover have "(\x. P x \ Q x) \ (\x. P' x \ Q' x)" by transfer_prover + ultimately have "F Q" by(simp add: mono) + moreover have "F Q = G Q'" by transfer_prover + ultimately show "G Q'" by simp + qed +qed + +lemma is_filter_parametric [transfer_rule]: + "\ bi_total A; bi_unique A \ + \ (((A ===> op =) ===> op =) ===> op =) is_filter is_filter" +apply(rule fun_relI) +apply(rule iffI) + apply(erule (3) is_filter_parametric_aux) +apply(erule is_filter_parametric_aux[where A="conversep A"]) +apply(auto simp add: fun_rel_def) +done + +lemma left_total_filter_rel [reflexivity_rule]: + assumes [transfer_rule]: "bi_total A" "bi_unique A" + shows "left_total (filter_rel A)" +proof(rule left_totalI) + fix F :: "'a filter" + from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq] + obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\P. eventually P F) G" + unfolding bi_total_def by blast + moreover have "is_filter (\P. eventually P F) \ is_filter G" by transfer_prover + hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter) + ultimately have "filter_rel A F (Abs_filter G)" + by(simp add: filter_rel_eventually eventually_Abs_filter) + thus "\G. filter_rel A F G" .. +qed + +lemma right_total_filter_rel [transfer_rule]: + "\ bi_total A; bi_unique A \ \ right_total (filter_rel A)" +using left_total_filter_rel[of "A\\"] by simp + +lemma bi_total_filter_rel [transfer_rule]: + assumes "bi_total A" "bi_unique A" + shows "bi_total (filter_rel A)" +unfolding bi_total_conv_left_right using assms +by(simp add: left_total_filter_rel right_total_filter_rel) + +lemma left_unique_filter_rel [reflexivity_rule]: + assumes "left_unique A" + shows "left_unique (filter_rel A)" +proof(rule left_uniqueI) + fix F F' G + assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G" + show "F = F'" + unfolding filter_eq_iff + proof + fix P :: "'a \ bool" + obtain P' where [transfer_rule]: "(A ===> op =) P P'" + using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast + have "eventually P F = eventually P' G" + and "eventually P F' = eventually P' G" by transfer_prover+ + thus "eventually P F = eventually P F'" by simp + qed +qed + +lemma right_unique_filter_rel [transfer_rule]: + "right_unique A \ right_unique (filter_rel A)" +using left_unique_filter_rel[of "A\\"] by simp + +lemma bi_unique_filter_rel [transfer_rule]: + "bi_unique A \ bi_unique (filter_rel A)" +by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel) + +lemma top_filter_parametric [transfer_rule]: + "bi_total A \ (filter_rel A) top top" +by(simp add: filter_rel_eventually All_transfer) + +lemma bot_filter_parametric [transfer_rule]: "(filter_rel A) bot bot" +by(simp add: filter_rel_eventually fun_rel_def) + +lemma sup_filter_parametric [transfer_rule]: + "(filter_rel A ===> filter_rel A ===> filter_rel A) sup sup" +by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD) + +lemma Sup_filter_parametric [transfer_rule]: + "(set_rel (filter_rel A) ===> filter_rel A) Sup Sup" +proof(rule fun_relI) + fix S T + assume [transfer_rule]: "set_rel (filter_rel A) S T" + show "filter_rel A (Sup S) (Sup T)" + by(simp add: filter_rel_eventually eventually_Sup) transfer_prover +qed + +lemma principal_parametric [transfer_rule]: + "(set_rel A ===> filter_rel A) principal principal" +proof(rule fun_relI) + fix S S' + assume [transfer_rule]: "set_rel A S S'" + show "filter_rel A (principal S) (principal S')" + by(simp add: filter_rel_eventually eventually_principal) transfer_prover +qed + +context + fixes A :: "'a \ 'b \ bool" + assumes [transfer_rule]: "bi_unique A" +begin + +lemma le_filter_parametric [transfer_rule]: + "(filter_rel A ===> filter_rel A ===> op =) op \ op \" +unfolding le_filter_def[abs_def] by transfer_prover + +lemma less_filter_parametric [transfer_rule]: + "(filter_rel A ===> filter_rel A ===> op =) op < op <" +unfolding less_filter_def[abs_def] by transfer_prover + +context + assumes [transfer_rule]: "bi_total A" +begin + +lemma Inf_filter_parametric [transfer_rule]: + "(set_rel (filter_rel A) ===> filter_rel A) Inf Inf" +unfolding Inf_filter_def[abs_def] by transfer_prover + +lemma inf_filter_parametric [transfer_rule]: + "(filter_rel A ===> filter_rel A ===> filter_rel A) inf inf" +proof(intro fun_relI)+ + fix F F' G G' + assume [transfer_rule]: "filter_rel A F F'" "filter_rel A G G'" + have "filter_rel A (Inf {F, G}) (Inf {F', G'})" by transfer_prover + thus "filter_rel A (inf F G) (inf F' G')" by simp +qed + end +end + +end + +end diff -r fc631b2831d3 -r 54b08afc03c7 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Sep 27 09:17:25 2013 +0200 +++ b/src/HOL/Transfer.thy Fri Sep 27 10:40:02 2013 +0200 @@ -201,6 +201,12 @@ "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" unfolding bi_unique_def fun_rel_def by auto +lemma bi_unique_conversep [simp]: "bi_unique R\\ = bi_unique R" +by(auto simp add: bi_unique_def) + +lemma bi_total_conversep [simp]: "bi_total R\\ = bi_total R" +by(auto simp add: bi_total_def) + text {* Properties are preserved by relation composition. *} lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)"