equal
deleted
inserted
replaced
1074 All "name set" "ty" |
1074 All "name set" "ty" |
1075 |
1075 |
1076 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
1076 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
1077 print_theorems |
1077 print_theorems |
1078 |
1078 |
1079 abbreviation |
|
1080 "atoms xs \<equiv> {atom x| x. x \<in> xs}" |
|
1081 |
|
1082 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} |
1079 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} |
1083 print_theorems |
1080 print_theorems |
1084 |
1081 |
1085 (* |
1082 (* |
1086 doesn't work yet |
1083 Doesnot work yet since we do not refer to fv_ty |
1087 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
1084 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
1088 print_theorems |
1085 print_theorems |
1089 *) |
1086 *) |
1090 |
1087 |
1091 primrec |
1088 primrec |
1092 fv_tyS |
1089 fv_tyS |
1093 where |
1090 where |
1094 "fv_tyS (All xs T) = (fv_ty T - atoms xs)" |
1091 "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" |
1095 |
1092 |
1096 inductive |
1093 inductive |
1097 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
1094 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
1098 where |
1095 where |
1099 a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2)) |
1096 a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) |
1100 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
1097 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
1101 |
1098 |
1102 lemma |
1099 lemma |
1103 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
1100 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
1104 apply(rule a1) |
1101 apply(rule a1) |