1 theory TypeSchemes |
1 theory TypeSchemes |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = alpha_type := AlphaRes *} |
|
10 |
|
11 nominal_datatype ty = |
9 nominal_datatype ty = |
12 Var "name" |
10 Var "name" |
13 | Fun "ty" "ty" |
11 | Fun "ty" "ty" |
14 and tys = |
12 and tys = |
15 All xs::"name fset" ty::"ty" bind xs in ty |
13 All xs::"name fset" ty::"ty" bind_res xs in ty |
16 |
14 |
17 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
15 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
18 |
16 |
19 (* below we define manually the function for size *) |
17 (* below we define manually the function for size *) |
20 |
18 |
123 lemma |
121 lemma |
124 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
122 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
125 apply(simp add: ty_tys.eq_iff) |
123 apply(simp add: ty_tys.eq_iff) |
126 apply(rule_tac x="0::perm" in exI) |
124 apply(rule_tac x="0::perm" in exI) |
127 apply(simp add: alphas) |
125 apply(simp add: alphas) |
128 apply(simp add: fresh_star_def fresh_zero_perm) |
126 apply(simp add: fresh_star_def fresh_zero_perm supp_at_base) |
129 done |
127 done |
130 |
128 |
131 lemma |
129 lemma |
132 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
130 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
133 apply(simp add: ty_tys.eq_iff) |
131 apply(simp add: ty_tys.eq_iff) |
134 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
132 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
135 apply(simp add: alphas fresh_star_def eqvts) |
133 apply(simp add: alphas fresh_star_def eqvts supp_at_base) |
136 done |
134 done |
137 |
135 |
138 lemma |
136 lemma |
139 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
137 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
140 apply(simp add: ty_tys.eq_iff) |
138 apply(simp add: ty_tys.eq_iff) |
141 apply(rule_tac x="0::perm" in exI) |
139 apply(rule_tac x="0::perm" in exI) |
142 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff) |
140 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base) |
143 done |
141 done |
144 |
142 |
145 lemma |
143 lemma |
146 assumes a: "a \<noteq> b" |
144 assumes a: "a \<noteq> b" |
147 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
145 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
148 using a |
146 using a |
149 apply(simp add: ty_tys.eq_iff) |
147 apply(simp add: ty_tys.eq_iff) |
150 apply(clarify) |
148 apply(clarify) |
151 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff) |
149 apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base) |
152 apply auto |
150 apply auto |
153 done |
151 done |
154 |
152 |
155 (* PROBLEM: |
153 (* PROBLEM: |
156 Type schemes with separate datatypes |
154 Type schemes with separate datatypes |