equal
deleted
inserted
replaced
17 (string * term * mixfix) list -> thm list -> local_theory -> local_theory |
17 (string * term * mixfix) list -> thm list -> local_theory -> local_theory |
18 |
18 |
19 val define_qsizes: typ list -> string list -> (string * sort) list -> |
19 val define_qsizes: typ list -> string list -> (string * sort) list -> |
20 (string * term * mixfix) list -> local_theory -> local_theory |
20 (string * term * mixfix) list -> local_theory -> local_theory |
21 |
21 |
22 val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm |
22 val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context |
23 end |
23 end |
24 |
24 |
25 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
25 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
26 struct |
26 struct |
27 |
27 |
47 |
47 |
48 |
48 |
49 (* defines the quotient permutations and proves pt-class *) |
49 (* defines the quotient permutations and proves pt-class *) |
50 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
50 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
51 let |
51 let |
52 val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys)) |
|
53 |
|
54 val lthy1 = |
52 val lthy1 = |
55 lthy |
53 lthy |
56 |> Local_Theory.exit_global |
54 |> Local_Theory.exit_global |
57 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
55 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
58 |
56 |
120 val trm' = Term.map_abs_vars unraw_str trm |
118 val trm' = Term.map_abs_vars unraw_str trm |
121 in |
119 in |
122 Thm.rename_boundvars trm trm' th |
120 Thm.rename_boundvars trm trm' th |
123 end |
121 end |
124 |
122 |
125 fun lift_thm ctxt qtys simps thm = |
123 fun lift_thms qtys simps thms ctxt = |
126 thm |
124 (map (Quotient_Tacs.lifted ctxt qtys simps |
127 |> Quotient_Tacs.lifted ctxt qtys simps |
125 #> unraw_bounds_thm |
128 |> unraw_bounds_thm |
126 #> unraw_vars_thm |
129 |> unraw_vars_thm |
127 #> Drule.zero_var_indexes) thms, ctxt) |
130 |> Drule.zero_var_indexes |
128 |
131 |
129 |
132 end (* structure *) |
130 end (* structure *) |
133 |
131 |