author  wenzelm 
Fri, 28 Oct 2011 23:10:44 +0200  
changeset 45292  90106a351a11 
parent 45291  57cd50f98fdc 
child 45598  87a2624f57e4 
permissions  rwrr 
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 
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

9 
val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) > 
45279  10 
local_theory > Quotient_Info.quotconsts * local_theory 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

11 

43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

12 
val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) > 
45279  13 
local_theory > Quotient_Info.quotconsts * local_theory 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

14 

37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset

15 
val lift_raw_const: typ list > (string * term * mixfix) > local_theory > 
45279  16 
Quotient_Info.quotconsts * local_theory 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 
end; 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

18 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

19 
structure Quotient_Def: QUOTIENT_DEF = 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

20 
struct 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

21 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

22 
(** Interface and Syntax Setup **) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

23 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

24 
(* The MLinterface for a quotient definition takes 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

25 
as argument: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

26 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

27 
 an optional binding and mixfix annotation 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

28 
 attributes 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

29 
 the new constant as term 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

30 
 the rhs of the definition as term 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

31 

45279  32 
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

33 

41444  34 
Restriction: At the moment the left and righthand 
35 
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

36 
*) 
41444  37 
fun error_msg bind str = 
38 
let 

39 
val name = Binding.name_of bind 

40 
val pos = Position.str_of (Binding.pos_of bind) 

41 
in 

42 
error ("Head of quotient_definition " ^ 

43 
quote str ^ " differs from declaration " ^ name ^ pos) 

44 
end 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

45 

43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

46 
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy = 
41444  47 
let 
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

48 
val (vars, ctxt) = prep_vars (the_list raw_var) lthy 
43663
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

49 
val T_opt = (case vars of [(_, SOME T, _)] => SOME T  _ => NONE) 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

50 
val lhs = prep_term T_opt ctxt lhs_raw 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

51 
val rhs = prep_term NONE ctxt rhs_raw 
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

52 

41444  53 
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." 
54 
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" 

55 
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

56 

43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

57 
val var = 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

58 
(case vars of 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

59 
[] => (Binding.name lhs_str, NoSyn) 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

60 
 [(binding, _, mx)] => 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

61 
if Variable.check_name binding = lhs_str then (binding, mx) 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

62 
else error_msg binding lhs_str 
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

63 
 _ => raise Match) 
41444  64 

41451  65 
val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs 
41444  66 
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) 
67 
val (_, prop') = Local_Defs.cert_def lthy prop 

68 
val (_, newrhs) = Local_Defs.abs_def prop' 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

69 

43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

70 
val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

71 

41444  72 
(* data storage *) 
73 
val qconst_data = {qconst = trm, rconst = rhs, def = thm} 

37530
70d03844b2f9
export of proper information in the MLinterface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset

74 

45292
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

75 
val lthy'' = lthy' 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

76 
> Local_Theory.declaration {syntax = false, pervasive = true} 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

77 
(fn phi => 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

78 
(case Quotient_Info.transform_quotconsts phi qconst_data of 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

79 
qcinfo as {qconst = Const (c, _), ...} => 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

80 
Quotient_Info.update_quotconsts c qcinfo 
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset

81 
 _ => I)); 
41444  82 
in 
83 
(qconst_data, lthy'') 

84 
end 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

85 

43663
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

86 
fun check_term' cnstr ctxt = 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

87 
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T  _ => I) 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

88 
fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

89 

e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

90 
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' 
e8c80bbc0c5d
recheck to explicitly propagate a given type constraint to lhs  necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset

91 
val quotdef_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

92 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

93 

37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset

94 
(* a wrapper for automatically lifting a raw constant *) 
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset

95 
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = 
41444  96 
let 
97 
val rty = fastype_of rconst 

41451  98 
val qty = Quotient_Term.derive_qtyp ctxt qtys rty 
41444  99 
val lhs = Free (qconst_name, qty) 
100 
in 

43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

101 
quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt 
41444  102 
end 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

103 

37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset

104 
(* parser and command *) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

105 
val quotdef_parser = 
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset

106 
Scan.option Parse_Spec.constdecl  
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

107 
Parse.!!! (Parse_Spec.opt_thm_name ":"  (Parse.term  Parse.$$$ "is"  Parse.term)) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

108 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

109 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

110 
Outer_Syntax.local_theory "quotient_definition" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

111 
"definition for constants over the quotient type" 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

112 
Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

113 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

114 
end; (* structure *) 