59 apply(induct T and S rule: t_tyS_inducts) |
59 apply(induct T and S rule: t_tyS_inducts) |
60 apply(simp_all add: t_tyS_fv) |
60 apply(simp_all add: t_tyS_fv) |
61 (* VarTS case *) |
61 (* VarTS case *) |
62 apply(simp only: supp_def) |
62 apply(simp only: supp_def) |
63 apply(simp only: t_tyS_perm) |
63 apply(simp only: t_tyS_perm) |
64 apply(simp only: t_tyS_inject) |
64 apply(simp only: t_tyS_eq_iff) |
65 apply(simp only: supp_def[symmetric]) |
65 apply(simp only: supp_def[symmetric]) |
66 apply(simp only: supp_at_base) |
66 apply(simp only: supp_at_base) |
67 (* FunTS case *) |
67 (* FunTS case *) |
68 apply(simp only: supp_def) |
68 apply(simp only: supp_def) |
69 apply(simp only: t_tyS_perm) |
69 apply(simp only: t_tyS_perm) |
70 apply(simp only: t_tyS_inject) |
70 apply(simp only: t_tyS_eq_iff) |
71 apply(simp only: de_Morgan_conj) |
71 apply(simp only: de_Morgan_conj) |
72 apply(simp only: Collect_disj_eq) |
72 apply(simp only: Collect_disj_eq) |
73 apply(simp only: infinite_Un) |
73 apply(simp only: infinite_Un) |
74 apply(simp only: Collect_disj_eq) |
74 apply(simp only: Collect_disj_eq) |
75 (* All case *) |
75 (* All case *) |
76 apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) |
76 apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst) |
77 apply(simp (no_asm) only: supp_def) |
77 apply(simp (no_asm) only: supp_def) |
78 apply(simp only: t_tyS_perm) |
78 apply(simp only: t_tyS_perm) |
79 apply(simp only: permute_ABS) |
79 apply(simp only: permute_ABS) |
80 apply(simp only: t_tyS_inject) |
80 apply(simp only: t_tyS_eq_iff) |
81 apply(simp only: Abs_eq_iff) |
81 apply(simp only: Abs_eq_iff) |
82 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
82 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) |
83 apply(simp only: alpha_gen) |
83 apply(simp only: alpha_gen) |
84 apply(simp only: supp_eqvt[symmetric]) |
84 apply(simp only: supp_eqvt[symmetric]) |
85 apply(simp only: eqvts) |
85 apply(simp only: eqvts) |
86 apply(simp only: supp_Abs) |
86 apply(simp only: supp_Abs) |
87 done |
87 done |
88 |
88 |
89 lemma |
89 lemma |
90 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
90 shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))" |
91 apply(simp add: t_tyS_inject) |
91 apply(simp add: t_tyS_eq_iff) |
92 apply(rule_tac x="0::perm" in exI) |
92 apply(rule_tac x="0::perm" in exI) |
93 apply(simp add: alpha_gen) |
93 apply(simp add: alpha_gen) |
94 apply(auto) |
94 apply(auto) |
95 apply(simp add: fresh_star_def fresh_zero_perm) |
95 apply(simp add: fresh_star_def fresh_zero_perm) |
96 done |
96 done |
97 |
97 |
98 lemma |
98 lemma |
99 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
99 shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))" |
100 apply(simp add: t_tyS_inject) |
100 apply(simp add: t_tyS_eq_iff) |
101 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
101 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
102 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) |
102 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts) |
103 apply auto |
103 apply auto |
104 done |
104 done |
105 |
105 |
106 lemma |
106 lemma |
107 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
107 shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))" |
108 apply(simp add: t_tyS_inject) |
108 apply(simp add: t_tyS_eq_iff) |
109 apply(rule_tac x="0::perm" in exI) |
109 apply(rule_tac x="0::perm" in exI) |
110 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) |
110 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff) |
111 oops |
111 oops |
112 |
112 |
113 lemma |
113 lemma |
114 assumes a: "a \<noteq> b" |
114 assumes a: "a \<noteq> b" |
115 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
115 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))" |
116 using a |
116 using a |
117 apply(simp add: t_tyS_inject) |
117 apply(simp add: t_tyS_eq_iff) |
118 apply(clarify) |
118 apply(clarify) |
119 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject) |
119 apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff) |
120 apply auto |
120 apply auto |
121 done |
121 done |
122 |
122 |
123 |
123 |
124 end |
124 end |