11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
12 |
12 |
13 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
13 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
14 Quotient_Info.qconsts_info list * local_theory |
14 Quotient_Info.qconsts_info list * local_theory |
15 |
15 |
16 val define_qperms: typ list -> string list -> (string * term * mixfix) list -> |
16 val define_qperms: typ list -> string list -> (string * sort) list -> |
17 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 * term * mixfix) list -> |
19 val define_qsizes: typ list -> string list -> (string * sort) list -> |
20 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_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 = |
45 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
45 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
46 end |
46 end |
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 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 lthy' = |
52 val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys)) |
|
53 |
|
54 val lthy1 = |
53 lthy |
55 lthy |
54 |> Local_Theory.exit_global |
56 |> Local_Theory.exit_global |
55 |> Class.instantiation (qfull_ty_names, [], @{sort pt}) |
57 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
56 |
58 |
57 val (_, lthy'') = define_qconsts qtys perm_specs lthy' |
59 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
58 |
60 |
59 val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys []) raw_perm_laws |
61 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
|
62 |
|
63 val lifted_perm_laws = |
|
64 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
|
65 |> Variable.exportT lthy3 lthy2 |
60 |
66 |
61 fun tac _ = |
67 fun tac _ = |
62 Class.intro_classes_tac [] THEN |
68 Class.intro_classes_tac [] THEN |
63 (ALLGOALS (resolve_tac lifted_perm_laws)) |
69 (ALLGOALS (resolve_tac lifted_perm_laws)) |
64 in |
70 in |
65 lthy'' |
71 lthy2 |
66 |> Class.prove_instantiation_exit tac |
72 |> Class.prove_instantiation_exit tac |
67 |> Named_Target.theory_init |
73 |> Named_Target.theory_init |
68 end |
74 end |
69 |
75 |
70 |
76 |
71 (* defines the size functions and proves size-class *) |
77 (* defines the size functions and proves size-class *) |
72 fun define_qsizes qtys qfull_ty_names size_specs lthy = |
78 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = |
73 let |
79 let |
74 fun tac _ = Class.intro_classes_tac [] |
80 fun tac _ = Class.intro_classes_tac [] |
75 in |
81 in |
76 lthy |
82 lthy |
77 |> Local_Theory.exit_global |
83 |> Local_Theory.exit_global |
78 |> Class.instantiation (qfull_ty_names, [], @{sort size}) |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |
79 |> snd o (define_qconsts qtys size_specs) |
85 |> snd o (define_qconsts qtys size_specs) |
80 |> Class.prove_instantiation_exit tac |
86 |> Class.prove_instantiation_exit tac |
81 |> Named_Target.theory_init |
87 |> Named_Target.theory_init |
82 end |
88 end |
83 |
89 |
84 |
90 |
85 (* lifts a theorem and deletes all "_raw" suffixes *) |
91 (* lifts a theorem and cleans all "_raw" instances |
|
92 from variable names *) |
86 |
93 |
87 fun unraw_str s = |
94 local |
88 unsuffix "_raw" s |
95 val any = Scan.one (Symbol.not_eof) |
89 handle Fail _ => s |
96 val raw = Scan.this_string "_raw" |
|
97 val exclude = |
|
98 Scan.repeat (Scan.unless raw any) --| raw >> implode |
|
99 val parser = Scan.repeat (exclude || any) |
|
100 in |
|
101 fun unraw_str s = |
|
102 s |> explode |
|
103 |> Scan.finite Symbol.stopper parser >> implode |
|
104 |> fst |
|
105 end |
90 |
106 |
91 fun unraw_vars_thm thm = |
107 fun unraw_vars_thm thm = |
92 let |
108 let |
93 fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) |
109 fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) |
94 |
110 |