equal
deleted
inserted
replaced
1 (* Title: nominal_dt_alpha.ML |
1 (* Title: nominal_dt_alpha.ML |
2 Author: Christian Urban |
2 Author: Christian Urban |
3 Author: Cezary Kaliszyk |
3 Author: Cezary Kaliszyk |
4 |
4 |
5 Performing quotient constructions |
5 Performing quotient constructions and lifting theorems |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_QUOT = |
8 signature NOMINAL_DT_QUOT = |
9 sig |
9 sig |
10 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
10 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
16 val define_qperms: typ list -> string list -> (string * term * mixfix) list -> |
16 val define_qperms: typ list -> string list -> (string * term * mixfix) list -> |
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 |
|
22 val lift_thm: typ list -> Proof.context -> thm -> thm |
21 end |
23 end |
22 |
24 |
23 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
25 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
24 struct |
26 struct |
25 |
27 |
77 |> snd o (define_qconsts qtys size_specs) |
79 |> snd o (define_qconsts qtys size_specs) |
78 |> Class.prove_instantiation_exit tac |
80 |> Class.prove_instantiation_exit tac |
79 |> Named_Target.theory_init |
81 |> Named_Target.theory_init |
80 end |
82 end |
81 |
83 |
|
84 |
|
85 (* lifts a theorem and deletes all "_raw" suffixes *) |
|
86 |
|
87 fun unraw_str s = |
|
88 unsuffix "_raw" s |
|
89 handle Fail _ => s |
|
90 |
|
91 fun unraw_vars_thm thm = |
|
92 let |
|
93 fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) |
|
94 |
|
95 val vars = Term.add_vars (prop_of thm) [] |
|
96 val vars' = map (Var o unraw_var_str) vars |
|
97 in |
|
98 Thm.certify_instantiate ([], (vars ~~ vars')) thm |
|
99 end |
|
100 |
|
101 fun unraw_bounds_thm th = |
|
102 let |
|
103 val trm = Thm.prop_of th |
|
104 val trm' = Term.map_abs_vars unraw_str trm |
|
105 in |
|
106 Thm.rename_boundvars trm trm' th |
|
107 end |
|
108 |
|
109 fun lift_thm qtys ctxt thm = |
|
110 Quotient_Tacs.lifted qtys ctxt thm |
|
111 |> unraw_bounds_thm |
|
112 |> unraw_vars_thm |
|
113 |
|
114 |
82 end (* structure *) |
115 end (* structure *) |
83 |
116 |