78 quotient_def |
78 quotient_def |
79 fv :: "lam \<Rightarrow> name set" |
79 fv :: "lam \<Rightarrow> name set" |
80 where |
80 where |
81 "fv \<equiv> rfv" |
81 "fv \<equiv> rfv" |
82 |
82 |
83 ML {* |
|
84 local |
|
85 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] |
|
86 fun pp_list xs = Pretty.list "[" "]" xs |
|
87 fun pp_str s = Pretty.str s |
|
88 fun pp_qstr s = Pretty.quote (pp_str s) |
|
89 fun pp_int i = pp_str (string_of_int i) |
|
90 fun pp_sort S = pp_list (map pp_qstr S) |
|
91 fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args] |
|
92 in |
|
93 fun raw_pp_typ (TVar ((a, i), S)) = |
|
94 pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S)) |
|
95 | raw_pp_typ (TFree (a, S)) = |
|
96 pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) |
|
97 | raw_pp_typ (Type (a, tys)) = |
|
98 pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) |
|
99 end *} |
|
100 |
|
101 ML {* |
|
102 PolyML.addPrettyPrinter |
|
103 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ) |
|
104 |
|
105 *} |
|
106 |
|
107 typ "name set" |
|
108 typ "name => bool" |
|
109 |
|
110 ML {* @{typ "name set"} *} |
|
111 |
|
112 thm fv_def |
83 thm fv_def |
113 |
84 |
114 (* definition of overloaded permutation function *) |
85 (* definition of overloaded permutation function *) |
115 (* for the lifted type lam *) |
86 (* for the lifted type lam *) |
116 overloading |
87 overloading |
201 ML {* val qty = @{typ "lam"} *} |
172 ML {* val qty = @{typ "lam"} *} |
202 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
203 |
174 |
204 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
205 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
206 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *} |
177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t *} |
207 |
178 |
208 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
209 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
210 done |
181 done |
211 |
182 |