57586
|
1 |
(* Title: HOL/BNF_Examples/IsaFoR_Datatypes.thy
|
57634
|
2 |
Author: Rene Thiemann, UIBK
|
57586
|
3 |
Copyright 2014
|
|
4 |
|
57634
|
5 |
Benchmark consisting of datatypes defined in IsaFoR.
|
57586
|
6 |
*)
|
|
7 |
|
57634
|
8 |
header {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
|
|
9 |
|
57586
|
10 |
theory IsaFoR_Datatypes
|
57634
|
11 |
imports Real
|
57586
|
12 |
begin
|
|
13 |
|
|
14 |
datatype_new ('f, 'l) lab =
|
57634
|
15 |
Lab "('f, 'l) lab" 'l
|
|
16 |
| FunLab "('f, 'l) lab" "('f, 'l) lab list"
|
|
17 |
| UnLab 'f
|
|
18 |
| Sharp "('f, 'l) lab"
|
57586
|
19 |
|
|
20 |
datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
|
|
21 |
|
|
22 |
datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
|
|
23 |
datatype_new ('f, 'v) ctxt =
|
57634
|
24 |
Hole ("\<box>")
|
|
25 |
| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
|
57586
|
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 |
|
57634
|
30 |
type_synonym ('f, 'v) rules = "('f, 'v) rule list"
|
57586
|
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"
|
57634
|
34 |
|
57586
|
35 |
datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
|
57634
|
36 |
|
57586
|
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_new location = H | A | B | R
|
|
53 |
|
57634
|
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"
|
57586
|
56 |
|
|
57 |
type_synonym ('f, 'l, 'v) fptrsLL =
|
57634
|
58 |
"(('f, 'l) lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
|
57586
|
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 |
|
57634
|
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"
|
57586
|
68 |
type_synonym 'a vec = "'a list"
|
57634
|
69 |
type_synonym 'a mat = "'a vec list"
|
57586
|
70 |
|
|
71 |
datatype_new arctic = MinInfty | Num_arc int
|
|
72 |
datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
|
|
73 |
datatype_new order_tag = Lex | Mul
|
|
74 |
|
57634
|
75 |
type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
|
|
76 |
|
|
77 |
datatype_new af_entry =
|
|
78 |
Collapse nat
|
|
79 |
| AFList "nat list"
|
57586
|
80 |
|
57634
|
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"
|
57586
|
83 |
|
57634
|
84 |
datatype_new 'f redtriple_impl =
|
|
85 |
Int_carrier "('f, int) lpoly_interL"
|
|
86 |
| Int_nl_carrier "('f, int) poly_inter_list"
|
57586
|
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"
|
57634
|
91 |
| Arctic_carrier "('f, arctic) lpoly_interL"
|
|
92 |
| Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL"
|
57586
|
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 |
|
57634
|
101 |
datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext
|
57586
|
102 |
type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
|
|
103 |
|
|
104 |
datatype_new '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"
|
57634
|
107 |
type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
|
57586
|
108 |
|
|
109 |
datatype_new arithFun =
|
57634
|
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
|
57586
|
117 |
|
|
118 |
datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
|
57634
|
119 |
datatype_new ('f, 'v) sl_variant =
|
|
120 |
Rootlab "('f \<times> nat) option"
|
|
121 |
| Finitelab "'f sl_inter"
|
|
122 |
| QuasiFinitelab "'f sl_inter" 'v
|
57586
|
123 |
|
57634
|
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_new 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
|
57586
|
127 |
|
|
128 |
type_synonym unknown_info = string
|
|
129 |
|
|
130 |
type_synonym dummy_prf = unit
|
|
131 |
|
57634
|
132 |
datatype_new ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
|
|
133 |
"('f, 'v) term"
|
|
134 |
"(('f, 'v) rule \<times> ('f, 'v) rule) list"
|
57586
|
135 |
|
57634
|
136 |
datatype_new ('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"
|
57586
|
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 |
|
57634
|
145 |
datatype_new ('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"
|
57586
|
154 |
|
57634
|
155 |
datatype_new ('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
|
57586
|
158 |
|
57634
|
159 |
datatype_new ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
|
|
160 |
datatype_new ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
|
|
161 |
datatype_new 'q ta_relation =
|
|
162 |
Decision_Proc
|
|
163 |
| Id_Relation
|
|
164 |
| Some_Relation "('q \<times> 'q) list"
|
57586
|
165 |
|
|
166 |
datatype_new boundstype = Roof | Match
|
57634
|
167 |
datatype_new ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
|
57586
|
168 |
|
|
169 |
datatype_new ('f, 'v) pat_eqv_prf =
|
57634
|
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"
|
57586
|
173 |
|
|
174 |
datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
|
|
175 |
|
57634
|
176 |
datatype_new ('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
|
57586
|
185 |
|
|
186 |
datatype_new ('f, 'v) non_loop_prf =
|
57634
|
187 |
Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
|
57586
|
188 |
|
57634
|
189 |
datatype_new ('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 |
|
57586
|
199 |
declare [[bnf_timing]]
|
|
200 |
|
57634
|
201 |
datatype_new ('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
|
57586
|
210 |
|
57634
|
211 |
type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
|
57586
|
212 |
|
57634
|
213 |
datatype_new ('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
|
57586
|
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'')"
|
57634
|
228 |
| "satisfied (Not_SN_TRS (nfs, q, r)) = (length q = length r)"
|
|
229 |
| "satisfied (Not_RelSN_TRS (nfs, q, r, rw)) = (r = rw)"
|
57586
|
230 |
| "satisfied (Infinite_DPP d) = (d = d)"
|
|
231 |
| "satisfied (Not_SN_FP_TRS t) = (t = t)"
|
|
232 |
|
57634
|
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
|
57586
|
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 |
|
57634
|
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
|
57586
|
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_new ('f, 'l, 'v) dp_nontermination_proof =
|
57634
|
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"
|
57586
|
314 |
|
|
315 |
datatype_new ('f, 'l, 'v) dp_termination_proof =
|
57634
|
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"
|
57586
|
359 |
and ('f, 'l, 'v) trs_termination_proof =
|
57634
|
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"
|
57586
|
375 |
and ('f, 'l, 'v) unknown_proof =
|
57634
|
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"
|
57586
|
377 |
and ('f, 'l, 'v) fptrs_termination_proof =
|
57634
|
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"
|
57586
|
379 |
|
|
380 |
end
|