91 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
91 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
92 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
92 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
94 print_theorems |
94 print_theorems |
95 |
95 |
96 lemma alpha_rfv: |
96 local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
97 shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and> |
97 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
98 (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and> |
|
99 (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)" |
|
100 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) |
|
101 apply(simp_all add: alpha_gen) |
|
102 done |
|
103 |
98 |
104 lemma perm_rsp[quot_respect]: |
99 lemma perm_rsp[quot_respect]: |
105 "(op = ===> alpha_rkind ===> alpha_rkind) permute permute" |
100 "(op = ===> alpha_rkind ===> alpha_rkind) permute permute" |
106 "(op = ===> alpha_rty ===> alpha_rty) permute permute" |
101 "(op = ===> alpha_rty ===> alpha_rty) permute permute" |
107 "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute" |
102 "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute" |
126 lemma kpi_rsp[quot_respect]: |
121 lemma kpi_rsp[quot_respect]: |
127 "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi" |
122 "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi" |
128 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
123 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
129 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all |
124 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all |
130 apply (rule_tac x="0" in exI) |
125 apply (rule_tac x="0" in exI) |
131 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) |
126 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
132 done |
127 done |
133 |
128 |
134 lemma tpi_rsp[quot_respect]: |
129 lemma tpi_rsp[quot_respect]: |
135 "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi" |
130 "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi" |
136 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
131 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
137 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all |
132 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all |
138 apply (rule_tac x="0" in exI) |
133 apply (rule_tac x="0" in exI) |
139 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) |
134 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
140 done |
135 done |
141 lemma lam_rsp[quot_respect]: |
136 lemma lam_rsp[quot_respect]: |
142 "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam" |
137 "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam" |
143 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
138 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
144 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all |
139 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all |
145 apply (rule_tac x="0" in exI) |
140 apply (rule_tac x="0" in exI) |
146 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) |
141 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
147 done |
142 done |
148 |
|
149 lemma fv_rty_rsp[quot_respect]: |
|
150 "(alpha_rty ===> op =) fv_rty fv_rty" |
|
151 by (simp add: alpha_rfv) |
|
152 lemma fv_rkind_rsp[quot_respect]: |
|
153 "(alpha_rkind ===> op =) fv_rkind fv_rkind" |
|
154 by (simp add: alpha_rfv) |
|
155 lemma fv_rtrm_rsp[quot_respect]: |
|
156 "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm" |
|
157 by (simp add: alpha_rfv) |
|
158 |
143 |
159 thm rkind_rty_rtrm.induct |
144 thm rkind_rty_rtrm.induct |
160 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
145 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
161 |
146 |
162 thm rkind_rty_rtrm.inducts |
147 thm rkind_rty_rtrm.inducts |