2336 |
2336 |
2337 subsection {* Setup @{typ "'a filter"} for lifting and transfer *} |
2337 subsection {* Setup @{typ "'a filter"} for lifting and transfer *} |
2338 |
2338 |
2339 context begin interpretation lifting_syntax . |
2339 context begin interpretation lifting_syntax . |
2340 |
2340 |
2341 definition filter_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool" |
2341 definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool" |
2342 where "filter_rel R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" |
2342 where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" |
2343 |
2343 |
2344 lemma filter_rel_eventually: |
2344 lemma rel_filter_eventually: |
2345 "filter_rel R F G \<longleftrightarrow> |
2345 "rel_filter R F G \<longleftrightarrow> |
2346 ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)" |
2346 ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)" |
2347 by(simp add: filter_rel_def eventually_def) |
2347 by(simp add: rel_filter_def eventually_def) |
2348 |
2348 |
2349 lemma filtermap_id [simp, id_simps]: "filtermap id = id" |
2349 lemma filtermap_id [simp, id_simps]: "filtermap id = id" |
2350 by(simp add: fun_eq_iff id_def filtermap_ident) |
2350 by(simp add: fun_eq_iff id_def filtermap_ident) |
2351 |
2351 |
2352 lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)" |
2352 lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)" |
2353 using filtermap_id unfolding id_def . |
2353 using filtermap_id unfolding id_def . |
2354 |
2354 |
2355 lemma Quotient_filter [quot_map]: |
2355 lemma Quotient_filter [quot_map]: |
2356 assumes Q: "Quotient R Abs Rep T" |
2356 assumes Q: "Quotient R Abs Rep T" |
2357 shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)" |
2357 shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)" |
2358 unfolding Quotient_alt_def |
2358 unfolding Quotient_alt_def |
2359 proof(intro conjI strip) |
2359 proof(intro conjI strip) |
2360 from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y" |
2360 from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y" |
2361 unfolding Quotient_alt_def by blast |
2361 unfolding Quotient_alt_def by blast |
2362 |
2362 |
2363 fix F G |
2363 fix F G |
2364 assume "filter_rel T F G" |
2364 assume "rel_filter T F G" |
2365 thus "filtermap Abs F = G" unfolding filter_eq_iff |
2365 thus "filtermap Abs F = G" unfolding filter_eq_iff |
2366 by(auto simp add: eventually_filtermap filter_rel_eventually * fun_relI del: iffI elim!: fun_relD) |
2366 by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD) |
2367 next |
2367 next |
2368 from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast |
2368 from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast |
2369 |
2369 |
2370 fix F |
2370 fix F |
2371 show "filter_rel T (filtermap Rep F) F" |
2371 show "rel_filter T (filtermap Rep F) F" |
2372 by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI |
2372 by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI |
2373 del: iffI simp add: eventually_filtermap filter_rel_eventually) |
2373 del: iffI simp add: eventually_filtermap rel_filter_eventually) |
2374 qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff filter_rel_eventually |
2374 qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually |
2375 fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def]) |
2375 fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def]) |
2376 |
2376 |
2377 lemma eventually_parametric [transfer_rule]: |
2377 lemma eventually_parametric [transfer_rule]: |
2378 "((A ===> op =) ===> filter_rel A ===> op =) eventually eventually" |
2378 "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually" |
2379 by(simp add: fun_rel_def filter_rel_eventually) |
2379 by(simp add: fun_rel_def rel_filter_eventually) |
2380 |
2380 |
2381 lemma filter_rel_eq [relator_eq]: "filter_rel op = = op =" |
2381 lemma rel_filter_eq [relator_eq]: "rel_filter op = = op =" |
2382 by(auto simp add: filter_rel_eventually fun_rel_eq fun_eq_iff filter_eq_iff) |
2382 by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff) |
2383 |
2383 |
2384 lemma filter_rel_mono [relator_mono]: |
2384 lemma rel_filter_mono [relator_mono]: |
2385 "A \<le> B \<Longrightarrow> filter_rel A \<le> filter_rel B" |
2385 "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B" |
2386 unfolding filter_rel_eventually[abs_def] |
2386 unfolding rel_filter_eventually[abs_def] |
2387 by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) |
2387 by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) |
2388 |
2388 |
2389 lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>" |
2389 lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>" |
2390 by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def) |
2390 by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def) |
2391 |
2391 |
2392 lemma is_filter_parametric_aux: |
2392 lemma is_filter_parametric_aux: |
2393 assumes "is_filter F" |
2393 assumes "is_filter F" |
2394 assumes [transfer_rule]: "bi_total A" "bi_unique A" |
2394 assumes [transfer_rule]: "bi_total A" "bi_unique A" |
2395 and [transfer_rule]: "((A ===> op =) ===> op =) F G" |
2395 and [transfer_rule]: "((A ===> op =) ===> op =) F G" |
2432 apply(erule (3) is_filter_parametric_aux) |
2432 apply(erule (3) is_filter_parametric_aux) |
2433 apply(erule is_filter_parametric_aux[where A="conversep A"]) |
2433 apply(erule is_filter_parametric_aux[where A="conversep A"]) |
2434 apply(auto simp add: fun_rel_def) |
2434 apply(auto simp add: fun_rel_def) |
2435 done |
2435 done |
2436 |
2436 |
2437 lemma left_total_filter_rel [reflexivity_rule]: |
2437 lemma left_total_rel_filter [reflexivity_rule]: |
2438 assumes [transfer_rule]: "bi_total A" "bi_unique A" |
2438 assumes [transfer_rule]: "bi_total A" "bi_unique A" |
2439 shows "left_total (filter_rel A)" |
2439 shows "left_total (rel_filter A)" |
2440 proof(rule left_totalI) |
2440 proof(rule left_totalI) |
2441 fix F :: "'a filter" |
2441 fix F :: "'a filter" |
2442 from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq] |
2442 from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq] |
2443 obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" |
2443 obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" |
2444 unfolding bi_total_def by blast |
2444 unfolding bi_total_def by blast |
2445 moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover |
2445 moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover |
2446 hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter) |
2446 hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter) |
2447 ultimately have "filter_rel A F (Abs_filter G)" |
2447 ultimately have "rel_filter A F (Abs_filter G)" |
2448 by(simp add: filter_rel_eventually eventually_Abs_filter) |
2448 by(simp add: rel_filter_eventually eventually_Abs_filter) |
2449 thus "\<exists>G. filter_rel A F G" .. |
2449 thus "\<exists>G. rel_filter A F G" .. |
2450 qed |
2450 qed |
2451 |
2451 |
2452 lemma right_total_filter_rel [transfer_rule]: |
2452 lemma right_total_rel_filter [transfer_rule]: |
2453 "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (filter_rel A)" |
2453 "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)" |
2454 using left_total_filter_rel[of "A\<inverse>\<inverse>"] by simp |
2454 using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2455 |
2455 |
2456 lemma bi_total_filter_rel [transfer_rule]: |
2456 lemma bi_total_rel_filter [transfer_rule]: |
2457 assumes "bi_total A" "bi_unique A" |
2457 assumes "bi_total A" "bi_unique A" |
2458 shows "bi_total (filter_rel A)" |
2458 shows "bi_total (rel_filter A)" |
2459 unfolding bi_total_conv_left_right using assms |
2459 unfolding bi_total_conv_left_right using assms |
2460 by(simp add: left_total_filter_rel right_total_filter_rel) |
2460 by(simp add: left_total_rel_filter right_total_rel_filter) |
2461 |
2461 |
2462 lemma left_unique_filter_rel [reflexivity_rule]: |
2462 lemma left_unique_rel_filter [reflexivity_rule]: |
2463 assumes "left_unique A" |
2463 assumes "left_unique A" |
2464 shows "left_unique (filter_rel A)" |
2464 shows "left_unique (rel_filter A)" |
2465 proof(rule left_uniqueI) |
2465 proof(rule left_uniqueI) |
2466 fix F F' G |
2466 fix F F' G |
2467 assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G" |
2467 assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G" |
2468 show "F = F'" |
2468 show "F = F'" |
2469 unfolding filter_eq_iff |
2469 unfolding filter_eq_iff |
2470 proof |
2470 proof |
2471 fix P :: "'a \<Rightarrow> bool" |
2471 fix P :: "'a \<Rightarrow> bool" |
2472 obtain P' where [transfer_rule]: "(A ===> op =) P P'" |
2472 obtain P' where [transfer_rule]: "(A ===> op =) P P'" |
2475 and "eventually P F' = eventually P' G" by transfer_prover+ |
2475 and "eventually P F' = eventually P' G" by transfer_prover+ |
2476 thus "eventually P F = eventually P F'" by simp |
2476 thus "eventually P F = eventually P F'" by simp |
2477 qed |
2477 qed |
2478 qed |
2478 qed |
2479 |
2479 |
2480 lemma right_unique_filter_rel [transfer_rule]: |
2480 lemma right_unique_rel_filter [transfer_rule]: |
2481 "right_unique A \<Longrightarrow> right_unique (filter_rel A)" |
2481 "right_unique A \<Longrightarrow> right_unique (rel_filter A)" |
2482 using left_unique_filter_rel[of "A\<inverse>\<inverse>"] by simp |
2482 using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2483 |
2483 |
2484 lemma bi_unique_filter_rel [transfer_rule]: |
2484 lemma bi_unique_rel_filter [transfer_rule]: |
2485 "bi_unique A \<Longrightarrow> bi_unique (filter_rel A)" |
2485 "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)" |
2486 by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel) |
2486 by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter) |
2487 |
2487 |
2488 lemma top_filter_parametric [transfer_rule]: |
2488 lemma top_filter_parametric [transfer_rule]: |
2489 "bi_total A \<Longrightarrow> (filter_rel A) top top" |
2489 "bi_total A \<Longrightarrow> (rel_filter A) top top" |
2490 by(simp add: filter_rel_eventually All_transfer) |
2490 by(simp add: rel_filter_eventually All_transfer) |
2491 |
2491 |
2492 lemma bot_filter_parametric [transfer_rule]: "(filter_rel A) bot bot" |
2492 lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot" |
2493 by(simp add: filter_rel_eventually fun_rel_def) |
2493 by(simp add: rel_filter_eventually fun_rel_def) |
2494 |
2494 |
2495 lemma sup_filter_parametric [transfer_rule]: |
2495 lemma sup_filter_parametric [transfer_rule]: |
2496 "(filter_rel A ===> filter_rel A ===> filter_rel A) sup sup" |
2496 "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup" |
2497 by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD) |
2497 by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD) |
2498 |
2498 |
2499 lemma Sup_filter_parametric [transfer_rule]: |
2499 lemma Sup_filter_parametric [transfer_rule]: |
2500 "(rel_set (filter_rel A) ===> filter_rel A) Sup Sup" |
2500 "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup" |
2501 proof(rule fun_relI) |
2501 proof(rule fun_relI) |
2502 fix S T |
2502 fix S T |
2503 assume [transfer_rule]: "rel_set (filter_rel A) S T" |
2503 assume [transfer_rule]: "rel_set (rel_filter A) S T" |
2504 show "filter_rel A (Sup S) (Sup T)" |
2504 show "rel_filter A (Sup S) (Sup T)" |
2505 by(simp add: filter_rel_eventually eventually_Sup) transfer_prover |
2505 by(simp add: rel_filter_eventually eventually_Sup) transfer_prover |
2506 qed |
2506 qed |
2507 |
2507 |
2508 lemma principal_parametric [transfer_rule]: |
2508 lemma principal_parametric [transfer_rule]: |
2509 "(rel_set A ===> filter_rel A) principal principal" |
2509 "(rel_set A ===> rel_filter A) principal principal" |
2510 proof(rule fun_relI) |
2510 proof(rule fun_relI) |
2511 fix S S' |
2511 fix S S' |
2512 assume [transfer_rule]: "rel_set A S S'" |
2512 assume [transfer_rule]: "rel_set A S S'" |
2513 show "filter_rel A (principal S) (principal S')" |
2513 show "rel_filter A (principal S) (principal S')" |
2514 by(simp add: filter_rel_eventually eventually_principal) transfer_prover |
2514 by(simp add: rel_filter_eventually eventually_principal) transfer_prover |
2515 qed |
2515 qed |
2516 |
2516 |
2517 context |
2517 context |
2518 fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool" |
2518 fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool" |
2519 assumes [transfer_rule]: "bi_unique A" |
2519 assumes [transfer_rule]: "bi_unique A" |
2520 begin |
2520 begin |
2521 |
2521 |
2522 lemma le_filter_parametric [transfer_rule]: |
2522 lemma le_filter_parametric [transfer_rule]: |
2523 "(filter_rel A ===> filter_rel A ===> op =) op \<le> op \<le>" |
2523 "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>" |
2524 unfolding le_filter_def[abs_def] by transfer_prover |
2524 unfolding le_filter_def[abs_def] by transfer_prover |
2525 |
2525 |
2526 lemma less_filter_parametric [transfer_rule]: |
2526 lemma less_filter_parametric [transfer_rule]: |
2527 "(filter_rel A ===> filter_rel A ===> op =) op < op <" |
2527 "(rel_filter A ===> rel_filter A ===> op =) op < op <" |
2528 unfolding less_filter_def[abs_def] by transfer_prover |
2528 unfolding less_filter_def[abs_def] by transfer_prover |
2529 |
2529 |
2530 context |
2530 context |
2531 assumes [transfer_rule]: "bi_total A" |
2531 assumes [transfer_rule]: "bi_total A" |
2532 begin |
2532 begin |
2533 |
2533 |
2534 lemma Inf_filter_parametric [transfer_rule]: |
2534 lemma Inf_filter_parametric [transfer_rule]: |
2535 "(rel_set (filter_rel A) ===> filter_rel A) Inf Inf" |
2535 "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf" |
2536 unfolding Inf_filter_def[abs_def] by transfer_prover |
2536 unfolding Inf_filter_def[abs_def] by transfer_prover |
2537 |
2537 |
2538 lemma inf_filter_parametric [transfer_rule]: |
2538 lemma inf_filter_parametric [transfer_rule]: |
2539 "(filter_rel A ===> filter_rel A ===> filter_rel A) inf inf" |
2539 "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf" |
2540 proof(intro fun_relI)+ |
2540 proof(intro fun_relI)+ |
2541 fix F F' G G' |
2541 fix F F' G G' |
2542 assume [transfer_rule]: "filter_rel A F F'" "filter_rel A G G'" |
2542 assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'" |
2543 have "filter_rel A (Inf {F, G}) (Inf {F', G'})" by transfer_prover |
2543 have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover |
2544 thus "filter_rel A (inf F G) (inf F' G')" by simp |
2544 thus "rel_filter A (inf F G) (inf F' G')" by simp |
2545 qed |
2545 qed |
2546 |
2546 |
2547 end |
2547 end |
2548 |
2548 |
2549 end |
2549 end |