equal
deleted
inserted
replaced
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l |
10 | Lam x::"name" l::"lam" bind x in l |
11 |
11 |
12 definition |
12 definition |
13 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
13 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
|
14 |
|
15 lemma supp_eqvt_at: |
|
16 assumes asm: "eqvt_at f x" |
|
17 and fin: "finite (supp x)" |
|
18 shows "supp (f x) \<subseteq> supp x" |
|
19 apply(rule supp_is_subset) |
|
20 unfolding supports_def |
|
21 unfolding fresh_def[symmetric] |
|
22 using asm |
|
23 apply(simp add: eqvt_at_def) |
|
24 apply(simp add: swap_fresh_fresh) |
|
25 apply(rule fin) |
|
26 done |
|
27 |
14 |
28 |
15 definition |
29 definition |
16 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
30 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
17 |
31 |
18 lemma eqvtI: |
32 lemma eqvtI: |
498 (exactly_one, function_value) |
512 (exactly_one, function_value) |
499 end |
513 end |
500 *} |
514 *} |
501 |
515 |
502 ML Thm.forall_elim_vars |
516 ML Thm.forall_elim_vars |
|
517 ML Thm.implies_intr |
503 |
518 |
504 ML {* (ex1_implies_ex, ex1_implies_un) *} |
519 ML {* (ex1_implies_ex, ex1_implies_un) *} |
505 thm fundef_ex1_eqvt_at |
520 thm fundef_ex1_eqvt_at |
506 |
521 |
507 ML {* |
522 ML {* |