equal
deleted
inserted
replaced
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_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context |
22 val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context |
|
23 |
23 end |
24 end |
24 |
25 |
25 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
26 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
26 struct |
27 struct |
|
28 |
27 |
29 |
28 (* defines the quotient types *) |
30 (* defines the quotient types *) |
29 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
31 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
30 let |
32 let |
31 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
33 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
84 |> Class.prove_instantiation_exit tac |
86 |> Class.prove_instantiation_exit tac |
85 |> Named_Target.theory_init |
87 |> Named_Target.theory_init |
86 end |
88 end |
87 |
89 |
88 |
90 |
89 (* lifts a theorem and cleans all "_raw" instances |
91 (* lifts a theorem and cleans all "_raw" parts |
90 from variable names *) |
92 from variable names *) |
91 |
93 |
92 local |
94 local |
93 val any = Scan.one (Symbol.not_eof) |
95 val any = Scan.one (Symbol.not_eof) |
94 val raw = Scan.this_string "_raw" |
96 val raw = Scan.this_string "_raw" |
124 (map (Quotient_Tacs.lifted ctxt qtys simps |
126 (map (Quotient_Tacs.lifted ctxt qtys simps |
125 #> unraw_bounds_thm |
127 #> unraw_bounds_thm |
126 #> unraw_vars_thm |
128 #> unraw_vars_thm |
127 #> Drule.zero_var_indexes) thms, ctxt) |
129 #> Drule.zero_var_indexes) thms, ctxt) |
128 |
130 |
129 |
|
130 end (* structure *) |
131 end (* structure *) |
131 |
132 |