author | kuncar |
Mon, 23 Apr 2012 17:18:18 +0200 | |
changeset 47698 | 18202d3d5832 |
parent 47504 | aa1b8a59017f |
child 47938 | 2924f37cb6b3 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Quotient/quotient_def.ML |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
35788 | 4 |
Definitions for constants on quotient types. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
signature QUOTIENT_DEF = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
sig |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
9 |
val add_quotient_def: |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
10 |
((binding * mixfix) * Attrib.binding) * (term * term) -> thm -> |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
11 |
local_theory -> Quotient_Info.quotconsts * local_theory |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
12 |
|
45598 | 13 |
val quotient_def: |
14 |
(binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> |
|
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
15 |
local_theory -> Proof.state |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
|
45598 | 17 |
val quotient_def_cmd: |
18 |
(binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> |
|
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
19 |
local_theory -> Proof.state |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
structure Quotient_Def: QUOTIENT_DEF = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
struct |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
(** Interface and Syntax Setup **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
28 |
(* Generation of the code certificate from the rsp theorem *) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
29 |
|
47698 | 30 |
open Lifting_Util |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
31 |
|
47698 | 32 |
infix 0 MRSL |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
33 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
34 |
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
35 |
| get_body_types (U, V) = (U, V) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
36 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
37 |
fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
38 |
| get_binder_types _ = [] |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
39 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
40 |
fun unabs_def ctxt def = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
41 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
42 |
val (_, rhs) = Thm.dest_equals (cprop_of def) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
43 |
fun dest_abs (Abs (var_name, T, _)) = (var_name, T) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
44 |
| dest_abs tm = raise TERM("get_abs_var",[tm]) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
45 |
val (var_name, T) = dest_abs (term_of rhs) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
46 |
val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
47 |
val thy = Proof_Context.theory_of ctxt' |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
48 |
val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T))) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
49 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
50 |
Thm.combination def refl_thm |> |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
51 |
singleton (Proof_Context.export ctxt' ctxt) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
52 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
53 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
54 |
fun unabs_all_def ctxt def = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
55 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
56 |
val (_, rhs) = Thm.dest_equals (cprop_of def) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
57 |
val xs = strip_abs_vars (term_of rhs) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
58 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
59 |
fold (K (unabs_def ctxt)) xs def |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
60 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
61 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
62 |
val map_fun_unfolded = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
63 |
@{thm map_fun_def[abs_def]} |> |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
64 |
unabs_def @{context} |> |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
65 |
unabs_def @{context} |> |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
66 |
Local_Defs.unfold @{context} [@{thm comp_def}] |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
67 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
68 |
fun unfold_fun_maps ctm = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
69 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
70 |
fun unfold_conv ctm = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
71 |
case (Thm.term_of ctm) of |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
72 |
Const (@{const_name "map_fun"}, _) $ _ $ _ => |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
73 |
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
74 |
| _ => Conv.all_conv ctm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
75 |
val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
76 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
77 |
(Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
78 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
79 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
80 |
fun prove_rel ctxt rsp_thm (rty, qty) = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
81 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
82 |
val ty_args = get_binder_types (rty, qty) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
83 |
fun disch_arg args_ty thm = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
84 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47418
diff
changeset
|
85 |
val quot_thm = Quotient_Term.prove_quot_thm ctxt args_ty |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
86 |
in |
47308 | 87 |
[quot_thm, thm] MRSL @{thm apply_rspQ3''} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
88 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
89 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
90 |
fold disch_arg ty_args rsp_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
91 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
92 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
93 |
exception CODE_CERT_GEN of string |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
94 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
95 |
fun simplify_code_eq ctxt def_thm = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
96 |
Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
97 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
98 |
fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
99 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47418
diff
changeset
|
100 |
val quot_thm = Quotient_Term.prove_quot_thm ctxt (get_body_types (rty, qty)) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
101 |
val fun_rel = prove_rel ctxt rsp_thm (rty, qty) |
47308 | 102 |
val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
103 |
val abs_rep_eq = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
104 |
case (HOLogic.dest_Trueprop o prop_of) fun_rel of |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
105 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm |
47308 | 106 |
| Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
107 |
| _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
108 |
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
109 |
val unabs_def = unabs_all_def ctxt unfolded_def |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
110 |
val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
111 |
val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
112 |
val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong} |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
113 |
val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans} |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
114 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
115 |
simplify_code_eq ctxt code_cert |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
116 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
117 |
|
47156 | 118 |
fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
119 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47418
diff
changeset
|
120 |
val quot_thm = Quotient_Term.prove_quot_thm lthy (get_body_types (rty, qty)) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
121 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
122 |
if Quotient_Type.can_generate_code_cert quot_thm then |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
123 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
124 |
val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
125 |
val add_abs_eqn_attribute = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
126 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
127 |
val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
128 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
129 |
lthy |
47156 | 130 |
|> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert]) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
131 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
132 |
else |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
133 |
lthy |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
134 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
135 |
|
47156 | 136 |
fun define_code_eq code_eqn_thm_name def_thm lthy = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
137 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
138 |
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
139 |
val code_eq = unabs_all_def lthy unfolded_def |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
140 |
val simp_code_eq = simplify_code_eq lthy code_eq |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
141 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
142 |
lthy |
47156 | 143 |
|> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
144 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
145 |
|
47156 | 146 |
fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
147 |
if body_type rty = body_type qty then |
47156 | 148 |
define_code_eq code_eqn_thm_name def_thm lthy |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
149 |
else |
47156 | 150 |
define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
151 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
(* The ML-interface for a quotient definition takes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
as argument: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
- an optional binding and mixfix annotation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
- attributes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
- the new constant as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
- the rhs of the definition as term |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
159 |
- respectfulness theorem for the rhs |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
|
45279 | 161 |
It stores the qconst_info in the quotconsts data slot. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
|
41444 | 163 |
Restriction: At the moment the left- and right-hand |
164 |
side of the definition must be a constant. |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
*) |
41444 | 166 |
fun error_msg bind str = |
167 |
let |
|
168 |
val name = Binding.name_of bind |
|
169 |
val pos = Position.str_of (Binding.pos_of bind) |
|
170 |
in |
|
171 |
error ("Head of quotient_definition " ^ |
|
172 |
quote str ^ " differs from declaration " ^ name ^ pos) |
|
173 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
|
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
175 |
fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
176 |
let |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
177 |
val rty = fastype_of rhs |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
178 |
val qty = fastype_of lhs |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
179 |
val absrep_trm = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
180 |
Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
181 |
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
182 |
val (_, prop') = Local_Defs.cert_def lthy prop |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
183 |
val (_, newrhs) = Local_Defs.abs_def prop' |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
184 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
185 |
val ((trm, (_ , def_thm)), lthy') = |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
186 |
Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
187 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
188 |
(* data storage *) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
189 |
val qconst_data = {qconst = trm, rconst = rhs, def = def_thm} |
47198
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
190 |
|
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
191 |
fun qualify defname suffix = Binding.name suffix |
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
192 |
|> Binding.qualify true defname |
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
193 |
|
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
194 |
val lhs_name = Binding.name_of (#1 var) |
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
195 |
val rsp_thm_name = qualify lhs_name "rsp" |
cfd8ff62eab1
use qualified names for rsp and rep_eq theorems in quotient_def
kuncar
parents:
47181
diff
changeset
|
196 |
val code_eqn_thm_name = qualify lhs_name "rep_eq" |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
197 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
198 |
val lthy'' = lthy' |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
199 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
200 |
(fn phi => |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
201 |
(case Quotient_Info.transform_quotconsts phi qconst_data of |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
202 |
qcinfo as {qconst = Const (c, _), ...} => |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
203 |
Quotient_Info.update_quotconsts c qcinfo |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
204 |
| _ => I)) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
205 |
|> (snd oo Local_Theory.note) |
47156 | 206 |
((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]), |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
207 |
[rsp_thm]) |
47156 | 208 |
|> define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
209 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
210 |
in |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
211 |
(qconst_data, lthy'') |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
212 |
end |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
213 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
214 |
fun mk_readable_rsp_thm_eq tm lthy = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
215 |
let |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
216 |
val ctm = cterm_of (Proof_Context.theory_of lthy) tm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
217 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
218 |
fun norm_fun_eq ctm = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
219 |
let |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
220 |
fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
221 |
fun erase_quants ctm' = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
222 |
case (Thm.term_of ctm') of |
47181
b351ad77eb78
some tuning while reviewing the current state of the quotient_def package
bulwahn
parents:
47156
diff
changeset
|
223 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.all_conv ctm' |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
224 |
| _ => (Conv.binder_conv (K erase_quants) lthy then_conv |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
225 |
Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm' |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
226 |
in |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
227 |
(abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
228 |
end |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
229 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
230 |
fun simp_arrows_conv ctm = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
231 |
let |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
232 |
val unfold_conv = Conv.rewrs_conv |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
233 |
[@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
234 |
@{thm fun_rel_def[THEN eq_reflection]}] |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
235 |
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
236 |
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
237 |
in |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
238 |
case (Thm.term_of ctm) of |
47181
b351ad77eb78
some tuning while reviewing the current state of the quotient_def package
bulwahn
parents:
47156
diff
changeset
|
239 |
Const (@{const_name fun_rel}, _) $ _ $ _ => |
b351ad77eb78
some tuning while reviewing the current state of the quotient_def package
bulwahn
parents:
47156
diff
changeset
|
240 |
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
241 |
| _ => Conv.all_conv ctm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
242 |
end |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
243 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
244 |
val unfold_ret_val_invs = Conv.bottom_conv |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
245 |
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
246 |
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
247 |
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
248 |
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
249 |
val beta_conv = Thm.beta_conversion true |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
250 |
val eq_thm = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47091
diff
changeset
|
251 |
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
252 |
in |
47181
b351ad77eb78
some tuning while reviewing the current state of the quotient_def package
bulwahn
parents:
47156
diff
changeset
|
253 |
Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2) |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
254 |
end |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
255 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
256 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
257 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
258 |
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy = |
41444 | 259 |
let |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
260 |
val (vars, ctxt) = prep_vars (the_list raw_var) lthy |
43663
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
261 |
val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE) |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
262 |
val lhs = prep_term T_opt ctxt lhs_raw |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
263 |
val rhs = prep_term NONE ctxt rhs_raw |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
264 |
|
41444 | 265 |
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
266 |
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
|
267 |
val _ = if is_Const rhs then () else warning "The definiens is not a constant" |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
269 |
val var = |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
270 |
(case vars of |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
271 |
[] => (Binding.name lhs_str, NoSyn) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
272 |
| [(binding, _, mx)] => |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
273 |
if Variable.check_name binding = lhs_str then (binding, mx) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
274 |
else error_msg binding lhs_str |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
275 |
| _ => raise Match) |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
276 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
277 |
fun try_to_prove_refl thm = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
278 |
let |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
279 |
val lhs_eq = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
280 |
thm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
281 |
|> prop_of |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
282 |
|> Logic.dest_implies |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
283 |
|> fst |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
284 |
|> strip_all_body |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
285 |
|> try HOLogic.dest_Trueprop |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
286 |
in |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
287 |
case lhs_eq of |
47181
b351ad77eb78
some tuning while reviewing the current state of the quotient_def package
bulwahn
parents:
47156
diff
changeset
|
288 |
SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm) |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
289 |
| SOME _ => (case body_type (fastype_of lhs) of |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
290 |
Type (typ_name, _) => ( SOME |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
291 |
(#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
292 |
RS @{thm Equiv_Relations.equivp_reflp} RS thm) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
293 |
handle _ => NONE) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
294 |
| _ => NONE |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
295 |
) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
296 |
| _ => NONE |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
297 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
298 |
|
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
299 |
val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
300 |
val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs)) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
301 |
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
302 |
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
303 |
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
304 |
|
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
305 |
fun after_qed thm_list lthy = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
306 |
let |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
307 |
val internal_rsp_thm = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
308 |
case thm_list of |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
309 |
[] => the maybe_proven_rsp_thm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
310 |
| [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
311 |
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
312 |
in |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
313 |
snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
314 |
end |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
315 |
|
41444 | 316 |
in |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
317 |
case maybe_proven_rsp_thm of |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
318 |
SOME _ => Proof.theorem NONE after_qed [] lthy |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
319 |
| NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy |
41444 | 320 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
321 |
|
43663
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
322 |
fun check_term' cnstr ctxt = |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
323 |
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I) |
45598 | 324 |
|
325 |
fun read_term' cnstr ctxt = |
|
45929
d7d6c8cfb6f6
removing some debug output in quotient_definition
bulwahn
parents:
45826
diff
changeset
|
326 |
check_term' cnstr ctxt o Syntax.parse_term ctxt |
43663
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
327 |
|
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
328 |
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' |
45598 | 329 |
val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term' |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
330 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
331 |
|
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
332 |
(* parser and command *) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
333 |
val quotdef_parser = |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
334 |
Scan.option Parse_Spec.constdecl -- |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
335 |
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term)) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
336 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
337 |
val _ = |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
338 |
Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
339 |
"definition for constants over the quotient type" |
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
340 |
(quotdef_parser >> quotient_def_cmd) |
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46961
diff
changeset
|
341 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
342 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
343 |
end; (* structure *) |