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 t_tyS_fv fresh_star_def t_tyS_perm 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 t_tyS_fv fresh_star_def t_tyS_perm 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 t_tyS_fv fresh_star_def t_tyS_perm 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 |