|
1 (* Title: HOL/BNF_Examples/IsaFoR_Datatypes.thy |
|
2 Author: René Thiemann |
|
3 Copyright 2014 |
|
4 |
|
5 Benchmark of datatypes defined in IsaFoR |
|
6 *) |
|
7 |
|
8 theory IsaFoR_Datatypes |
|
9 imports |
|
10 Real |
|
11 begin |
|
12 |
|
13 datatype_new ('f, 'l) lab = |
|
14 Lab "('f, 'l) lab" 'l |
|
15 | FunLab "('f, 'l) lab" "('f, 'l) lab list" |
|
16 | UnLab 'f |
|
17 | Sharp "('f, 'l) lab" |
|
18 |
|
19 datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list" |
|
20 |
|
21 datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list" |
|
22 datatype_new ('f, 'v) ctxt = |
|
23 Hole ("\<box>") |
|
24 | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list" |
|
25 |
|
26 |
|
27 type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term" |
|
28 type_synonym ('f, 'v) trs = "('f, 'v) rule set" |
|
29 |
|
30 type_synonym ('f, 'v) rules = "('f,'v) rule list" |
|
31 type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule" |
|
32 type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules" |
|
33 type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list" |
|
34 datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70) |
|
35 type_synonym ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list" |
|
36 type_synonym ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list" |
|
37 |
|
38 type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list" |
|
39 type_synonym ('f, 'l, 'v) dppLL = |
|
40 "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times> |
|
41 ('f, 'l, 'v) termsLL \<times> |
|
42 ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL" |
|
43 |
|
44 type_synonym ('f, 'l, 'v) qreltrsLL = |
|
45 "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL" |
|
46 |
|
47 type_synonym ('f, 'l, 'v) qtrsLL = |
|
48 "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL" |
|
49 |
|
50 datatype_new location = H | A | B | R |
|
51 |
|
52 type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \<times> ('f,'v)term \<times> location" |
|
53 type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set" |
|
54 |
|
55 type_synonym ('f, 'l, 'v) fptrsLL = |
|
56 "(('f, 'l)lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL" |
|
57 |
|
58 type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL" |
|
59 |
|
60 type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)" |
|
61 type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list" |
|
62 |
|
63 type_synonym 'v monom = "('v \<times> nat)list" |
|
64 type_synonym ('v,'a)poly = "('v monom \<times> 'a)list" |
|
65 type_synonym ('f,'a)poly_inter_list = "(('f \<times> nat) \<times> (nat,'a)poly)list" |
|
66 type_synonym 'a vec = "'a list" |
|
67 type_synonym 'a mat = "'a vec list" |
|
68 |
|
69 |
|
70 datatype_new arctic = MinInfty | Num_arc int |
|
71 datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a |
|
72 datatype_new order_tag = Lex | Mul |
|
73 |
|
74 type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag))list" |
|
75 datatype_new af_entry = Collapse nat | AFList "nat list" |
|
76 type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry)list" |
|
77 type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option)))list \<times> nat" |
|
78 |
|
79 |
|
80 datatype_new 'f redtriple_impl = |
|
81 Int_carrier "('f, int) lpoly_interL" |
|
82 | Int_nl_carrier "('f, int) poly_inter_list" |
|
83 | Rat_carrier "('f, rat) lpoly_interL" |
|
84 | Rat_nl_carrier rat "('f, rat) poly_inter_list" |
|
85 | Real_carrier "('f, real) lpoly_interL" |
|
86 | Real_nl_carrier real "('f, real) poly_inter_list" |
|
87 | Arctic_carrier "('f, arctic) lpoly_interL" |
|
88 | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" |
|
89 | Int_mat_carrier nat nat "('f, int mat) lpoly_interL" |
|
90 | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL" |
|
91 | Real_mat_carrier nat nat "('f, real mat) lpoly_interL" |
|
92 | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL" |
|
93 | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL" |
|
94 | RPO "'f status_prec_repr" "'f afs_list" |
|
95 | KBO "'f prec_weight_repr" "'f afs_list" |
|
96 |
|
97 datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext |
|
98 type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list" |
|
99 |
|
100 datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl" |
|
101 |
|
102 type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list" |
|
103 type_synonym ('f,'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f,'v)rules \<times> ('f,'v)rules" |
|
104 |
|
105 datatype_new arithFun = |
|
106 Arg nat |
|
107 | Const nat |
|
108 | Sum "arithFun list" |
|
109 | Max "arithFun list" |
|
110 | Min "arithFun list" |
|
111 | Prod "arithFun list" |
|
112 | IfEqual arithFun arithFun arithFun arithFun |
|
113 |
|
114 datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list" |
|
115 datatype_new ('f,'v)sl_variant = Rootlab "('f \<times> nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v |
|
116 |
|
117 type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \<times> ('f,'v)rseq \<times> ('f,'v)term \<times> ('f,'v)rseq)list" |
|
118 datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat |
|
119 |
|
120 type_synonym unknown_info = string |
|
121 |
|
122 type_synonym dummy_prf = unit |
|
123 |
|
124 |
|
125 datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof |
|
126 "('f,'v)term" |
|
127 "(('f,'v)rule \<times> ('f,'v)rule) list" |
|
128 |
|
129 datatype_new ('f,'v)cond_constraint |
|
130 = CC_cond bool "('f,'v)rule" |
|
131 | CC_rewr "('f,'v)term" "('f,'v)term" |
|
132 | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint" |
|
133 | CC_all 'v "('f,'v)cond_constraint" |
|
134 |
|
135 type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list" |
|
136 type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL" |
|
137 |
|
138 datatype_new ('f,'v)cond_constraint_prf = |
|
139 Final |
|
140 | Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" |
|
141 | Different_Constructor "('f,'v)cond_constraint" |
|
142 | Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" |
|
143 | Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" |
|
144 | Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" |
|
145 | Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" |
|
146 | Induction "('f,'v)cond_constraint" "('f,'v)cond_constraint list" "(('f,'v)rule \<times> (('f,'v)term \<times> 'v list) list \<times> ('f,'v)cond_constraint \<times> ('f,'v)cond_constraint_prf) list" |
|
147 |
|
148 |
|
149 datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf |
|
150 'f |
|
151 "(('f,'v)cond_constraint \<times> ('f,'v)rules \<times> ('f,'v)cond_constraint_prf) list" |
|
152 nat |
|
153 nat |
|
154 |
|
155 datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _") |
|
156 datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \<times> 'q)list" |
|
157 datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \<times> 'q) list" |
|
158 |
|
159 datatype_new boundstype = Roof | Match |
|
160 datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation" |
|
161 |
|
162 datatype_new ('f, 'v) pat_eqv_prf = |
|
163 Pat_Dom_Renaming "('f, 'v) substL" |
|
164 | Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL" |
|
165 | Pat_Simplify "('f, 'v) substL" "('f, 'v) substL" |
|
166 |
|
167 datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close |
|
168 |
|
169 datatype_new ('f, 'v) pat_rule_prf = |
|
170 Pat_OrigRule "('f, 'v) rule" bool |
|
171 | Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" |
|
172 | Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v |
|
173 | Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf" |
|
174 | Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos |
|
175 | Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos |
|
176 | Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v |
|
177 | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat |
|
178 |
|
179 datatype_new ('f, 'v) non_loop_prf = |
|
180 Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos |
|
181 |
|
182 |
|
183 datatype_new ('f, 'l, 'v) problem = |
|
184 SN_TRS "('f,'l,'v)qreltrsLL" |
|
185 | SN_FP_TRS "('f,'l,'v)fptrsLL" |
|
186 | Finite_DPP "('f,'l,'v) dppLL" |
|
187 | Unknown_Problem unknown_info |
|
188 | Not_SN_TRS "('f,'l,'v)qtrsLL" |
|
189 | Not_RelSN_TRS "('f,'l,'v)qreltrsLL" |
|
190 | Infinite_DPP "('f,'l,'v) dppLL" |
|
191 | Not_SN_FP_TRS "('f,'l,'v)fptrsLL" |
|
192 declare [[bnf_timing]] |
|
193 datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = |
|
194 SN_assm_proof "('f,'l,'v)qreltrsLL" 'a |
|
195 | Finite_assm_proof "('f,'l,'v)dppLL" 'b |
|
196 | SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c |
|
197 | Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a |
|
198 | Infinite_assm_proof "('f,'l,'v)dppLL" 'b |
|
199 | Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c |
|
200 | Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd |
|
201 | Unknown_assm_proof unknown_info 'e |
|
202 |
|
203 type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof" |
|
204 |
|
205 datatype_new ('f, 'l, 'v) assm = |
|
206 SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" |
|
207 | SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" |
|
208 | Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" |
|
209 | Unknown_assm "('f,'l,'v)problem list" unknown_info |
|
210 | Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" |
|
211 | Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" |
|
212 | Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" |
|
213 | Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" |
|
214 |
|
215 fun satisfied :: "('f,'l,'v)problem \<Rightarrow> bool" where |
|
216 "satisfied (SN_TRS t) = (t = t)" |
|
217 | "satisfied (SN_FP_TRS t) = (t \<noteq> t)" |
|
218 | "satisfied (Finite_DPP d) = (d \<noteq> d)" |
|
219 | "satisfied (Unknown_Problem s) = (s = ''foo'')" |
|
220 | "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)" |
|
221 | "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)" |
|
222 | "satisfied (Infinite_DPP d) = (d = d)" |
|
223 | "satisfied (Not_SN_FP_TRS t) = (t = t)" |
|
224 |
|
225 fun collect_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) |
|
226 \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list) |
|
227 \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list) |
|
228 \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) |
|
229 \<Rightarrow> ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \<Rightarrow> ('f,'l,'v) assm list" where |
|
230 "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf" |
|
231 | "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf" |
|
232 | "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf" |
|
233 | "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf" |
|
234 | "collect_assms _ _ _ _ _ = []" |
|
235 |
|
236 fun collect_neg_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) |
|
237 \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list) |
|
238 \<Rightarrow> ('rtp \<Rightarrow> ('f,'l,'v) assm list) |
|
239 \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list) |
|
240 \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) |
|
241 \<Rightarrow> ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \<Rightarrow> ('f,'l,'v) assm list" where |
|
242 "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf" |
|
243 | "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf" |
|
244 | "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf" |
|
245 | "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf" |
|
246 | "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf" |
|
247 | "collect_neg_assms tp dpp rtp fptp unk _ = []" |
|
248 |
|
249 |
|
250 |
|
251 datatype_new ('f, 'l, 'v) dp_nontermination_proof = |
|
252 DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" |
|
253 | DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf" |
|
254 | DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof" |
|
255 | DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" |
|
256 | DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" |
|
257 | DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof" |
|
258 | DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" |
|
259 | DP_Rewriting "('f,'l,'v)trsLL option" "('f,'l,'v)ruleLL" "('f,'l,'v)ruleLL" "('f,'l,'v)ruleLL" "(('f,'l)lab,'v)rule" pos "('f,'l,'v) dp_nontermination_proof" |
|
260 | DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" |
|
261 | DP_Assume_Infinite "('f, 'l, 'v) dppLL" |
|
262 "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, |
|
263 ('f, 'l, 'v) dp_nontermination_proof, |
|
264 ('f, 'l, 'v) reltrs_nontermination_proof, |
|
265 ('f, 'l, 'v) fp_nontermination_proof, |
|
266 ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" |
|
267 and |
|
268 ('f,'l,'v) "trs_nontermination_proof" = |
|
269 TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" |
|
270 | TRS_Not_Well_Formed |
|
271 | TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof" |
|
272 | TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof" |
|
273 | TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" |
|
274 | TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf" |
|
275 | TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof" |
|
276 | TRS_Assume_Not_SN "('f, 'l, 'v)qtrsLL" |
|
277 "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, |
|
278 ('f, 'l, 'v) dp_nontermination_proof, |
|
279 ('f, 'l, 'v) reltrs_nontermination_proof, |
|
280 ('f, 'l, 'v) fp_nontermination_proof, |
|
281 ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" |
|
282 and |
|
283 ('f,'l,'v)"reltrs_nontermination_proof" = |
|
284 Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" |
|
285 | Rel_Not_Well_Formed |
|
286 | Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof" |
|
287 | Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof" |
|
288 | Rel_TRS_Assume_Not_SN "('f, 'l, 'v)qreltrsLL" |
|
289 "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, |
|
290 ('f, 'l, 'v) dp_nontermination_proof, |
|
291 ('f, 'l, 'v) reltrs_nontermination_proof, |
|
292 ('f, 'l, 'v) fp_nontermination_proof, |
|
293 ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" |
|
294 and |
|
295 ('f, 'l, 'v) "fp_nontermination_proof" = |
|
296 FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" |
|
297 | FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" |
|
298 | FPTRS_Assume_Not_SN "('f, 'l, 'v)fptrsLL" |
|
299 "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, |
|
300 ('f, 'l, 'v) dp_nontermination_proof, |
|
301 ('f, 'l, 'v) reltrs_nontermination_proof, |
|
302 ('f, 'l, 'v) fp_nontermination_proof, |
|
303 ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" |
|
304 and |
|
305 ('f, 'l, 'v) neg_unknown_proof = |
|
306 Assume_NT_Unknown unknown_info |
|
307 "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, |
|
308 ('f, 'l, 'v) dp_nontermination_proof, |
|
309 ('f, 'l, 'v) reltrs_nontermination_proof, |
|
310 ('f, 'l, 'v) fp_nontermination_proof, |
|
311 ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" |
|
312 |
|
313 |
|
314 datatype_new ('f, 'l, 'v) dp_termination_proof = |
|
315 P_is_Empty |
|
316 | Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL" |
|
317 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
318 | Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
319 | Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" |
|
320 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
321 | Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
322 | Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list" |
|
323 | Mono_Redpair_Proc "('f, 'l) lab redtriple_impl" |
|
324 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
325 | Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl" |
|
326 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
327 | Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list" |
|
328 | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option" |
|
329 "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list" |
|
330 | Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info" |
|
331 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
332 | Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list" |
|
333 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
334 | Split_Proc |
|
335 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" |
|
336 "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof" |
|
337 | Semlab_Proc |
|
338 "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL" |
|
339 "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL" |
|
340 "('f, 'l, 'v) dp_termination_proof" |
|
341 | Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof" |
|
342 | Rewriting_Proc |
|
343 "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" |
|
344 "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof" |
|
345 | Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
346 | Forward_Instantiation_Proc |
|
347 "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof" |
|
348 | Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
349 | Assume_Finite |
|
350 "('f, 'l, 'v) dppLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list" |
|
351 | Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" |
|
352 | Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof" |
|
353 | Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof" |
|
354 | General_Redpair_Proc |
|
355 "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" |
|
356 "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" |
|
357 | To_Trs_Proc "('f, 'l, 'v) trs_termination_proof" |
|
358 and ('f, 'l, 'v) trs_termination_proof = |
|
359 DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof" |
|
360 | Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof" |
|
361 | String_Reversal "('f, 'l, 'v) trs_termination_proof" |
|
362 | Bounds "(('f, 'l) lab, 'v) bounds_info" |
|
363 | Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" |
|
364 | Semlab |
|
365 "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list" |
|
366 "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" |
|
367 | R_is_Empty |
|
368 | Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" |
|
369 | Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof" |
|
370 | Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" |
|
371 | Drop_Equality "('f, 'l, 'v) trs_termination_proof" |
|
372 | Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" |
|
373 | Assume_SN "('f, 'l, 'v) qreltrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list" |
|
374 and ('f, 'l, 'v) unknown_proof = |
|
375 Assume_Unknown unknown_info "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list" |
|
376 and ('f, 'l, 'v) fptrs_termination_proof = |
|
377 Assume_FP_SN "('f,'l,'v)fptrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list" |
|
378 |
|
379 |
|
380 end |