equal
deleted
inserted
replaced
17 thm list -> local_theory -> local_theory |
17 thm list -> local_theory -> local_theory |
18 |
18 |
19 val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> |
19 val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> |
20 local_theory -> local_theory |
20 local_theory -> local_theory |
21 |
21 |
22 val lift_thm: Proof.context -> typ list -> thm -> thm |
22 val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm |
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 |
54 |> Local_Theory.exit_global |
54 |> Local_Theory.exit_global |
55 |> Class.instantiation (qfull_ty_names, [], @{sort pt}) |
55 |> Class.instantiation (qfull_ty_names, [], @{sort pt}) |
56 |
56 |
57 val (_, lthy'') = define_qconsts qtys perm_specs lthy' |
57 val (_, lthy'') = define_qconsts qtys perm_specs lthy' |
58 |
58 |
59 val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys) raw_perm_laws |
59 val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys []) raw_perm_laws |
60 |
60 |
61 fun tac _ = |
61 fun tac _ = |
62 Class.intro_classes_tac [] THEN |
62 Class.intro_classes_tac [] THEN |
63 (ALLGOALS (resolve_tac lifted_perm_laws)) |
63 (ALLGOALS (resolve_tac lifted_perm_laws)) |
64 in |
64 in |
104 val trm' = Term.map_abs_vars unraw_str trm |
104 val trm' = Term.map_abs_vars unraw_str trm |
105 in |
105 in |
106 Thm.rename_boundvars trm trm' th |
106 Thm.rename_boundvars trm trm' th |
107 end |
107 end |
108 |
108 |
109 fun lift_thm ctxt qtys thm = |
109 fun lift_thm ctxt qtys simps thm = |
110 Quotient_Tacs.lifted ctxt qtys thm |
110 thm |
|
111 |> Quotient_Tacs.lifted ctxt qtys simps |
111 |> unraw_bounds_thm |
112 |> unraw_bounds_thm |
112 |> unraw_vars_thm |
113 |> unraw_vars_thm |
113 |
114 |
114 |
115 |
115 end (* structure *) |
116 end (* structure *) |