diff -r c6db12ddb60c -r c785fff02a8f Nominal/FSet.thy --- a/Nominal/FSet.thy Thu May 27 18:37:52 2010 +0200 +++ b/Nominal/FSet.thy Thu May 27 18:40:10 2010 +0200 @@ -160,10 +160,14 @@ text {* Respectfullness *} -lemma [quot_respect]: +lemma append_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) op @ op @" by auto +lemma append_rsp_unfolded: + "\x \ y; v \ w\ \ x @ v \ y @ w" + by auto + lemma [quot_respect]: shows "(op \ ===> op \ ===> op =) sub_list sub_list" by (auto simp add: sub_list_def) @@ -350,7 +354,7 @@ then show ?thesis using f i by auto qed -lemma [quot_respect]: +lemma concat_rsp[quot_respect]: shows "(list_rel op \ OOO op \ ===> op \) concat concat" proof (rule fun_relI, elim pred_compE) fix a b ba bb @@ -373,6 +377,31 @@ then show "concat a \ concat b" by simp qed + + +lemma concat_rsp_unfolded: + "\list_rel op \ a ba; ba \ bb; list_rel op \ bb b\ \ concat a \ concat b" +proof - + fix a b ba bb + assume a: "list_rel op \ a ba" + assume b: "ba \ bb" + assume c: "list_rel op \ bb b" + have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + fix x + show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + assume d: "\xa\set a. x \ set xa" + show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) + next + assume e: "\xa\set b. x \ set xa" + have a': "list_rel op \ ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) + have b': "bb \ ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) + have c': "list_rel op \ b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) + show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) + qed + qed + then show "concat a \ concat b" by simp +qed + lemma [quot_respect]: "((op =) ===> op \ ===> op \) filter filter" by auto @@ -597,6 +626,11 @@ apply auto done +lemma insert_preserve2: + shows "((rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op #) = + (id ---> rep_fset ---> abs_fset) op #" + by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) + lemma [quot_preserve]: "(rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op # = finsert" by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]