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