27 struct |
27 struct |
28 |
28 |
29 |
29 |
30 (* defines the quotient types *) |
30 (* defines the quotient types *) |
31 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 = |
32 let |
32 let |
33 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 |
34 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
34 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
35 in |
35 in |
36 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
36 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
37 end |
37 end |
38 |
38 |
39 |
39 |
40 (* defines quotient constants *) |
40 (* defines quotient constants *) |
41 fun define_qconsts qtys consts_specs lthy = |
41 fun define_qconsts qtys consts_specs lthy = |
42 let |
42 let |
43 val (qconst_infos, lthy') = |
43 val (qconst_infos, lthy') = |
44 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
44 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
45 val phi = ProofContext.export_morphism lthy' lthy |
45 val phi = ProofContext.export_morphism lthy' lthy |
46 in |
46 in |
47 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
47 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
48 end |
48 end |
49 |
49 |
50 |
50 |
51 (* defines the quotient permutations and proves pt-class *) |
51 (* defines the quotient permutations and proves pt-class *) |
52 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
52 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = |
53 let |
53 let |
54 val lthy1 = |
54 val lthy1 = |
55 lthy |
55 lthy |
56 |> Local_Theory.exit_global |
56 |> Local_Theory.exit_global |
57 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
57 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
58 |
58 |
59 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
59 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
60 |
60 |
61 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
61 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
62 |
62 |
63 val lifted_perm_laws = |
63 val lifted_perm_laws = |
64 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
64 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
65 |> Variable.exportT lthy3 lthy2 |
65 |> Variable.exportT lthy3 lthy2 |
66 |
66 |
67 fun tac _ = |
67 fun tac _ = |
68 Class.intro_classes_tac [] THEN |
68 Class.intro_classes_tac [] THEN |
69 (ALLGOALS (resolve_tac lifted_perm_laws)) |
69 (ALLGOALS (resolve_tac lifted_perm_laws)) |
70 in |
70 in |
71 lthy2 |
71 lthy2 |
72 |> Class.prove_instantiation_exit tac |
72 |> Class.prove_instantiation_exit tac |
73 |> Named_Target.theory_init |
73 |> Named_Target.theory_init |
74 end |
74 end |
75 |
75 |
76 |
76 |
77 (* defines the size functions and proves size-class *) |
77 (* defines the size functions and proves size-class *) |
78 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = |
78 fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = |
79 let |
79 let |
80 fun tac _ = Class.intro_classes_tac [] |
80 val tac = K (Class.intro_classes_tac []) |
81 in |
81 in |
82 lthy |
82 lthy |
83 |> Local_Theory.exit_global |
83 |> Local_Theory.exit_global |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |
85 |> snd o (define_qconsts qtys size_specs) |
85 |> snd o (define_qconsts qtys size_specs) |
86 |> Class.prove_instantiation_exit tac |
86 |> Class.prove_instantiation_exit tac |
87 |> Named_Target.theory_init |
87 |> Named_Target.theory_init |
88 end |
88 end |
89 |
89 |
90 |
90 |
91 (* lifts a theorem and cleans all "_raw" parts |
91 (* lifts a theorem and cleans all "_raw" parts |
92 from variable names *) |
92 from variable names *) |
93 |
93 |
97 val exclude = |
97 val exclude = |
98 Scan.repeat (Scan.unless raw any) --| raw >> implode |
98 Scan.repeat (Scan.unless raw any) --| raw >> implode |
99 val parser = Scan.repeat (exclude || any) |
99 val parser = Scan.repeat (exclude || any) |
100 in |
100 in |
101 fun unraw_str s = |
101 fun unraw_str s = |
102 s |> explode |
102 s |> explode |
103 |> Scan.finite Symbol.stopper parser >> implode |
103 |> Scan.finite Symbol.stopper parser >> implode |
104 |> fst |
104 |> fst |
105 end |
105 end |
106 |
106 |
107 fun unraw_vars_thm thm = |
107 fun unraw_vars_thm thm = |
108 let |
108 let |
109 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) |
110 |
110 |
111 val vars = Term.add_vars (prop_of thm) [] |
111 val vars = Term.add_vars (prop_of thm) [] |
112 val vars' = map (Var o unraw_var_str) vars |
112 val vars' = map (Var o unraw_var_str) vars |
113 in |
113 in |
114 Thm.certify_instantiate ([], (vars ~~ vars')) thm |
114 Thm.certify_instantiate ([], (vars ~~ vars')) thm |
115 end |
115 end |
116 |
116 |
117 fun unraw_bounds_thm th = |
117 fun unraw_bounds_thm th = |
118 let |
118 let |
119 val trm = Thm.prop_of th |
119 val trm = Thm.prop_of th |
120 val trm' = Term.map_abs_vars unraw_str trm |
120 val trm' = Term.map_abs_vars unraw_str trm |
121 in |
121 in |
122 Thm.rename_boundvars trm trm' th |
122 Thm.rename_boundvars trm trm' th |
123 end |
123 end |
124 |
124 |
125 fun lift_thms qtys simps thms ctxt = |
125 fun lift_thms qtys simps thms ctxt = |
126 (map (Quotient_Tacs.lifted ctxt qtys simps |
126 (map (Quotient_Tacs.lifted ctxt qtys simps |
127 #> unraw_bounds_thm |
127 #> unraw_bounds_thm |
128 #> unraw_vars_thm |
128 #> unraw_vars_thm |