2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
15 let string_iter sep f n =
16 let rec aux = function
19 | n -> f n ^ sep ^ aux (pred n)
24 let rec aux = function
27 | n -> f n; aux (pred n)
31 let mk_exists ooch noch c v =
32 let description = "multiple existental quantifier" in
33 let prec = "non associative with precedence 20\n" in
35 if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
37 let o_name = name "ex" in
39 if v = 1 then "'Ex" else P.sprintf "'Ex%u" v
41 let set n = P.sprintf "A%u" (v - n) in
42 let set_list = string_iter "," set v in
43 let set_type = string_iter "→" set v in
45 let ele n = P.sprintf "x%u" (v - n) in
46 let ele_list = string_iter "," ele v in
47 let ele_seq = string_iter " " ele v in
49 let pre n = P.sprintf "P%u" (c - n) in
50 let pre_list = string_iter "," pre c in
51 let pre_seq = string_iter " " pre c in
52 let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in
53 let pre_type = string_iter " → " pre_appl c in
56 let qm_set = string_iter " " qm v in
57 let qm_pre = string_iter " " qm c in
59 let id n = P.sprintf "ident x%u" (v - n) in
60 let id_list = string_iter " , " id v in
62 let term n = P.sprintf "term 19 P%u" (c - n) in
63 let term_conj = string_iter " break & " term c in
65 let abst b n = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in
66 P.sprintf "λ${ident x%u}%s" (v - n) xty in
68 let abst_clo b = string_iter "." (abst b) v in
70 let full b n = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in
71 let full_seq b = string_iter " " (full b) c in
73 P.fprintf ooch "(* Note: %s (%u, %u) *)\n" description c v;
75 P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n"
76 o_name set_list pre_list set_type;
77 P.fprintf ooch " | %s_intro: ∀%s. %s → %s %s %s\n.\n\n"
78 o_name ele_list pre_type o_name qm_set qm_pre;
80 P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n"
81 description c v i_name pre_seq o_name qm_set pre_seq;
83 P.fprintf noch "(* Note: %s (%u, %u) *)\n" description c v;
85 P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n"
86 id_list term_conj prec i_name (full_seq false);
88 P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n"
89 id_list term_conj prec i_name (full_seq true)
91 let mk_or ooch noch c =
92 let description = "multiple disjunction connective" in
93 let prec = "non associative with precedence 30\n" in
94 let name s = P.sprintf "%s%u" s c in
95 let o_name = name "or" in
98 let pre n = P.sprintf "P%u" (c - n) in
99 let pre_list = string_iter "," pre c in
100 let pre_seq = string_iter " " pre c in
103 let qm_pre = string_iter " " qm c in
105 let term n = P.sprintf "term 29 P%u" (c - n) in
106 let term_disj = string_iter " break | " term c in
108 let par n = P.sprintf "$P%u" (c - n) in
109 let par_seq = string_iter " " par c in
111 let mk_con n = P.fprintf ooch " | %s_intro%u: %s → %s %s\n"
112 o_name (c - n) (pre n) o_name qm_pre
115 P.fprintf ooch "(* Note: %s (%u) *)\n" description c;
117 P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
120 P.fprintf ooch ".\n\n";
122 P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
123 description c i_name pre_seq o_name pre_seq;
125 P.fprintf noch "(* Note: %s (%u) *)\n" description c;
127 P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n"
128 term_disj prec i_name par_seq
130 let mk_and ooch noch c =
131 let description = "multiple conjunction connective" in
132 let prec = "non associative with precedence 35\n" in
133 let name s = P.sprintf "%s%u" s c in
134 let o_name = name "and" in
135 let i_name = "'And" in
137 let pre n = P.sprintf "P%u" (c - n) in
138 let pre_list = string_iter "," pre c in
139 let pre_type = string_iter " → " pre c in
140 let pre_seq = string_iter " " pre c in
143 let qm_pre = string_iter " " qm c in
145 let term n = P.sprintf "term 34 P%u" (c - n) in
146 let term_conj = string_iter " break & " term c in
148 let par n = P.sprintf "$P%u" (c - n) in
149 let par_seq = string_iter " " par c in
151 P.fprintf ooch "(* Note: %s (%u) *)\n" description c;
153 P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
155 P.fprintf ooch " | %s_intro: %s → %s %s\n.\n\n"
156 o_name pre_type o_name qm_pre;
158 P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
159 description c i_name pre_seq o_name pre_seq;
161 P.fprintf noch "(* Note: %s (%u) *)\n" description c;
163 P.fprintf noch "notation \"hvbox(∧∧ %s)\"\n %s for @{ %s %s }.\n\n"
164 term_conj prec i_name par_seq
166 let generate ooch noch = function
168 if c > 0 && v > 0 then mk_exists ooch noch c v
170 if c > 1 then mk_or ooch noch c
172 if c > 1 then mk_and ooch noch c