68 @{thms rkind.distinct rty.distinct rtrm.distinct} |
68 @{thms rkind.distinct rty.distinct rtrm.distinct} |
69 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
69 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
70 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
70 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
71 thm alpha_equivps |
71 thm alpha_equivps |
72 |
72 |
73 quotient_type kind = rkind / alpha_rkind |
73 local_setup {* define_quotient_type |
74 by (rule alpha_equivps) |
74 [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})), |
75 |
75 (([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )), |
76 quotient_type |
76 (([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))] |
77 ty = rty / alpha_rty and |
77 (ALLGOALS (resolve_tac @{thms alpha_equivps})) |
78 trm = rtrm / alpha_rtrm |
78 *} |
79 by (auto intro: alpha_equivps) |
79 |
80 |
80 local_setup {* |
81 quotient_definition |
81 (fn ctxt => ctxt |
82 "TYP :: kind" |
82 |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type})) |
83 is |
83 |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi})) |
84 "Type" |
84 |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst})) |
85 |
85 |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp})) |
86 quotient_definition |
86 |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi})) |
87 "KPI :: ty \<Rightarrow> name \<Rightarrow> kind \<Rightarrow> kind" |
87 |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const})) |
88 is |
88 |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var})) |
89 "KPi" |
89 |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App})) |
90 |
90 |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam})) |
91 quotient_definition |
91 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
92 "TCONST :: ident \<Rightarrow> ty" |
92 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
93 is |
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
94 "TConst" |
94 print_theorems |
95 |
|
96 quotient_definition |
|
97 "TAPP :: ty \<Rightarrow> trm \<Rightarrow> ty" |
|
98 is |
|
99 "TApp" |
|
100 |
|
101 quotient_definition |
|
102 "TPI :: ty \<Rightarrow> name \<Rightarrow> ty \<Rightarrow> ty" |
|
103 is |
|
104 "TPi" |
|
105 |
|
106 (* FIXME: does not work with CONST *) |
|
107 quotient_definition |
|
108 "CONS :: ident \<Rightarrow> trm" |
|
109 is |
|
110 "Const" |
|
111 |
|
112 quotient_definition |
|
113 "VAR :: name \<Rightarrow> trm" |
|
114 is |
|
115 "Var" |
|
116 |
|
117 quotient_definition |
|
118 "APP :: trm \<Rightarrow> trm \<Rightarrow> trm" |
|
119 is |
|
120 "App" |
|
121 |
|
122 quotient_definition |
|
123 "LAM :: ty \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" |
|
124 is |
|
125 "Lam" |
|
126 |
|
127 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *) |
|
128 quotient_definition |
|
129 "fv_kind :: kind \<Rightarrow> atom set" |
|
130 is |
|
131 "fv_rkind" |
|
132 |
|
133 quotient_definition |
|
134 "fv_ty :: ty \<Rightarrow> atom set" |
|
135 is |
|
136 "fv_rty" |
|
137 |
|
138 quotient_definition |
|
139 "fv_trm :: trm \<Rightarrow> atom set" |
|
140 is |
|
141 "fv_rtrm" |
|
142 |
95 |
143 lemma alpha_rfv: |
96 lemma alpha_rfv: |
144 shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and> |
97 shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and> |
145 (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and> |
98 (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and> |
146 (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)" |
99 (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)" |