14 Var "name" |
14 Var "name" |
15 | Fun "t" "t" |
15 | Fun "t" "t" |
16 and tyS = |
16 and tyS = |
17 All xs::"name set" ty::"t" bind xs in ty |
17 All xs::"name set" ty::"t" bind xs in ty |
18 |
18 |
19 thm t_tyS_fv |
19 thm t_tyS.fv |
20 thm t_tyS_eq_iff |
20 thm t_tyS.eq_iff |
21 thm t_tyS_bn |
21 thm t_tyS.bn |
22 thm t_tyS_perm |
22 thm t_tyS.perm |
23 thm t_tyS_induct |
23 thm t_tyS.induct |
24 thm t_tyS_distinct |
24 thm t_tyS.distinct |
25 |
25 |
26 lemma |
26 lemma |
27 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
27 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
28 apply(simp add: t_tyS_eq_iff) |
28 apply(simp add: t_tyS.eq_iff) |
29 apply(rule_tac x="0::perm" in exI) |
29 apply(rule_tac x="0::perm" in exI) |
30 apply(simp add: alpha_gen) |
30 apply(simp add: alpha_gen) |
31 apply(auto) |
31 apply(auto) |
32 apply(simp add: fresh_star_def fresh_zero_perm) |
32 apply(simp add: fresh_star_def fresh_zero_perm) |
33 done |
33 done |
34 |
34 |
35 lemma |
35 lemma |
36 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
36 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
37 apply(simp add: t_tyS_eq_iff) |
37 apply(simp add: t_tyS.eq_iff) |
38 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
38 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
39 apply(simp add: alpha_gen fresh_star_def eqvts) |
39 apply(simp add: alpha_gen fresh_star_def eqvts) |
40 apply auto |
40 apply auto |
41 done |
41 done |
42 |
42 |
43 lemma |
43 lemma |
44 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
44 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
45 apply(simp add: t_tyS_eq_iff) |
45 apply(simp add: t_tyS.eq_iff) |
46 apply(rule_tac x="0::perm" in exI) |
46 apply(rule_tac x="0::perm" in exI) |
47 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff) |
47 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
48 oops |
48 oops |
49 |
49 |
50 lemma |
50 lemma |
51 assumes a: "a \<noteq> b" |
51 assumes a: "a \<noteq> b" |
52 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
52 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
53 using a |
53 using a |
54 apply(simp add: t_tyS_eq_iff) |
54 apply(simp add: t_tyS.eq_iff) |
55 apply(clarify) |
55 apply(clarify) |
56 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff) |
56 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
57 apply auto |
57 apply auto |
58 done |
58 done |
59 |
59 |
60 end |
60 end |