equal
deleted
inserted
replaced
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
|
24 typ trm |
|
25 typ assg |
24 term Var |
26 term Var |
25 term App |
27 term App |
26 term Baz |
28 term Baz |
27 term bn |
29 term bn |
28 term fv_trm |
30 term fv_trm |
|
31 |
|
32 lemma [quot_respect]: |
|
33 "(op = ===> alpha_trm_raw) Var_raw Var_raw" |
|
34 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
|
35 apply(auto) |
|
36 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
37 apply(rule refl) |
|
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
39 apply(assumption) |
|
40 apply(assumption) |
|
41 done |
|
42 |
|
43 |
|
44 |
|
45 lemma "Var x \<noteq> App y1 y2" |
|
46 apply(descending) |
|
47 apply(simp add: trm_raw.distinct) |
|
48 |
|
49 |
|
50 |
|
51 ML {* |
|
52 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.distinct(1)} |
|
53 *} |
|
54 |
|
55 |
29 |
56 |
30 |
57 |
31 typ trm |
58 typ trm |
32 typ assg |
59 typ assg |
33 |
60 |