1.1 --- a/NEWS Thu Apr 29 17:50:11 2010 +0200
1.2 +++ b/NEWS Thu Apr 29 18:41:38 2010 +0200
1.3 @@ -89,6 +89,10 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* 'code_reflect' allows to incorporate generated ML code into
1.8 +runtime environment; replaces immature code_datatype antiquotation.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 * Empty class specifications observe default sort. INCOMPATIBILITY.
1.12
1.13 * Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
2.1 --- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 29 17:50:11 2010 +0200
2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 29 18:41:38 2010 +0200
2.3 @@ -3209,47 +3209,12 @@
2.4 interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
2.5 interpret_floatarith_sin
2.6
2.7 -ML {*
2.8 -structure Float_Arith =
2.9 -struct
2.10 -
2.11 -@{code_datatype float = Float}
2.12 -@{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
2.13 - | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num }
2.14 -@{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
2.15 -
2.16 -val approx_form = @{code approx_form}
2.17 -val approx_tse_form = @{code approx_tse_form}
2.18 -val approx' = @{code approx'}
2.19 -val approx_form_eval = @{code approx_form_eval}
2.20 -
2.21 -end
2.22 -*}
2.23 -
2.24 -code_reserved Eval Float_Arith
2.25 -
2.26 -code_type float (Eval "Float'_Arith.float")
2.27 -code_const Float (Eval "Float'_Arith.Float/ (_,/ _)")
2.28 -
2.29 -code_type floatarith (Eval "Float'_Arith.floatarith")
2.30 -code_const Add and Minus and Mult and Inverse and Cos and Arctan and Abs and Max and Min and
2.31 - Pi and Sqrt and Exp and Ln and Power and Var and Num
2.32 - (Eval "Float'_Arith.Add/ (_,/ _)" and "Float'_Arith.Minus" and "Float'_Arith.Mult/ (_,/ _)" and
2.33 - "Float'_Arith.Inverse" and "Float'_Arith.Cos" and
2.34 - "Float'_Arith.Arctan" and "Float'_Arith.Abs" and "Float'_Arith.Max/ (_,/ _)" and
2.35 - "Float'_Arith.Min/ (_,/ _)" and "Float'_Arith.Pi" and "Float'_Arith.Sqrt" and
2.36 - "Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and
2.37 - "Float'_Arith.Var" and "Float'_Arith.Num")
2.38 -
2.39 -code_type form (Eval "Float'_Arith.form")
2.40 -code_const Bound and Assign and Less and LessEqual and AtLeastAtMost
2.41 - (Eval "Float'_Arith.Bound/ (_,/ _,/ _,/ _)" and "Float'_Arith.Assign/ (_,/ _,/ _)" and
2.42 - "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)" and
2.43 - "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
2.44 -
2.45 -code_const approx_form (Eval "Float'_Arith.approx'_form")
2.46 -code_const approx_tse_form (Eval "Float'_Arith.approx'_tse'_form")
2.47 -code_const approx' (Eval "Float'_Arith.approx'")
2.48 +code_reflect Float_Arith
2.49 + datatypes float = Float
2.50 + and floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
2.51 + | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num
2.52 + and form = Bound | Assign | Less | LessEqual | AtLeastAtMost
2.53 + functions approx_form approx_tse_form approx' approx_form_eval
2.54
2.55 ML {*
2.56 fun reorder_bounds_tac prems i =
3.1 --- a/src/HOL/Decision_Procs/Cooper.thy Thu Apr 29 17:50:11 2010 +0200
3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Apr 29 18:41:38 2010 +0200
3.3 @@ -1909,10 +1909,9 @@
3.4
3.5 ML {* @{code cooper_test} () *}
3.6
3.7 -(*
3.8 -code_reserved SML oo
3.9 -export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
3.10 -*)
3.11 +code_reflect Generated_Cooper
3.12 + functions pa
3.13 + file "~~/src/HOL/Tools/Qelim/generated_cooper.ML"
3.14
3.15 oracle linzqe_oracle = {*
3.16 let
4.1 --- a/src/HOL/Decision_Procs/MIR.thy Thu Apr 29 17:50:11 2010 +0200
4.2 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Apr 29 18:41:38 2010 +0200
4.3 @@ -5791,8 +5791,9 @@
4.4 ML {* @{code test4} () *}
4.5 ML {* @{code test5} () *}
4.6
4.7 -(*export_code mircfrqe mirlfrqe
4.8 - in SML module_name Mir file "raw_mir.ML"*)
4.9 +(*code_reflect Mir
4.10 + functions mircfrqe mirlfrqe
4.11 + file "mir.ML"*)
4.12
4.13 oracle mirfr_oracle = {* fn (proofs, ct) =>
4.14 let
5.1 --- a/src/HOL/HOL.thy Thu Apr 29 17:50:11 2010 +0200
5.2 +++ b/src/HOL/HOL.thy Thu Apr 29 18:41:38 2010 +0200
5.3 @@ -1962,6 +1962,10 @@
5.4
5.5 subsubsection {* Evaluation and normalization by evaluation *}
5.6
5.7 +text {* Avoid some named infixes in evaluation environment *}
5.8 +
5.9 +code_reserved Eval oo ooo oooo upto downto orf andf mem mem_int mem_string
5.10 +
5.11 setup {*
5.12 Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
5.13 *}
6.1 --- a/src/HOL/Lazy_Sequence.thy Thu Apr 29 17:50:11 2010 +0200
6.2 +++ b/src/HOL/Lazy_Sequence.thy Thu Apr 29 18:41:38 2010 +0200
6.3 @@ -123,41 +123,18 @@
6.4
6.5 subsection {* Code setup *}
6.6
6.7 -code_reflect
6.8 +fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
6.9 + "anamorph f k x = (if k = 0 then ([], x)
6.10 + else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
6.11 + let (vs, z) = anamorph f (k - 1) y
6.12 + in (v # vs, z))"
6.13 +
6.14 +definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
6.15 + "yieldn = anamorph yield"
6.16 +
6.17 +code_reflect Lazy_Sequence
6.18 datatypes lazy_sequence = Lazy_Sequence
6.19 - functions map yield
6.20 - module_name Lazy_Sequence
6.21 -
6.22 -(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
6.23 -
6.24 -ML {*
6.25 -signature LAZY_SEQUENCE =
6.26 -sig
6.27 - datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
6.28 - val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
6.29 - val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
6.30 - val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
6.31 - val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
6.32 -end;
6.33 -
6.34 -structure Lazy_Sequence : LAZY_SEQUENCE =
6.35 -struct
6.36 -
6.37 -open Lazy_Sequence;
6.38 -
6.39 -fun map f = mapa f;
6.40 -
6.41 -fun anamorph f k x = (if k = 0 then ([], x)
6.42 - else case f x
6.43 - of NONE => ([], x)
6.44 - | SOME (v, y) => let
6.45 - val (vs, z) = anamorph f (k - 1) y
6.46 - in (v :: vs, z) end);
6.47 -
6.48 -fun yieldn S = anamorph yield S;
6.49 -
6.50 -end;
6.51 -*}
6.52 + functions map yield yieldn
6.53
6.54 section {* With Hit Bound Value *}
6.55 text {* assuming in negative context *}
7.1 --- a/src/HOL/Predicate.thy Thu Apr 29 17:50:11 2010 +0200
7.2 +++ b/src/HOL/Predicate.thy Thu Apr 29 18:41:38 2010 +0200
7.3 @@ -880,10 +880,9 @@
7.4
7.5 code_abort not_unique
7.6
7.7 -code_reflect
7.8 +code_reflect Predicate
7.9 datatypes pred = Seq and seq = Empty | Insert | Join
7.10 functions map
7.11 - module_name Predicate
7.12
7.13 ML {*
7.14 signature PREDICATE =
8.1 --- a/src/HOL/Random.thy Thu Apr 29 17:50:11 2010 +0200
8.2 +++ b/src/HOL/Random.thy Thu Apr 29 18:41:38 2010 +0200
8.3 @@ -138,10 +138,15 @@
8.4
8.5 subsection {* @{text ML} interface *}
8.6
8.7 +code_reflect Random_Engine
8.8 + functions range select select_weight
8.9 +
8.10 ML {*
8.11 structure Random_Engine =
8.12 struct
8.13
8.14 +open Random_Engine;
8.15 +
8.16 type seed = int * int;
8.17
8.18 local
9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 29 17:50:11 2010 +0200
9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 29 18:41:38 2010 +0200
9.3 @@ -3232,14 +3232,14 @@
9.4 (Code_Eval.eval NONE
9.5 ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
9.6 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
9.7 - |> Lazy_Sequence.map (apfst proc))
9.8 + |> Lazy_Sequence.mapa (apfst proc))
9.9 thy t' [] nrandom size seed depth))))
9.10 else rpair NONE
9.11 (fst (Lazy_Sequence.yieldn k
9.12 (Code_Eval.eval NONE
9.13 ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
9.14 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
9.15 - |> Lazy_Sequence.map proc)
9.16 + |> Lazy_Sequence.mapa proc)
9.17 thy t' [] nrandom size seed depth)))
9.18 end
9.19 | _ =>
10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Apr 29 17:50:11 2010 +0200
10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Apr 29 18:41:38 2010 +0200
10.3 @@ -267,7 +267,7 @@
10.4 Code_Eval.eval (SOME target)
10.5 ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
10.6 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
10.7 - g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
10.8 + g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
10.9 thy4 qc_term []
10.10 in
10.11 fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
11.1 --- a/src/HOL/Tools/Qelim/cooper.ML Thu Apr 29 17:50:11 2010 +0200
11.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Apr 29 18:41:38 2010 +0200
11.3 @@ -536,7 +536,7 @@
11.4 structure Coopereif =
11.5 struct
11.6
11.7 -open GeneratedCooper;
11.8 +open Generated_Cooper;
11.9
11.10 fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
11.11 fun i_of_term vs t = case t
12.1 --- a/src/HOL/Tools/Qelim/generated_cooper.ML Thu Apr 29 17:50:11 2010 +0200
12.2 +++ b/src/HOL/Tools/Qelim/generated_cooper.ML Thu Apr 29 18:41:38 2010 +0200
12.3 @@ -1,49 +1,263 @@
12.4 -(* Title: HOL/Tools/Qelim/generated_cooper.ML
12.5 +(* Generated from Cooper.thy; DO NOT EDIT! *)
12.6
12.7 -This file is generated from HOL/Decision_Procs/Cooper.thy. DO NOT EDIT.
12.8 -*)
12.9 -
12.10 -structure GeneratedCooper =
12.11 -struct
12.12 +structure Generated_Cooper : sig
12.13 + type 'a eq
12.14 + val eq : 'a eq -> 'a -> 'a -> bool
12.15 + val eqa : 'a eq -> 'a -> 'a -> bool
12.16 + val leta : 'a -> ('a -> 'b) -> 'b
12.17 + val suc : IntInf.int -> IntInf.int
12.18 + datatype num = C of IntInf.int | Bound of IntInf.int |
12.19 + Cn of IntInf.int * IntInf.int * num | Neg of num | Add of num * num |
12.20 + Sub of num * num | Mul of IntInf.int * num
12.21 + datatype fm = T | F | Lt of num | Le of num | Gt of num | Ge of num |
12.22 + Eq of num | NEq of num | Dvd of IntInf.int * num | NDvd of IntInf.int * num
12.23 + | Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm |
12.24 + Iff of fm * fm | E of fm | A of fm | Closed of IntInf.int |
12.25 + NClosed of IntInf.int
12.26 + val map : ('a -> 'b) -> 'a list -> 'b list
12.27 + val append : 'a list -> 'a list -> 'a list
12.28 + val disjuncts : fm -> fm list
12.29 + val fm_case :
12.30 + 'a -> 'a -> (num -> 'a) ->
12.31 + (num -> 'a) ->
12.32 + (num -> 'a) ->
12.33 + (num -> 'a) ->
12.34 + (num -> 'a) ->
12.35 + (num -> 'a) ->
12.36 + (IntInf.int -> num -> 'a) ->
12.37 + (IntInf.int -> num -> 'a) ->
12.38 + (fm -> 'a) ->
12.39 + (fm -> fm -> 'a) ->
12.40 + (fm -> fm -> 'a) ->
12.41 + (fm -> fm -> 'a) ->
12.42 +(fm -> fm -> 'a) ->
12.43 + (fm -> 'a) ->
12.44 + (fm -> 'a) -> (IntInf.int -> 'a) -> (IntInf.int -> 'a) -> fm -> 'a
12.45 + val eq_num : num -> num -> bool
12.46 + val eq_fm : fm -> fm -> bool
12.47 + val djf : ('a -> fm) -> 'a -> fm -> fm
12.48 + val foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
12.49 + val evaldjf : ('a -> fm) -> 'a list -> fm
12.50 + val dj : (fm -> fm) -> fm -> fm
12.51 + val disj : fm -> fm -> fm
12.52 + val minus_nat : IntInf.int -> IntInf.int -> IntInf.int
12.53 + val decrnum : num -> num
12.54 + val decr : fm -> fm
12.55 + val concat_map : ('a -> 'b list) -> 'a list -> 'b list
12.56 + val numsubst0 : num -> num -> num
12.57 + val subst0 : num -> fm -> fm
12.58 + val minusinf : fm -> fm
12.59 + val eq_int : IntInf.int eq
12.60 + val zero_int : IntInf.int
12.61 + type 'a zero
12.62 + val zero : 'a zero -> 'a
12.63 + val zero_inta : IntInf.int zero
12.64 + type 'a times
12.65 + val times : 'a times -> 'a -> 'a -> 'a
12.66 + type 'a no_zero_divisors
12.67 + val times_no_zero_divisors : 'a no_zero_divisors -> 'a times
12.68 + val zero_no_zero_divisors : 'a no_zero_divisors -> 'a zero
12.69 + val times_int : IntInf.int times
12.70 + val no_zero_divisors_int : IntInf.int no_zero_divisors
12.71 + type 'a one
12.72 + val one : 'a one -> 'a
12.73 + type 'a zero_neq_one
12.74 + val one_zero_neq_one : 'a zero_neq_one -> 'a one
12.75 + val zero_zero_neq_one : 'a zero_neq_one -> 'a zero
12.76 + type 'a semigroup_mult
12.77 + val times_semigroup_mult : 'a semigroup_mult -> 'a times
12.78 + type 'a plus
12.79 + val plus : 'a plus -> 'a -> 'a -> 'a
12.80 + type 'a semigroup_add
12.81 + val plus_semigroup_add : 'a semigroup_add -> 'a plus
12.82 + type 'a ab_semigroup_add
12.83 + val semigroup_add_ab_semigroup_add : 'a ab_semigroup_add -> 'a semigroup_add
12.84 + type 'a semiring
12.85 + val ab_semigroup_add_semiring : 'a semiring -> 'a ab_semigroup_add
12.86 + val semigroup_mult_semiring : 'a semiring -> 'a semigroup_mult
12.87 + type 'a mult_zero
12.88 + val times_mult_zero : 'a mult_zero -> 'a times
12.89 + val zero_mult_zero : 'a mult_zero -> 'a zero
12.90 + type 'a monoid_add
12.91 + val semigroup_add_monoid_add : 'a monoid_add -> 'a semigroup_add
12.92 + val zero_monoid_add : 'a monoid_add -> 'a zero
12.93 + type 'a comm_monoid_add
12.94 + val ab_semigroup_add_comm_monoid_add :
12.95 + 'a comm_monoid_add -> 'a ab_semigroup_add
12.96 + val monoid_add_comm_monoid_add : 'a comm_monoid_add -> 'a monoid_add
12.97 + type 'a semiring_0
12.98 + val comm_monoid_add_semiring_0 : 'a semiring_0 -> 'a comm_monoid_add
12.99 + val mult_zero_semiring_0 : 'a semiring_0 -> 'a mult_zero
12.100 + val semiring_semiring_0 : 'a semiring_0 -> 'a semiring
12.101 + type 'a power
12.102 + val one_power : 'a power -> 'a one
12.103 + val times_power : 'a power -> 'a times
12.104 + type 'a monoid_mult
12.105 + val semigroup_mult_monoid_mult : 'a monoid_mult -> 'a semigroup_mult
12.106 + val power_monoid_mult : 'a monoid_mult -> 'a power
12.107 + type 'a semiring_1
12.108 + val monoid_mult_semiring_1 : 'a semiring_1 -> 'a monoid_mult
12.109 + val semiring_0_semiring_1 : 'a semiring_1 -> 'a semiring_0
12.110 + val zero_neq_one_semiring_1 : 'a semiring_1 -> 'a zero_neq_one
12.111 + type 'a cancel_semigroup_add
12.112 + val semigroup_add_cancel_semigroup_add :
12.113 + 'a cancel_semigroup_add -> 'a semigroup_add
12.114 + type 'a cancel_ab_semigroup_add
12.115 + val ab_semigroup_add_cancel_ab_semigroup_add :
12.116 + 'a cancel_ab_semigroup_add -> 'a ab_semigroup_add
12.117 + val cancel_semigroup_add_cancel_ab_semigroup_add :
12.118 + 'a cancel_ab_semigroup_add -> 'a cancel_semigroup_add
12.119 + type 'a cancel_comm_monoid_add
12.120 + val cancel_ab_semigroup_add_cancel_comm_monoid_add :
12.121 + 'a cancel_comm_monoid_add -> 'a cancel_ab_semigroup_add
12.122 + val comm_monoid_add_cancel_comm_monoid_add :
12.123 + 'a cancel_comm_monoid_add -> 'a comm_monoid_add
12.124 + type 'a semiring_0_cancel
12.125 + val cancel_comm_monoid_add_semiring_0_cancel :
12.126 + 'a semiring_0_cancel -> 'a cancel_comm_monoid_add
12.127 + val semiring_0_semiring_0_cancel : 'a semiring_0_cancel -> 'a semiring_0
12.128 + type 'a semiring_1_cancel
12.129 + val semiring_0_cancel_semiring_1_cancel :
12.130 + 'a semiring_1_cancel -> 'a semiring_0_cancel
12.131 + val semiring_1_semiring_1_cancel : 'a semiring_1_cancel -> 'a semiring_1
12.132 + type 'a dvd
12.133 + val times_dvd : 'a dvd -> 'a times
12.134 + type 'a ab_semigroup_mult
12.135 + val semigroup_mult_ab_semigroup_mult :
12.136 + 'a ab_semigroup_mult -> 'a semigroup_mult
12.137 + type 'a comm_semiring
12.138 + val ab_semigroup_mult_comm_semiring : 'a comm_semiring -> 'a ab_semigroup_mult
12.139 + val semiring_comm_semiring : 'a comm_semiring -> 'a semiring
12.140 + type 'a comm_semiring_0
12.141 + val comm_semiring_comm_semiring_0 : 'a comm_semiring_0 -> 'a comm_semiring
12.142 + val semiring_0_comm_semiring_0 : 'a comm_semiring_0 -> 'a semiring_0
12.143 + type 'a comm_monoid_mult
12.144 + val ab_semigroup_mult_comm_monoid_mult :
12.145 + 'a comm_monoid_mult -> 'a ab_semigroup_mult
12.146 + val monoid_mult_comm_monoid_mult : 'a comm_monoid_mult -> 'a monoid_mult
12.147 + type 'a comm_semiring_1
12.148 + val comm_monoid_mult_comm_semiring_1 :
12.149 + 'a comm_semiring_1 -> 'a comm_monoid_mult
12.150 + val comm_semiring_0_comm_semiring_1 : 'a comm_semiring_1 -> 'a comm_semiring_0
12.151 + val dvd_comm_semiring_1 : 'a comm_semiring_1 -> 'a dvd
12.152 + val semiring_1_comm_semiring_1 : 'a comm_semiring_1 -> 'a semiring_1
12.153 + type 'a comm_semiring_0_cancel
12.154 + val comm_semiring_0_comm_semiring_0_cancel :
12.155 + 'a comm_semiring_0_cancel -> 'a comm_semiring_0
12.156 + val semiring_0_cancel_comm_semiring_0_cancel :
12.157 + 'a comm_semiring_0_cancel -> 'a semiring_0_cancel
12.158 + type 'a comm_semiring_1_cancel
12.159 + val comm_semiring_0_cancel_comm_semiring_1_cancel :
12.160 + 'a comm_semiring_1_cancel -> 'a comm_semiring_0_cancel
12.161 + val comm_semiring_1_comm_semiring_1_cancel :
12.162 + 'a comm_semiring_1_cancel -> 'a comm_semiring_1
12.163 + val semiring_1_cancel_comm_semiring_1_cancel :
12.164 + 'a comm_semiring_1_cancel -> 'a semiring_1_cancel
12.165 + type 'a diva
12.166 + val dvd_div : 'a diva -> 'a dvd
12.167 + val diva : 'a diva -> 'a -> 'a -> 'a
12.168 + val moda : 'a diva -> 'a -> 'a -> 'a
12.169 + type 'a semiring_div
12.170 + val div_semiring_div : 'a semiring_div -> 'a diva
12.171 + val comm_semiring_1_cancel_semiring_div :
12.172 + 'a semiring_div -> 'a comm_semiring_1_cancel
12.173 + val no_zero_divisors_semiring_div : 'a semiring_div -> 'a no_zero_divisors
12.174 + val one_int : IntInf.int
12.175 + val one_inta : IntInf.int one
12.176 + val zero_neq_one_int : IntInf.int zero_neq_one
12.177 + val semigroup_mult_int : IntInf.int semigroup_mult
12.178 + val plus_int : IntInf.int plus
12.179 + val semigroup_add_int : IntInf.int semigroup_add
12.180 + val ab_semigroup_add_int : IntInf.int ab_semigroup_add
12.181 + val semiring_int : IntInf.int semiring
12.182 + val mult_zero_int : IntInf.int mult_zero
12.183 + val monoid_add_int : IntInf.int monoid_add
12.184 + val comm_monoid_add_int : IntInf.int comm_monoid_add
12.185 + val semiring_0_int : IntInf.int semiring_0
12.186 + val power_int : IntInf.int power
12.187 + val monoid_mult_int : IntInf.int monoid_mult
12.188 + val semiring_1_int : IntInf.int semiring_1
12.189 + val cancel_semigroup_add_int : IntInf.int cancel_semigroup_add
12.190 + val cancel_ab_semigroup_add_int : IntInf.int cancel_ab_semigroup_add
12.191 + val cancel_comm_monoid_add_int : IntInf.int cancel_comm_monoid_add
12.192 + val semiring_0_cancel_int : IntInf.int semiring_0_cancel
12.193 + val semiring_1_cancel_int : IntInf.int semiring_1_cancel
12.194 + val dvd_int : IntInf.int dvd
12.195 + val ab_semigroup_mult_int : IntInf.int ab_semigroup_mult
12.196 + val comm_semiring_int : IntInf.int comm_semiring
12.197 + val comm_semiring_0_int : IntInf.int comm_semiring_0
12.198 + val comm_monoid_mult_int : IntInf.int comm_monoid_mult
12.199 + val comm_semiring_1_int : IntInf.int comm_semiring_1
12.200 + val comm_semiring_0_cancel_int : IntInf.int comm_semiring_0_cancel
12.201 + val comm_semiring_1_cancel_int : IntInf.int comm_semiring_1_cancel
12.202 + val abs_int : IntInf.int -> IntInf.int
12.203 + val split : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
12.204 + val sgn_int : IntInf.int -> IntInf.int
12.205 + val apsnd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
12.206 + val divmod_int : IntInf.int -> IntInf.int -> IntInf.int * IntInf.int
12.207 + val snd : 'a * 'b -> 'b
12.208 + val mod_int : IntInf.int -> IntInf.int -> IntInf.int
12.209 + val fst : 'a * 'b -> 'a
12.210 + val div_int : IntInf.int -> IntInf.int -> IntInf.int
12.211 + val div_inta : IntInf.int diva
12.212 + val semiring_div_int : IntInf.int semiring_div
12.213 + val dvd : 'a semiring_div * 'a eq -> 'a -> 'a -> bool
12.214 + val num_case :
12.215 + (IntInf.int -> 'a) ->
12.216 + (IntInf.int -> 'a) ->
12.217 + (IntInf.int -> IntInf.int -> num -> 'a) ->
12.218 + (num -> 'a) ->
12.219 + (num -> num -> 'a) ->
12.220 + (num -> num -> 'a) -> (IntInf.int -> num -> 'a) -> num -> 'a
12.221 + val nummul : IntInf.int -> num -> num
12.222 + val numneg : num -> num
12.223 + val numadd : num * num -> num
12.224 + val numsub : num -> num -> num
12.225 + val simpnum : num -> num
12.226 + val nota : fm -> fm
12.227 + val iffa : fm -> fm -> fm
12.228 + val impa : fm -> fm -> fm
12.229 + val conj : fm -> fm -> fm
12.230 + val simpfm : fm -> fm
12.231 + val iupt : IntInf.int -> IntInf.int -> IntInf.int list
12.232 + val mirror : fm -> fm
12.233 + val size_list : 'a list -> IntInf.int
12.234 + val alpha : fm -> num list
12.235 + val beta : fm -> num list
12.236 + val eq_numa : num eq
12.237 + val member : 'a eq -> 'a -> 'a list -> bool
12.238 + val remdups : 'a eq -> 'a list -> 'a list
12.239 + val gcd_int : IntInf.int -> IntInf.int -> IntInf.int
12.240 + val lcm_int : IntInf.int -> IntInf.int -> IntInf.int
12.241 + val delta : fm -> IntInf.int
12.242 + val a_beta : fm -> IntInf.int -> fm
12.243 + val zeta : fm -> IntInf.int
12.244 + val zsplit0 : num -> IntInf.int * num
12.245 + val zlfm : fm -> fm
12.246 + val unita : fm -> fm * (num list * IntInf.int)
12.247 + val cooper : fm -> fm
12.248 + val prep : fm -> fm
12.249 + val qelim : fm -> (fm -> fm) -> fm
12.250 + val pa : fm -> fm
12.251 +end = struct
12.252
12.253 type 'a eq = {eq : 'a -> 'a -> bool};
12.254 -fun eq (A_:'a eq) = #eq A_;
12.255 +val eq = #eq : 'a eq -> 'a -> 'a -> bool;
12.256
12.257 -val eq_nat = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
12.258 -
12.259 -fun eqop A_ a b = eq A_ a b;
12.260 -
12.261 -fun divmod n m = (if eqop eq_nat m 0 then (0, n) else IntInf.divMod (n, m));
12.262 -
12.263 -fun snd (a, b) = b;
12.264 -
12.265 -fun mod_nat m n = snd (divmod m n);
12.266 -
12.267 -fun gcd m n = (if eqop eq_nat n 0 then m else gcd n (mod_nat m n));
12.268 -
12.269 -fun fst (a, b) = a;
12.270 -
12.271 -fun div_nat m n = fst (divmod m n);
12.272 -
12.273 -fun lcm m n = div_nat (IntInf.* (m, n)) (gcd m n);
12.274 +fun eqa A_ a b = eq A_ a b;
12.275
12.276 fun leta s f = f s;
12.277
12.278 -fun suc n = IntInf.+ (n, 1);
12.279 +fun suc n = IntInf.+ (n, (1 : IntInf.int));
12.280
12.281 -datatype num = Mul of IntInf.int * num | Sub of num * num | Add of num * num |
12.282 - Neg of num | Cn of IntInf.int * IntInf.int * num | Bound of IntInf.int |
12.283 - C of IntInf.int;
12.284 +datatype num = C of IntInf.int | Bound of IntInf.int |
12.285 + Cn of IntInf.int * IntInf.int * num | Neg of num | Add of num * num |
12.286 + Sub of num * num | Mul of IntInf.int * num;
12.287
12.288 -datatype fm = NClosed of IntInf.int | Closed of IntInf.int | A of fm | E of fm |
12.289 - Iff of fm * fm | Imp of fm * fm | Or of fm * fm | And of fm * fm | Not of fm |
12.290 - NDvd of IntInf.int * num | Dvd of IntInf.int * num | NEq of num | Eq of num |
12.291 - Ge of num | Gt of num | Le of num | Lt of num | F | T;
12.292 -
12.293 -fun abs_int i = (if IntInf.< (i, (0 : IntInf.int)) then IntInf.~ i else i);
12.294 -
12.295 -fun zlcm i j =
12.296 - (lcm (IntInf.max (0, (abs_int i))) (IntInf.max (0, (abs_int j))));
12.297 +datatype fm = T | F | Lt of num | Le of num | Gt of num | Ge of num | Eq of num
12.298 + | NEq of num | Dvd of IntInf.int * num | NDvd of IntInf.int * num | Not of fm
12.299 + | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | E of fm |
12.300 + A of fm | Closed of IntInf.int | NClosed of IntInf.int;
12.301
12.302 fun map f [] = []
12.303 | map f (x :: xs) = f x :: map f xs;
12.304 @@ -110,449 +324,441 @@
12.305 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
12.306 = f1;
12.307
12.308 -fun eq_num (Mul (c, d)) (Sub (a, b)) = false
12.309 - | eq_num (Mul (c, d)) (Add (a, b)) = false
12.310 - | eq_num (Sub (c, d)) (Add (a, b)) = false
12.311 - | eq_num (Mul (b, c)) (Neg a) = false
12.312 - | eq_num (Sub (b, c)) (Neg a) = false
12.313 - | eq_num (Add (b, c)) (Neg a) = false
12.314 - | eq_num (Mul (d, e)) (Cn (a, b, c)) = false
12.315 - | eq_num (Sub (d, e)) (Cn (a, b, c)) = false
12.316 - | eq_num (Add (d, e)) (Cn (a, b, c)) = false
12.317 - | eq_num (Neg d) (Cn (a, b, c)) = false
12.318 - | eq_num (Mul (b, c)) (Bound a) = false
12.319 - | eq_num (Sub (b, c)) (Bound a) = false
12.320 - | eq_num (Add (b, c)) (Bound a) = false
12.321 - | eq_num (Neg b) (Bound a) = false
12.322 - | eq_num (Cn (b, c, d)) (Bound a) = false
12.323 - | eq_num (Mul (b, c)) (C a) = false
12.324 - | eq_num (Sub (b, c)) (C a) = false
12.325 - | eq_num (Add (b, c)) (C a) = false
12.326 - | eq_num (Neg b) (C a) = false
12.327 - | eq_num (Cn (b, c, d)) (C a) = false
12.328 - | eq_num (Bound b) (C a) = false
12.329 - | eq_num (Sub (a, b)) (Mul (c, d)) = false
12.330 - | eq_num (Add (a, b)) (Mul (c, d)) = false
12.331 - | eq_num (Add (a, b)) (Sub (c, d)) = false
12.332 - | eq_num (Neg a) (Mul (b, c)) = false
12.333 - | eq_num (Neg a) (Sub (b, c)) = false
12.334 - | eq_num (Neg a) (Add (b, c)) = false
12.335 - | eq_num (Cn (a, b, c)) (Mul (d, e)) = false
12.336 - | eq_num (Cn (a, b, c)) (Sub (d, e)) = false
12.337 - | eq_num (Cn (a, b, c)) (Add (d, e)) = false
12.338 - | eq_num (Cn (a, b, c)) (Neg d) = false
12.339 - | eq_num (Bound a) (Mul (b, c)) = false
12.340 - | eq_num (Bound a) (Sub (b, c)) = false
12.341 - | eq_num (Bound a) (Add (b, c)) = false
12.342 - | eq_num (Bound a) (Neg b) = false
12.343 - | eq_num (Bound a) (Cn (b, c, d)) = false
12.344 - | eq_num (C a) (Mul (b, c)) = false
12.345 - | eq_num (C a) (Sub (b, c)) = false
12.346 - | eq_num (C a) (Add (b, c)) = false
12.347 - | eq_num (C a) (Neg b) = false
12.348 - | eq_num (C a) (Cn (b, c, d)) = false
12.349 - | eq_num (C a) (Bound b) = false
12.350 - | eq_num (Mul (inta, num)) (Mul (int', num')) =
12.351 - ((inta : IntInf.int) = int') andalso eq_num num num'
12.352 - | eq_num (Sub (num1, num2)) (Sub (num1', num2')) =
12.353 - eq_num num1 num1' andalso eq_num num2 num2'
12.354 - | eq_num (Add (num1, num2)) (Add (num1', num2')) =
12.355 - eq_num num1 num1' andalso eq_num num2 num2'
12.356 - | eq_num (Neg num) (Neg num') = eq_num num num'
12.357 - | eq_num (Cn (nat, inta, num)) (Cn (nat', int', num')) =
12.358 - ((nat : IntInf.int) = nat') andalso
12.359 - (((inta : IntInf.int) = int') andalso eq_num num num')
12.360 - | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat')
12.361 - | eq_num (C inta) (C int') = ((inta : IntInf.int) = int');
12.362 +fun eq_num (C intaa) (C inta) = ((intaa : IntInf.int) = inta)
12.363 + | eq_num (Bound nata) (Bound nat) = ((nata : IntInf.int) = nat)
12.364 + | eq_num (Cn (nata, intaa, numa)) (Cn (nat, inta, num)) =
12.365 + ((nata : IntInf.int) = nat) andalso
12.366 + (((intaa : IntInf.int) = inta) andalso eq_num numa num)
12.367 + | eq_num (Neg numa) (Neg num) = eq_num numa num
12.368 + | eq_num (Add (num1a, num2a)) (Add (num1, num2)) =
12.369 + eq_num num1a num1 andalso eq_num num2a num2
12.370 + | eq_num (Sub (num1a, num2a)) (Sub (num1, num2)) =
12.371 + eq_num num1a num1 andalso eq_num num2a num2
12.372 + | eq_num (Mul (intaa, numa)) (Mul (inta, num)) =
12.373 + ((intaa : IntInf.int) = inta) andalso eq_num numa num
12.374 + | eq_num (C inta) (Bound nat) = false
12.375 + | eq_num (Bound nat) (C inta) = false
12.376 + | eq_num (C intaa) (Cn (nat, inta, num)) = false
12.377 + | eq_num (Cn (nat, intaa, num)) (C inta) = false
12.378 + | eq_num (C inta) (Neg num) = false
12.379 + | eq_num (Neg num) (C inta) = false
12.380 + | eq_num (C inta) (Add (num1, num2)) = false
12.381 + | eq_num (Add (num1, num2)) (C inta) = false
12.382 + | eq_num (C inta) (Sub (num1, num2)) = false
12.383 + | eq_num (Sub (num1, num2)) (C inta) = false
12.384 + | eq_num (C intaa) (Mul (inta, num)) = false
12.385 + | eq_num (Mul (intaa, num)) (C inta) = false
12.386 + | eq_num (Bound nata) (Cn (nat, inta, num)) = false
12.387 + | eq_num (Cn (nata, inta, num)) (Bound nat) = false
12.388 + | eq_num (Bound nat) (Neg num) = false
12.389 + | eq_num (Neg num) (Bound nat) = false
12.390 + | eq_num (Bound nat) (Add (num1, num2)) = false
12.391 + | eq_num (Add (num1, num2)) (Bound nat) = false
12.392 + | eq_num (Bound nat) (Sub (num1, num2)) = false
12.393 + | eq_num (Sub (num1, num2)) (Bound nat) = false
12.394 + | eq_num (Bound nat) (Mul (inta, num)) = false
12.395 + | eq_num (Mul (inta, num)) (Bound nat) = false
12.396 + | eq_num (Cn (nat, inta, numa)) (Neg num) = false
12.397 + | eq_num (Neg numa) (Cn (nat, inta, num)) = false
12.398 + | eq_num (Cn (nat, inta, num)) (Add (num1, num2)) = false
12.399 + | eq_num (Add (num1, num2)) (Cn (nat, inta, num)) = false
12.400 + | eq_num (Cn (nat, inta, num)) (Sub (num1, num2)) = false
12.401 + | eq_num (Sub (num1, num2)) (Cn (nat, inta, num)) = false
12.402 + | eq_num (Cn (nat, intaa, numa)) (Mul (inta, num)) = false
12.403 + | eq_num (Mul (intaa, numa)) (Cn (nat, inta, num)) = false
12.404 + | eq_num (Neg num) (Add (num1, num2)) = false
12.405 + | eq_num (Add (num1, num2)) (Neg num) = false
12.406 + | eq_num (Neg num) (Sub (num1, num2)) = false
12.407 + | eq_num (Sub (num1, num2)) (Neg num) = false
12.408 + | eq_num (Neg numa) (Mul (inta, num)) = false
12.409 + | eq_num (Mul (inta, numa)) (Neg num) = false
12.410 + | eq_num (Add (num1a, num2a)) (Sub (num1, num2)) = false
12.411 + | eq_num (Sub (num1a, num2a)) (Add (num1, num2)) = false
12.412 + | eq_num (Add (num1, num2)) (Mul (inta, num)) = false
12.413 + | eq_num (Mul (inta, num)) (Add (num1, num2)) = false
12.414 + | eq_num (Sub (num1, num2)) (Mul (inta, num)) = false
12.415 + | eq_num (Mul (inta, num)) (Sub (num1, num2)) = false;
12.416
12.417 -fun eq_fm (NClosed b) (Closed a) = false
12.418 - | eq_fm (NClosed b) (A a) = false
12.419 - | eq_fm (Closed b) (A a) = false
12.420 - | eq_fm (NClosed b) (E a) = false
12.421 - | eq_fm (Closed b) (E a) = false
12.422 - | eq_fm (A b) (E a) = false
12.423 - | eq_fm (NClosed c) (Iff (a, b)) = false
12.424 - | eq_fm (Closed c) (Iff (a, b)) = false
12.425 - | eq_fm (A c) (Iff (a, b)) = false
12.426 - | eq_fm (E c) (Iff (a, b)) = false
12.427 - | eq_fm (NClosed c) (Imp (a, b)) = false
12.428 - | eq_fm (Closed c) (Imp (a, b)) = false
12.429 - | eq_fm (A c) (Imp (a, b)) = false
12.430 - | eq_fm (E c) (Imp (a, b)) = false
12.431 - | eq_fm (Iff (c, d)) (Imp (a, b)) = false
12.432 - | eq_fm (NClosed c) (Or (a, b)) = false
12.433 - | eq_fm (Closed c) (Or (a, b)) = false
12.434 - | eq_fm (A c) (Or (a, b)) = false
12.435 - | eq_fm (E c) (Or (a, b)) = false
12.436 - | eq_fm (Iff (c, d)) (Or (a, b)) = false
12.437 - | eq_fm (Imp (c, d)) (Or (a, b)) = false
12.438 - | eq_fm (NClosed c) (And (a, b)) = false
12.439 - | eq_fm (Closed c) (And (a, b)) = false
12.440 - | eq_fm (A c) (And (a, b)) = false
12.441 - | eq_fm (E c) (And (a, b)) = false
12.442 - | eq_fm (Iff (c, d)) (And (a, b)) = false
12.443 - | eq_fm (Imp (c, d)) (And (a, b)) = false
12.444 - | eq_fm (Or (c, d)) (And (a, b)) = false
12.445 - | eq_fm (NClosed b) (Not a) = false
12.446 - | eq_fm (Closed b) (Not a) = false
12.447 - | eq_fm (A b) (Not a) = false
12.448 - | eq_fm (E b) (Not a) = false
12.449 - | eq_fm (Iff (b, c)) (Not a) = false
12.450 - | eq_fm (Imp (b, c)) (Not a) = false
12.451 - | eq_fm (Or (b, c)) (Not a) = false
12.452 - | eq_fm (And (b, c)) (Not a) = false
12.453 - | eq_fm (NClosed c) (NDvd (a, b)) = false
12.454 - | eq_fm (Closed c) (NDvd (a, b)) = false
12.455 - | eq_fm (A c) (NDvd (a, b)) = false
12.456 - | eq_fm (E c) (NDvd (a, b)) = false
12.457 - | eq_fm (Iff (c, d)) (NDvd (a, b)) = false
12.458 - | eq_fm (Imp (c, d)) (NDvd (a, b)) = false
12.459 - | eq_fm (Or (c, d)) (NDvd (a, b)) = false
12.460 - | eq_fm (And (c, d)) (NDvd (a, b)) = false
12.461 - | eq_fm (Not c) (NDvd (a, b)) = false
12.462 - | eq_fm (NClosed c) (Dvd (a, b)) = false
12.463 - | eq_fm (Closed c) (Dvd (a, b)) = false
12.464 - | eq_fm (A c) (Dvd (a, b)) = false
12.465 - | eq_fm (E c) (Dvd (a, b)) = false
12.466 - | eq_fm (Iff (c, d)) (Dvd (a, b)) = false
12.467 - | eq_fm (Imp (c, d)) (Dvd (a, b)) = false
12.468 - | eq_fm (Or (c, d)) (Dvd (a, b)) = false
12.469 - | eq_fm (And (c, d)) (Dvd (a, b)) = false
12.470 - | eq_fm (Not c) (Dvd (a, b)) = false
12.471 - | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false
12.472 - | eq_fm (NClosed b) (NEq a) = false
12.473 - | eq_fm (Closed b) (NEq a) = false
12.474 - | eq_fm (A b) (NEq a) = false
12.475 - | eq_fm (E b) (NEq a) = false
12.476 - | eq_fm (Iff (b, c)) (NEq a) = false
12.477 - | eq_fm (Imp (b, c)) (NEq a) = false
12.478 - | eq_fm (Or (b, c)) (NEq a) = false
12.479 - | eq_fm (And (b, c)) (NEq a) = false
12.480 - | eq_fm (Not b) (NEq a) = false
12.481 - | eq_fm (NDvd (b, c)) (NEq a) = false
12.482 - | eq_fm (Dvd (b, c)) (NEq a) = false
12.483 - | eq_fm (NClosed b) (Eq a) = false
12.484 - | eq_fm (Closed b) (Eq a) = false
12.485 - | eq_fm (A b) (Eq a) = false
12.486 - | eq_fm (E b) (Eq a) = false
12.487 - | eq_fm (Iff (b, c)) (Eq a) = false
12.488 - | eq_fm (Imp (b, c)) (Eq a) = false
12.489 - | eq_fm (Or (b, c)) (Eq a) = false
12.490 - | eq_fm (And (b, c)) (Eq a) = false
12.491 - | eq_fm (Not b) (Eq a) = false
12.492 - | eq_fm (NDvd (b, c)) (Eq a) = false
12.493 - | eq_fm (Dvd (b, c)) (Eq a) = false
12.494 - | eq_fm (NEq b) (Eq a) = false
12.495 - | eq_fm (NClosed b) (Ge a) = false
12.496 - | eq_fm (Closed b) (Ge a) = false
12.497 - | eq_fm (A b) (Ge a) = false
12.498 - | eq_fm (E b) (Ge a) = false
12.499 - | eq_fm (Iff (b, c)) (Ge a) = false
12.500 - | eq_fm (Imp (b, c)) (Ge a) = false
12.501 - | eq_fm (Or (b, c)) (Ge a) = false
12.502 - | eq_fm (And (b, c)) (Ge a) = false
12.503 - | eq_fm (Not b) (Ge a) = false
12.504 - | eq_fm (NDvd (b, c)) (Ge a) = false
12.505 - | eq_fm (Dvd (b, c)) (Ge a) = false
12.506 - | eq_fm (NEq b) (Ge a) = false
12.507 - | eq_fm (Eq b) (Ge a) = false
12.508 - | eq_fm (NClosed b) (Gt a) = false
12.509 - | eq_fm (Closed b) (Gt a) = false
12.510 - | eq_fm (A b) (Gt a) = false
12.511 - | eq_fm (E b) (Gt a) = false
12.512 - | eq_fm (Iff (b, c)) (Gt a) = false
12.513 - | eq_fm (Imp (b, c)) (Gt a) = false
12.514 - | eq_fm (Or (b, c)) (Gt a) = false
12.515 - | eq_fm (And (b, c)) (Gt a) = false
12.516 - | eq_fm (Not b) (Gt a) = false
12.517 - | eq_fm (NDvd (b, c)) (Gt a) = false
12.518 - | eq_fm (Dvd (b, c)) (Gt a) = false
12.519 - | eq_fm (NEq b) (Gt a) = false
12.520 - | eq_fm (Eq b) (Gt a) = false
12.521 - | eq_fm (Ge b) (Gt a) = false
12.522 - | eq_fm (NClosed b) (Le a) = false
12.523 - | eq_fm (Closed b) (Le a) = false
12.524 - | eq_fm (A b) (Le a) = false
12.525 - | eq_fm (E b) (Le a) = false
12.526 - | eq_fm (Iff (b, c)) (Le a) = false
12.527 - | eq_fm (Imp (b, c)) (Le a) = false
12.528 - | eq_fm (Or (b, c)) (Le a) = false
12.529 - | eq_fm (And (b, c)) (Le a) = false
12.530 - | eq_fm (Not b) (Le a) = false
12.531 - | eq_fm (NDvd (b, c)) (Le a) = false
12.532 - | eq_fm (Dvd (b, c)) (Le a) = false
12.533 - | eq_fm (NEq b) (Le a) = false
12.534 - | eq_fm (Eq b) (Le a) = false
12.535 - | eq_fm (Ge b) (Le a) = false
12.536 - | eq_fm (Gt b) (Le a) = false
12.537 - | eq_fm (NClosed b) (Lt a) = false
12.538 - | eq_fm (Closed b) (Lt a) = false
12.539 - | eq_fm (A b) (Lt a) = false
12.540 - | eq_fm (E b) (Lt a) = false
12.541 - | eq_fm (Iff (b, c)) (Lt a) = false
12.542 - | eq_fm (Imp (b, c)) (Lt a) = false
12.543 - | eq_fm (Or (b, c)) (Lt a) = false
12.544 - | eq_fm (And (b, c)) (Lt a) = false
12.545 - | eq_fm (Not b) (Lt a) = false
12.546 - | eq_fm (NDvd (b, c)) (Lt a) = false
12.547 - | eq_fm (Dvd (b, c)) (Lt a) = false
12.548 - | eq_fm (NEq b) (Lt a) = false
12.549 - | eq_fm (Eq b) (Lt a) = false
12.550 - | eq_fm (Ge b) (Lt a) = false
12.551 - | eq_fm (Gt b) (Lt a) = false
12.552 - | eq_fm (Le b) (Lt a) = false
12.553 - | eq_fm (NClosed a) F = false
12.554 - | eq_fm (Closed a) F = false
12.555 - | eq_fm (A a) F = false
12.556 - | eq_fm (E a) F = false
12.557 - | eq_fm (Iff (a, b)) F = false
12.558 - | eq_fm (Imp (a, b)) F = false
12.559 - | eq_fm (Or (a, b)) F = false
12.560 - | eq_fm (And (a, b)) F = false
12.561 - | eq_fm (Not a) F = false
12.562 - | eq_fm (NDvd (a, b)) F = false
12.563 - | eq_fm (Dvd (a, b)) F = false
12.564 - | eq_fm (NEq a) F = false
12.565 - | eq_fm (Eq a) F = false
12.566 - | eq_fm (Ge a) F = false
12.567 - | eq_fm (Gt a) F = false
12.568 - | eq_fm (Le a) F = false
12.569 - | eq_fm (Lt a) F = false
12.570 - | eq_fm (NClosed a) T = false
12.571 - | eq_fm (Closed a) T = false
12.572 - | eq_fm (A a) T = false
12.573 - | eq_fm (E a) T = false
12.574 - | eq_fm (Iff (a, b)) T = false
12.575 - | eq_fm (Imp (a, b)) T = false
12.576 - | eq_fm (Or (a, b)) T = false
12.577 - | eq_fm (And (a, b)) T = false
12.578 - | eq_fm (Not a) T = false
12.579 - | eq_fm (NDvd (a, b)) T = false
12.580 - | eq_fm (Dvd (a, b)) T = false
12.581 - | eq_fm (NEq a) T = false
12.582 - | eq_fm (Eq a) T = false
12.583 - | eq_fm (Ge a) T = false
12.584 - | eq_fm (Gt a) T = false
12.585 - | eq_fm (Le a) T = false
12.586 - | eq_fm (Lt a) T = false
12.587 +fun eq_fm T T = true
12.588 + | eq_fm F F = true
12.589 + | eq_fm (Lt numa) (Lt num) = eq_num numa num
12.590 + | eq_fm (Le numa) (Le num) = eq_num numa num
12.591 + | eq_fm (Gt numa) (Gt num) = eq_num numa num
12.592 + | eq_fm (Ge numa) (Ge num) = eq_num numa num
12.593 + | eq_fm (Eq numa) (Eq num) = eq_num numa num
12.594 + | eq_fm (NEq numa) (NEq num) = eq_num numa num
12.595 + | eq_fm (Dvd (intaa, numa)) (Dvd (inta, num)) =
12.596 + ((intaa : IntInf.int) = inta) andalso eq_num numa num
12.597 + | eq_fm (NDvd (intaa, numa)) (NDvd (inta, num)) =
12.598 + ((intaa : IntInf.int) = inta) andalso eq_num numa num
12.599 + | eq_fm (Not fma) (Not fm) = eq_fm fma fm
12.600 + | eq_fm (And (fm1a, fm2a)) (And (fm1, fm2)) =
12.601 + eq_fm fm1a fm1 andalso eq_fm fm2a fm2
12.602 + | eq_fm (Or (fm1a, fm2a)) (Or (fm1, fm2)) =
12.603 + eq_fm fm1a fm1 andalso eq_fm fm2a fm2
12.604 + | eq_fm (Imp (fm1a, fm2a)) (Imp (fm1, fm2)) =
12.605 + eq_fm fm1a fm1 andalso eq_fm fm2a fm2
12.606 + | eq_fm (Iff (fm1a, fm2a)) (Iff (fm1, fm2)) =
12.607 + eq_fm fm1a fm1 andalso eq_fm fm2a fm2
12.608 + | eq_fm (E fma) (E fm) = eq_fm fma fm
12.609 + | eq_fm (A fma) (A fm) = eq_fm fma fm
12.610 + | eq_fm (Closed nata) (Closed nat) = ((nata : IntInf.int) = nat)
12.611 + | eq_fm (NClosed nata) (NClosed nat) = ((nata : IntInf.int) = nat)
12.612 + | eq_fm T F = false
12.613 | eq_fm F T = false
12.614 - | eq_fm (Closed a) (NClosed b) = false
12.615 - | eq_fm (A a) (NClosed b) = false
12.616 - | eq_fm (A a) (Closed b) = false
12.617 - | eq_fm (E a) (NClosed b) = false
12.618 - | eq_fm (E a) (Closed b) = false
12.619 - | eq_fm (E a) (A b) = false
12.620 - | eq_fm (Iff (a, b)) (NClosed c) = false
12.621 - | eq_fm (Iff (a, b)) (Closed c) = false
12.622 - | eq_fm (Iff (a, b)) (A c) = false
12.623 - | eq_fm (Iff (a, b)) (E c) = false
12.624 - | eq_fm (Imp (a, b)) (NClosed c) = false
12.625 - | eq_fm (Imp (a, b)) (Closed c) = false
12.626 - | eq_fm (Imp (a, b)) (A c) = false
12.627 - | eq_fm (Imp (a, b)) (E c) = false
12.628 - | eq_fm (Imp (a, b)) (Iff (c, d)) = false
12.629 - | eq_fm (Or (a, b)) (NClosed c) = false
12.630 - | eq_fm (Or (a, b)) (Closed c) = false
12.631 - | eq_fm (Or (a, b)) (A c) = false
12.632 - | eq_fm (Or (a, b)) (E c) = false
12.633 - | eq_fm (Or (a, b)) (Iff (c, d)) = false
12.634 - | eq_fm (Or (a, b)) (Imp (c, d)) = false
12.635 - | eq_fm (And (a, b)) (NClosed c) = false
12.636 - | eq_fm (And (a, b)) (Closed c) = false
12.637 - | eq_fm (And (a, b)) (A c) = false
12.638 - | eq_fm (And (a, b)) (E c) = false
12.639 - | eq_fm (And (a, b)) (Iff (c, d)) = false
12.640 - | eq_fm (And (a, b)) (Imp (c, d)) = false
12.641 - | eq_fm (And (a, b)) (Or (c, d)) = false
12.642 - | eq_fm (Not a) (NClosed b) = false
12.643 - | eq_fm (Not a) (Closed b) = false
12.644 - | eq_fm (Not a) (A b) = false
12.645 - | eq_fm (Not a) (E b) = false
12.646 - | eq_fm (Not a) (Iff (b, c)) = false
12.647 - | eq_fm (Not a) (Imp (b, c)) = false
12.648 - | eq_fm (Not a) (Or (b, c)) = false
12.649 - | eq_fm (Not a) (And (b, c)) = false
12.650 - | eq_fm (NDvd (a, b)) (NClosed c) = false
12.651 - | eq_fm (NDvd (a, b)) (Closed c) = false
12.652 - | eq_fm (NDvd (a, b)) (A c) = false
12.653 - | eq_fm (NDvd (a, b)) (E c) = false
12.654 - | eq_fm (NDvd (a, b)) (Iff (c, d)) = false
12.655 - | eq_fm (NDvd (a, b)) (Imp (c, d)) = false
12.656 - | eq_fm (NDvd (a, b)) (Or (c, d)) = false
12.657 - | eq_fm (NDvd (a, b)) (And (c, d)) = false
12.658 - | eq_fm (NDvd (a, b)) (Not c) = false
12.659 - | eq_fm (Dvd (a, b)) (NClosed c) = false
12.660 - | eq_fm (Dvd (a, b)) (Closed c) = false
12.661 - | eq_fm (Dvd (a, b)) (A c) = false
12.662 - | eq_fm (Dvd (a, b)) (E c) = false
12.663 - | eq_fm (Dvd (a, b)) (Iff (c, d)) = false
12.664 - | eq_fm (Dvd (a, b)) (Imp (c, d)) = false
12.665 - | eq_fm (Dvd (a, b)) (Or (c, d)) = false
12.666 - | eq_fm (Dvd (a, b)) (And (c, d)) = false
12.667 - | eq_fm (Dvd (a, b)) (Not c) = false
12.668 - | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false
12.669 - | eq_fm (NEq a) (NClosed b) = false
12.670 - | eq_fm (NEq a) (Closed b) = false
12.671 - | eq_fm (NEq a) (A b) = false
12.672 - | eq_fm (NEq a) (E b) = false
12.673 - | eq_fm (NEq a) (Iff (b, c)) = false
12.674 - | eq_fm (NEq a) (Imp (b, c)) = false
12.675 - | eq_fm (NEq a) (Or (b, c)) = false
12.676 - | eq_fm (NEq a) (And (b, c)) = false
12.677 - | eq_fm (NEq a) (Not b) = false
12.678 - | eq_fm (NEq a) (NDvd (b, c)) = false
12.679 - | eq_fm (NEq a) (Dvd (b, c)) = false
12.680 - | eq_fm (Eq a) (NClosed b) = false
12.681 - | eq_fm (Eq a) (Closed b) = false
12.682 - | eq_fm (Eq a) (A b) = false
12.683 - | eq_fm (Eq a) (E b) = false
12.684 - | eq_fm (Eq a) (Iff (b, c)) = false
12.685 - | eq_fm (Eq a) (Imp (b, c)) = false
12.686 - | eq_fm (Eq a) (Or (b, c)) = false
12.687 - | eq_fm (Eq a) (And (b, c)) = false
12.688 - | eq_fm (Eq a) (Not b) = false
12.689 - | eq_fm (Eq a) (NDvd (b, c)) = false
12.690 - | eq_fm (Eq a) (Dvd (b, c)) = false
12.691 - | eq_fm (Eq a) (NEq b) = false
12.692 - | eq_fm (Ge a) (NClosed b) = false
12.693 - | eq_fm (Ge a) (Closed b) = false
12.694 - | eq_fm (Ge a) (A b) = false
12.695 - | eq_fm (Ge a) (E b) = false
12.696 - | eq_fm (Ge a) (Iff (b, c)) = false
12.697 - | eq_fm (Ge a) (Imp (b, c)) = false
12.698 - | eq_fm (Ge a) (Or (b, c)) = false
12.699 - | eq_fm (Ge a) (And (b, c)) = false
12.700 - | eq_fm (Ge a) (Not b) = false
12.701 - | eq_fm (Ge a) (NDvd (b, c)) = false
12.702 - | eq_fm (Ge a) (Dvd (b, c)) = false
12.703 - | eq_fm (Ge a) (NEq b) = false
12.704 - | eq_fm (Ge a) (Eq b) = false
12.705 - | eq_fm (Gt a) (NClosed b) = false
12.706 - | eq_fm (Gt a) (Closed b) = false
12.707 - | eq_fm (Gt a) (A b) = false
12.708 - | eq_fm (Gt a) (E b) = false
12.709 - | eq_fm (Gt a) (Iff (b, c)) = false
12.710 - | eq_fm (Gt a) (Imp (b, c)) = false
12.711 - | eq_fm (Gt a) (Or (b, c)) = false
12.712 - | eq_fm (Gt a) (And (b, c)) = false
12.713 - | eq_fm (Gt a) (Not b) = false
12.714 - | eq_fm (Gt a) (NDvd (b, c)) = false
12.715 - | eq_fm (Gt a) (Dvd (b, c)) = false
12.716 - | eq_fm (Gt a) (NEq b) = false
12.717 - | eq_fm (Gt a) (Eq b) = false
12.718 - | eq_fm (Gt a) (Ge b) = false
12.719 - | eq_fm (Le a) (NClosed b) = false
12.720 - | eq_fm (Le a) (Closed b) = false
12.721 - | eq_fm (Le a) (A b) = false
12.722 - | eq_fm (Le a) (E b) = false
12.723 - | eq_fm (Le a) (Iff (b, c)) = false
12.724 - | eq_fm (Le a) (Imp (b, c)) = false
12.725 - | eq_fm (Le a) (Or (b, c)) = false
12.726 - | eq_fm (Le a) (And (b, c)) = false
12.727 - | eq_fm (Le a) (Not b) = false
12.728 - | eq_fm (Le a) (NDvd (b, c)) = false
12.729 - | eq_fm (Le a) (Dvd (b, c)) = false
12.730 - | eq_fm (Le a) (NEq b) = false
12.731 - | eq_fm (Le a) (Eq b) = false
12.732 - | eq_fm (Le a) (Ge b) = false
12.733 - | eq_fm (Le a) (Gt b) = false
12.734 - | eq_fm (Lt a) (NClosed b) = false
12.735 - | eq_fm (Lt a) (Closed b) = false
12.736 - | eq_fm (Lt a) (A b) = false
12.737 - | eq_fm (Lt a) (E b) = false
12.738 - | eq_fm (Lt a) (Iff (b, c)) = false
12.739 - | eq_fm (Lt a) (Imp (b, c)) = false
12.740 - | eq_fm (Lt a) (Or (b, c)) = false
12.741 - | eq_fm (Lt a) (And (b, c)) = false
12.742 - | eq_fm (Lt a) (Not b) = false
12.743 - | eq_fm (Lt a) (NDvd (b, c)) = false
12.744 - | eq_fm (Lt a) (Dvd (b, c)) = false
12.745 - | eq_fm (Lt a) (NEq b) = false
12.746 - | eq_fm (Lt a) (Eq b) = false
12.747 - | eq_fm (Lt a) (Ge b) = false
12.748 - | eq_fm (Lt a) (Gt b) = false
12.749 - | eq_fm (Lt a) (Le b) = false
12.750 - | eq_fm F (NClosed a) = false
12.751 - | eq_fm F (Closed a) = false
12.752 - | eq_fm F (A a) = false
12.753 - | eq_fm F (E a) = false
12.754 - | eq_fm F (Iff (a, b)) = false
12.755 - | eq_fm F (Imp (a, b)) = false
12.756 - | eq_fm F (Or (a, b)) = false
12.757 - | eq_fm F (And (a, b)) = false
12.758 - | eq_fm F (Not a) = false
12.759 - | eq_fm F (NDvd (a, b)) = false
12.760 - | eq_fm F (Dvd (a, b)) = false
12.761 - | eq_fm F (NEq a) = false
12.762 - | eq_fm F (Eq a) = false
12.763 - | eq_fm F (Ge a) = false
12.764 - | eq_fm F (Gt a) = false
12.765 - | eq_fm F (Le a) = false
12.766 - | eq_fm F (Lt a) = false
12.767 - | eq_fm T (NClosed a) = false
12.768 - | eq_fm T (Closed a) = false
12.769 - | eq_fm T (A a) = false
12.770 - | eq_fm T (E a) = false
12.771 - | eq_fm T (Iff (a, b)) = false
12.772 - | eq_fm T (Imp (a, b)) = false
12.773 - | eq_fm T (Or (a, b)) = false
12.774 - | eq_fm T (And (a, b)) = false
12.775 - | eq_fm T (Not a) = false
12.776 - | eq_fm T (NDvd (a, b)) = false
12.777 - | eq_fm T (Dvd (a, b)) = false
12.778 - | eq_fm T (NEq a) = false
12.779 - | eq_fm T (Eq a) = false
12.780 - | eq_fm T (Ge a) = false
12.781 - | eq_fm T (Gt a) = false
12.782 - | eq_fm T (Le a) = false
12.783 - | eq_fm T (Lt a) = false
12.784 - | eq_fm T F = false
12.785 - | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat')
12.786 - | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat')
12.787 - | eq_fm (A fm) (A fm') = eq_fm fm fm'
12.788 - | eq_fm (E fm) (E fm') = eq_fm fm fm'
12.789 - | eq_fm (Iff (fm1, fm2)) (Iff (fm1', fm2')) =
12.790 - eq_fm fm1 fm1' andalso eq_fm fm2 fm2'
12.791 - | eq_fm (Imp (fm1, fm2)) (Imp (fm1', fm2')) =
12.792 - eq_fm fm1 fm1' andalso eq_fm fm2 fm2'
12.793 - | eq_fm (Or (fm1, fm2)) (Or (fm1', fm2')) =
12.794 - eq_fm fm1 fm1' andalso eq_fm fm2 fm2'
12.795 - | eq_fm (And (fm1, fm2)) (And (fm1', fm2')) =
12.796 - eq_fm fm1 fm1' andalso eq_fm fm2 fm2'
12.797 - | eq_fm (Not fm) (Not fm') = eq_fm fm fm'
12.798 - | eq_fm (NDvd (inta, num)) (NDvd (int', num')) =
12.799 - ((inta : IntInf.int) = int') andalso eq_num num num'
12.800 - | eq_fm (Dvd (inta, num)) (Dvd (int', num')) =
12.801 - ((inta : IntInf.int) = int') andalso eq_num num num'
12.802 - | eq_fm (NEq num) (NEq num') = eq_num num num'
12.803 - | eq_fm (Eq num) (Eq num') = eq_num num num'
12.804 - | eq_fm (Ge num) (Ge num') = eq_num num num'
12.805 - | eq_fm (Gt num) (Gt num') = eq_num num num'
12.806 - | eq_fm (Le num) (Le num') = eq_num num num'
12.807 - | eq_fm (Lt num) (Lt num') = eq_num num num'
12.808 - | eq_fm F F = true
12.809 - | eq_fm T T = true;
12.810 -
12.811 -val eq_fma = {eq = eq_fm} : fm eq;
12.812 + | eq_fm T (Lt num) = false
12.813 + | eq_fm (Lt num) T = false
12.814 + | eq_fm T (Le num) = false
12.815 + | eq_fm (Le num) T = false
12.816 + | eq_fm T (Gt num) = false
12.817 + | eq_fm (Gt num) T = false
12.818 + | eq_fm T (Ge num) = false
12.819 + | eq_fm (Ge num) T = false
12.820 + | eq_fm T (Eq num) = false
12.821 + | eq_fm (Eq num) T = false
12.822 + | eq_fm T (NEq num) = false
12.823 + | eq_fm (NEq num) T = false
12.824 + | eq_fm T (Dvd (inta, num)) = false
12.825 + | eq_fm (Dvd (inta, num)) T = false
12.826 + | eq_fm T (NDvd (inta, num)) = false
12.827 + | eq_fm (NDvd (inta, num)) T = false
12.828 + | eq_fm T (Not fm) = false
12.829 + | eq_fm (Not fm) T = false
12.830 + | eq_fm T (And (fm1, fm2)) = false
12.831 + | eq_fm (And (fm1, fm2)) T = false
12.832 + | eq_fm T (Or (fm1, fm2)) = false
12.833 + | eq_fm (Or (fm1, fm2)) T = false
12.834 + | eq_fm T (Imp (fm1, fm2)) = false
12.835 + | eq_fm (Imp (fm1, fm2)) T = false
12.836 + | eq_fm T (Iff (fm1, fm2)) = false
12.837 + | eq_fm (Iff (fm1, fm2)) T = false
12.838 + | eq_fm T (E fm) = false
12.839 + | eq_fm (E fm) T = false
12.840 + | eq_fm T (A fm) = false
12.841 + | eq_fm (A fm) T = false
12.842 + | eq_fm T (Closed nat) = false
12.843 + | eq_fm (Closed nat) T = false
12.844 + | eq_fm T (NClosed nat) = false
12.845 + | eq_fm (NClosed nat) T = false
12.846 + | eq_fm F (Lt num) = false
12.847 + | eq_fm (Lt num) F = false
12.848 + | eq_fm F (Le num) = false
12.849 + | eq_fm (Le num) F = false
12.850 + | eq_fm F (Gt num) = false
12.851 + | eq_fm (Gt num) F = false
12.852 + | eq_fm F (Ge num) = false
12.853 + | eq_fm (Ge num) F = false
12.854 + | eq_fm F (Eq num) = false
12.855 + | eq_fm (Eq num) F = false
12.856 + | eq_fm F (NEq num) = false
12.857 + | eq_fm (NEq num) F = false
12.858 + | eq_fm F (Dvd (inta, num)) = false
12.859 + | eq_fm (Dvd (inta, num)) F = false
12.860 + | eq_fm F (NDvd (inta, num)) = false
12.861 + | eq_fm (NDvd (inta, num)) F = false
12.862 + | eq_fm F (Not fm) = false
12.863 + | eq_fm (Not fm) F = false
12.864 + | eq_fm F (And (fm1, fm2)) = false
12.865 + | eq_fm (And (fm1, fm2)) F = false
12.866 + | eq_fm F (Or (fm1, fm2)) = false
12.867 + | eq_fm (Or (fm1, fm2)) F = false
12.868 + | eq_fm F (Imp (fm1, fm2)) = false
12.869 + | eq_fm (Imp (fm1, fm2)) F = false
12.870 + | eq_fm F (Iff (fm1, fm2)) = false
12.871 + | eq_fm (Iff (fm1, fm2)) F = false
12.872 + | eq_fm F (E fm) = false
12.873 + | eq_fm (E fm) F = false
12.874 + | eq_fm F (A fm) = false
12.875 + | eq_fm (A fm) F = false
12.876 + | eq_fm F (Closed nat) = false
12.877 + | eq_fm (Closed nat) F = false
12.878 + | eq_fm F (NClosed nat) = false
12.879 + | eq_fm (NClosed nat) F = false
12.880 + | eq_fm (Lt numa) (Le num) = false
12.881 + | eq_fm (Le numa) (Lt num) = false
12.882 + | eq_fm (Lt numa) (Gt num) = false
12.883 + | eq_fm (Gt numa) (Lt num) = false
12.884 + | eq_fm (Lt numa) (Ge num) = false
12.885 + | eq_fm (Ge numa) (Lt num) = false
12.886 + | eq_fm (Lt numa) (Eq num) = false
12.887 + | eq_fm (Eq numa) (Lt num) = false
12.888 + | eq_fm (Lt numa) (NEq num) = false
12.889 + | eq_fm (NEq numa) (Lt num) = false
12.890 + | eq_fm (Lt numa) (Dvd (inta, num)) = false
12.891 + | eq_fm (Dvd (inta, numa)) (Lt num) = false
12.892 + | eq_fm (Lt numa) (NDvd (inta, num)) = false
12.893 + | eq_fm (NDvd (inta, numa)) (Lt num) = false
12.894 + | eq_fm (Lt num) (Not fm) = false
12.895 + | eq_fm (Not fm) (Lt num) = false
12.896 + | eq_fm (Lt num) (And (fm1, fm2)) = false
12.897 + | eq_fm (And (fm1, fm2)) (Lt num) = false
12.898 + | eq_fm (Lt num) (Or (fm1, fm2)) = false
12.899 + | eq_fm (Or (fm1, fm2)) (Lt num) = false
12.900 + | eq_fm (Lt num) (Imp (fm1, fm2)) = false
12.901 + | eq_fm (Imp (fm1, fm2)) (Lt num) = false
12.902 + | eq_fm (Lt num) (Iff (fm1, fm2)) = false
12.903 + | eq_fm (Iff (fm1, fm2)) (Lt num) = false
12.904 + | eq_fm (Lt num) (E fm) = false
12.905 + | eq_fm (E fm) (Lt num) = false
12.906 + | eq_fm (Lt num) (A fm) = false
12.907 + | eq_fm (A fm) (Lt num) = false
12.908 + | eq_fm (Lt num) (Closed nat) = false
12.909 + | eq_fm (Closed nat) (Lt num) = false
12.910 + | eq_fm (Lt num) (NClosed nat) = false
12.911 + | eq_fm (NClosed nat) (Lt num) = false
12.912 + | eq_fm (Le numa) (Gt num) = false
12.913 + | eq_fm (Gt numa) (Le num) = false
12.914 + | eq_fm (Le numa) (Ge num) = false
12.915 + | eq_fm (Ge numa) (Le num) = false
12.916 + | eq_fm (Le numa) (Eq num) = false
12.917 + | eq_fm (Eq numa) (Le num) = false
12.918 + | eq_fm (Le numa) (NEq num) = false
12.919 + | eq_fm (NEq numa) (Le num) = false
12.920 + | eq_fm (Le numa) (Dvd (inta, num)) = false
12.921 + | eq_fm (Dvd (inta, numa)) (Le num) = false
12.922 + | eq_fm (Le numa) (NDvd (inta, num)) = false
12.923 + | eq_fm (NDvd (inta, numa)) (Le num) = false
12.924 + | eq_fm (Le num) (Not fm) = false
12.925 + | eq_fm (Not fm) (Le num) = false
12.926 + | eq_fm (Le num) (And (fm1, fm2)) = false
12.927 + | eq_fm (And (fm1, fm2)) (Le num) = false
12.928 + | eq_fm (Le num) (Or (fm1, fm2)) = false
12.929 + | eq_fm (Or (fm1, fm2)) (Le num) = false
12.930 + | eq_fm (Le num) (Imp (fm1, fm2)) = false
12.931 + | eq_fm (Imp (fm1, fm2)) (Le num) = false
12.932 + | eq_fm (Le num) (Iff (fm1, fm2)) = false
12.933 + | eq_fm (Iff (fm1, fm2)) (Le num) = false
12.934 + | eq_fm (Le num) (E fm) = false
12.935 + | eq_fm (E fm) (Le num) = false
12.936 + | eq_fm (Le num) (A fm) = false
12.937 + | eq_fm (A fm) (Le num) = false
12.938 + | eq_fm (Le num) (Closed nat) = false
12.939 + | eq_fm (Closed nat) (Le num) = false
12.940 + | eq_fm (Le num) (NClosed nat) = false
12.941 + | eq_fm (NClosed nat) (Le num) = false
12.942 + | eq_fm (Gt numa) (Ge num) = false
12.943 + | eq_fm (Ge numa) (Gt num) = false
12.944 + | eq_fm (Gt numa) (Eq num) = false
12.945 + | eq_fm (Eq numa) (Gt num) = false
12.946 + | eq_fm (Gt numa) (NEq num) = false
12.947 + | eq_fm (NEq numa) (Gt num) = false
12.948 + | eq_fm (Gt numa) (Dvd (inta, num)) = false
12.949 + | eq_fm (Dvd (inta, numa)) (Gt num) = false
12.950 + | eq_fm (Gt numa) (NDvd (inta, num)) = false
12.951 + | eq_fm (NDvd (inta, numa)) (Gt num) = false
12.952 + | eq_fm (Gt num) (Not fm) = false
12.953 + | eq_fm (Not fm) (Gt num) = false
12.954 + | eq_fm (Gt num) (And (fm1, fm2)) = false
12.955 + | eq_fm (And (fm1, fm2)) (Gt num) = false
12.956 + | eq_fm (Gt num) (Or (fm1, fm2)) = false
12.957 + | eq_fm (Or (fm1, fm2)) (Gt num) = false
12.958 + | eq_fm (Gt num) (Imp (fm1, fm2)) = false
12.959 + | eq_fm (Imp (fm1, fm2)) (Gt num) = false
12.960 + | eq_fm (Gt num) (Iff (fm1, fm2)) = false
12.961 + | eq_fm (Iff (fm1, fm2)) (Gt num) = false
12.962 + | eq_fm (Gt num) (E fm) = false
12.963 + | eq_fm (E fm) (Gt num) = false
12.964 + | eq_fm (Gt num) (A fm) = false
12.965 + | eq_fm (A fm) (Gt num) = false
12.966 + | eq_fm (Gt num) (Closed nat) = false
12.967 + | eq_fm (Closed nat) (Gt num) = false
12.968 + | eq_fm (Gt num) (NClosed nat) = false
12.969 + | eq_fm (NClosed nat) (Gt num) = false
12.970 + | eq_fm (Ge numa) (Eq num) = false
12.971 + | eq_fm (Eq numa) (Ge num) = false
12.972 + | eq_fm (Ge numa) (NEq num) = false
12.973 + | eq_fm (NEq numa) (Ge num) = false
12.974 + | eq_fm (Ge numa) (Dvd (inta, num)) = false
12.975 + | eq_fm (Dvd (inta, numa)) (Ge num) = false
12.976 + | eq_fm (Ge numa) (NDvd (inta, num)) = false
12.977 + | eq_fm (NDvd (inta, numa)) (Ge num) = false
12.978 + | eq_fm (Ge num) (Not fm) = false
12.979 + | eq_fm (Not fm) (Ge num) = false
12.980 + | eq_fm (Ge num) (And (fm1, fm2)) = false
12.981 + | eq_fm (And (fm1, fm2)) (Ge num) = false
12.982 + | eq_fm (Ge num) (Or (fm1, fm2)) = false
12.983 + | eq_fm (Or (fm1, fm2)) (Ge num) = false
12.984 + | eq_fm (Ge num) (Imp (fm1, fm2)) = false
12.985 + | eq_fm (Imp (fm1, fm2)) (Ge num) = false
12.986 + | eq_fm (Ge num) (Iff (fm1, fm2)) = false
12.987 + | eq_fm (Iff (fm1, fm2)) (Ge num) = false
12.988 + | eq_fm (Ge num) (E fm) = false
12.989 + | eq_fm (E fm) (Ge num) = false
12.990 + | eq_fm (Ge num) (A fm) = false
12.991 + | eq_fm (A fm) (Ge num) = false
12.992 + | eq_fm (Ge num) (Closed nat) = false
12.993 + | eq_fm (Closed nat) (Ge num) = false
12.994 + | eq_fm (Ge num) (NClosed nat) = false
12.995 + | eq_fm (NClosed nat) (Ge num) = false
12.996 + | eq_fm (Eq numa) (NEq num) = false
12.997 + | eq_fm (NEq numa) (Eq num) = false
12.998 + | eq_fm (Eq numa) (Dvd (inta, num)) = false
12.999 + | eq_fm (Dvd (inta, numa)) (Eq num) = false
12.1000 + | eq_fm (Eq numa) (NDvd (inta, num)) = false
12.1001 + | eq_fm (NDvd (inta, numa)) (Eq num) = false
12.1002 + | eq_fm (Eq num) (Not fm) = false
12.1003 + | eq_fm (Not fm) (Eq num) = false
12.1004 + | eq_fm (Eq num) (And (fm1, fm2)) = false
12.1005 + | eq_fm (And (fm1, fm2)) (Eq num) = false
12.1006 + | eq_fm (Eq num) (Or (fm1, fm2)) = false
12.1007 + | eq_fm (Or (fm1, fm2)) (Eq num) = false
12.1008 + | eq_fm (Eq num) (Imp (fm1, fm2)) = false
12.1009 + | eq_fm (Imp (fm1, fm2)) (Eq num) = false
12.1010 + | eq_fm (Eq num) (Iff (fm1, fm2)) = false
12.1011 + | eq_fm (Iff (fm1, fm2)) (Eq num) = false
12.1012 + | eq_fm (Eq num) (E fm) = false
12.1013 + | eq_fm (E fm) (Eq num) = false
12.1014 + | eq_fm (Eq num) (A fm) = false
12.1015 + | eq_fm (A fm) (Eq num) = false
12.1016 + | eq_fm (Eq num) (Closed nat) = false
12.1017 + | eq_fm (Closed nat) (Eq num) = false
12.1018 + | eq_fm (Eq num) (NClosed nat) = false
12.1019 + | eq_fm (NClosed nat) (Eq num) = false
12.1020 + | eq_fm (NEq numa) (Dvd (inta, num)) = false
12.1021 + | eq_fm (Dvd (inta, numa)) (NEq num) = false
12.1022 + | eq_fm (NEq numa) (NDvd (inta, num)) = false
12.1023 + | eq_fm (NDvd (inta, numa)) (NEq num) = false
12.1024 + | eq_fm (NEq num) (Not fm) = false
12.1025 + | eq_fm (Not fm) (NEq num) = false
12.1026 + | eq_fm (NEq num) (And (fm1, fm2)) = false
12.1027 + | eq_fm (And (fm1, fm2)) (NEq num) = false
12.1028 + | eq_fm (NEq num) (Or (fm1, fm2)) = false
12.1029 + | eq_fm (Or (fm1, fm2)) (NEq num) = false
12.1030 + | eq_fm (NEq num) (Imp (fm1, fm2)) = false
12.1031 + | eq_fm (Imp (fm1, fm2)) (NEq num) = false
12.1032 + | eq_fm (NEq num) (Iff (fm1, fm2)) = false
12.1033 + | eq_fm (Iff (fm1, fm2)) (NEq num) = false
12.1034 + | eq_fm (NEq num) (E fm) = false
12.1035 + | eq_fm (E fm) (NEq num) = false
12.1036 + | eq_fm (NEq num) (A fm) = false
12.1037 + | eq_fm (A fm) (NEq num) = false
12.1038 + | eq_fm (NEq num) (Closed nat) = false
12.1039 + | eq_fm (Closed nat) (NEq num) = false
12.1040 + | eq_fm (NEq num) (NClosed nat) = false
12.1041 + | eq_fm (NClosed nat) (NEq num) = false
12.1042 + | eq_fm (Dvd (intaa, numa)) (NDvd (inta, num)) = false
12.1043 + | eq_fm (NDvd (intaa, numa)) (Dvd (inta, num)) = false
12.1044 + | eq_fm (Dvd (inta, num)) (Not fm) = false
12.1045 + | eq_fm (Not fm) (Dvd (inta, num)) = false
12.1046 + | eq_fm (Dvd (inta, num)) (And (fm1, fm2)) = false
12.1047 + | eq_fm (And (fm1, fm2)) (Dvd (inta, num)) = false
12.1048 + | eq_fm (Dvd (inta, num)) (Or (fm1, fm2)) = false
12.1049 + | eq_fm (Or (fm1, fm2)) (Dvd (inta, num)) = false
12.1050 + | eq_fm (Dvd (inta, num)) (Imp (fm1, fm2)) = false
12.1051 + | eq_fm (Imp (fm1, fm2)) (Dvd (inta, num)) = false
12.1052 + | eq_fm (Dvd (inta, num)) (Iff (fm1, fm2)) = false
12.1053 + | eq_fm (Iff (fm1, fm2)) (Dvd (inta, num)) = false
12.1054 + | eq_fm (Dvd (inta, num)) (E fm) = false
12.1055 + | eq_fm (E fm) (Dvd (inta, num)) = false
12.1056 + | eq_fm (Dvd (inta, num)) (A fm) = false
12.1057 + | eq_fm (A fm) (Dvd (inta, num)) = false
12.1058 + | eq_fm (Dvd (inta, num)) (Closed nat) = false
12.1059 + | eq_fm (Closed nat) (Dvd (inta, num)) = false
12.1060 + | eq_fm (Dvd (inta, num)) (NClosed nat) = false
12.1061 + | eq_fm (NClosed nat) (Dvd (inta, num)) = false
12.1062 + | eq_fm (NDvd (inta, num)) (Not fm) = false
12.1063 + | eq_fm (Not fm) (NDvd (inta, num)) = false
12.1064 + | eq_fm (NDvd (inta, num)) (And (fm1, fm2)) = false
12.1065 + | eq_fm (And (fm1, fm2)) (NDvd (inta, num)) = false
12.1066 + | eq_fm (NDvd (inta, num)) (Or (fm1, fm2)) = false
12.1067 + | eq_fm (Or (fm1, fm2)) (NDvd (inta, num)) = false
12.1068 + | eq_fm (NDvd (inta, num)) (Imp (fm1, fm2)) = false
12.1069 + | eq_fm (Imp (fm1, fm2)) (NDvd (inta, num)) = false
12.1070 + | eq_fm (NDvd (inta, num)) (Iff (fm1, fm2)) = false
12.1071 + | eq_fm (Iff (fm1, fm2)) (NDvd (inta, num)) = false
12.1072 + | eq_fm (NDvd (inta, num)) (E fm) = false
12.1073 + | eq_fm (E fm) (NDvd (inta, num)) = false
12.1074 + | eq_fm (NDvd (inta, num)) (A fm) = false
12.1075 + | eq_fm (A fm) (NDvd (inta, num)) = false
12.1076 + | eq_fm (NDvd (inta, num)) (Closed nat) = false
12.1077 + | eq_fm (Closed nat) (NDvd (inta, num)) = false
12.1078 + | eq_fm (NDvd (inta, num)) (NClosed nat) = false
12.1079 + | eq_fm (NClosed nat) (NDvd (inta, num)) = false
12.1080 + | eq_fm (Not fm) (And (fm1, fm2)) = false
12.1081 + | eq_fm (And (fm1, fm2)) (Not fm) = false
12.1082 + | eq_fm (Not fm) (Or (fm1, fm2)) = false
12.1083 + | eq_fm (Or (fm1, fm2)) (Not fm) = false
12.1084 + | eq_fm (Not fm) (Imp (fm1, fm2)) = false
12.1085 + | eq_fm (Imp (fm1, fm2)) (Not fm) = false
12.1086 + | eq_fm (Not fm) (Iff (fm1, fm2)) = false
12.1087 + | eq_fm (Iff (fm1, fm2)) (Not fm) = false
12.1088 + | eq_fm (Not fma) (E fm) = false
12.1089 + | eq_fm (E fma) (Not fm) = false
12.1090 + | eq_fm (Not fma) (A fm) = false
12.1091 + | eq_fm (A fma) (Not fm) = false
12.1092 + | eq_fm (Not fm) (Closed nat) = false
12.1093 + | eq_fm (Closed nat) (Not fm) = false
12.1094 + | eq_fm (Not fm) (NClosed nat) = false
12.1095 + | eq_fm (NClosed nat) (Not fm) = false
12.1096 + | eq_fm (And (fm1a, fm2a)) (Or (fm1, fm2)) = false
12.1097 + | eq_fm (Or (fm1a, fm2a)) (And (fm1, fm2)) = false
12.1098 + | eq_fm (And (fm1a, fm2a)) (Imp (fm1, fm2)) = false
12.1099 + | eq_fm (Imp (fm1a, fm2a)) (And (fm1, fm2)) = false
12.1100 + | eq_fm (And (fm1a, fm2a)) (Iff (fm1, fm2)) = false
12.1101 + | eq_fm (Iff (fm1a, fm2a)) (And (fm1, fm2)) = false
12.1102 + | eq_fm (And (fm1, fm2)) (E fm) = false
12.1103 + | eq_fm (E fm) (And (fm1, fm2)) = false
12.1104 + | eq_fm (And (fm1, fm2)) (A fm) = false
12.1105 + | eq_fm (A fm) (And (fm1, fm2)) = false
12.1106 + | eq_fm (And (fm1, fm2)) (Closed nat) = false
12.1107 + | eq_fm (Closed nat) (And (fm1, fm2)) = false
12.1108 + | eq_fm (And (fm1, fm2)) (NClosed nat) = false
12.1109 + | eq_fm (NClosed nat) (And (fm1, fm2)) = false
12.1110 + | eq_fm (Or (fm1a, fm2a)) (Imp (fm1, fm2)) = false
12.1111 + | eq_fm (Imp (fm1a, fm2a)) (Or (fm1, fm2)) = false
12.1112 + | eq_fm (Or (fm1a, fm2a)) (Iff (fm1, fm2)) = false
12.1113 + | eq_fm (Iff (fm1a, fm2a)) (Or (fm1, fm2)) = false
12.1114 + | eq_fm (Or (fm1, fm2)) (E fm) = false
12.1115 + | eq_fm (E fm) (Or (fm1, fm2)) = false
12.1116 + | eq_fm (Or (fm1, fm2)) (A fm) = false
12.1117 + | eq_fm (A fm) (Or (fm1, fm2)) = false
12.1118 + | eq_fm (Or (fm1, fm2)) (Closed nat) = false
12.1119 + | eq_fm (Closed nat) (Or (fm1, fm2)) = false
12.1120 + | eq_fm (Or (fm1, fm2)) (NClosed nat) = false
12.1121 + | eq_fm (NClosed nat) (Or (fm1, fm2)) = false
12.1122 + | eq_fm (Imp (fm1a, fm2a)) (Iff (fm1, fm2)) = false
12.1123 + | eq_fm (Iff (fm1a, fm2a)) (Imp (fm1, fm2)) = false
12.1124 + | eq_fm (Imp (fm1, fm2)) (E fm) = false
12.1125 + | eq_fm (E fm) (Imp (fm1, fm2)) = false
12.1126 + | eq_fm (Imp (fm1, fm2)) (A fm) = false
12.1127 + | eq_fm (A fm) (Imp (fm1, fm2)) = false
12.1128 + | eq_fm (Imp (fm1, fm2)) (Closed nat) = false
12.1129 + | eq_fm (Closed nat) (Imp (fm1, fm2)) = false
12.1130 + | eq_fm (Imp (fm1, fm2)) (NClosed nat) = false
12.1131 + | eq_fm (NClosed nat) (Imp (fm1, fm2)) = false
12.1132 + | eq_fm (Iff (fm1, fm2)) (E fm) = false
12.1133 + | eq_fm (E fm) (Iff (fm1, fm2)) = false
12.1134 + | eq_fm (Iff (fm1, fm2)) (A fm) = false
12.1135 + | eq_fm (A fm) (Iff (fm1, fm2)) = false
12.1136 + | eq_fm (Iff (fm1, fm2)) (Closed nat) = false
12.1137 + | eq_fm (Closed nat) (Iff (fm1, fm2)) = false
12.1138 + | eq_fm (Iff (fm1, fm2)) (NClosed nat) = false
12.1139 + | eq_fm (NClosed nat) (Iff (fm1, fm2)) = false
12.1140 + | eq_fm (E fma) (A fm) = false
12.1141 + | eq_fm (A fma) (E fm) = false
12.1142 + | eq_fm (E fm) (Closed nat) = false
12.1143 + | eq_fm (Closed nat) (E fm) = false
12.1144 + | eq_fm (E fm) (NClosed nat) = false
12.1145 + | eq_fm (NClosed nat) (E fm) = false
12.1146 + | eq_fm (A fm) (Closed nat) = false
12.1147 + | eq_fm (Closed nat) (A fm) = false
12.1148 + | eq_fm (A fm) (NClosed nat) = false
12.1149 + | eq_fm (NClosed nat) (A fm) = false
12.1150 + | eq_fm (Closed nata) (NClosed nat) = false
12.1151 + | eq_fm (NClosed nata) (Closed nat) = false;
12.1152
12.1153 fun djf f p q =
12.1154 - (if eqop eq_fma q T then T
12.1155 - else (if eqop eq_fma q F then f p
12.1156 - else let
12.1157 - val a = f p;
12.1158 - in
12.1159 - (case a of T => T | F => q | Lt num => Or (f p, q)
12.1160 - | Le num => Or (f p, q) | Gt num => Or (f p, q)
12.1161 - | Ge num => Or (f p, q) | Eq num => Or (f p, q)
12.1162 - | NEq num => Or (f p, q) | Dvd (inta, num) => Or (f p, q)
12.1163 - | NDvd (inta, num) => Or (f p, q) | Not fm => Or (f p, q)
12.1164 - | And (fm1, fm2) => Or (f p, q)
12.1165 - | Or (fm1, fm2) => Or (f p, q)
12.1166 - | Imp (fm1, fm2) => Or (f p, q)
12.1167 - | Iff (fm1, fm2) => Or (f p, q) | E fm => Or (f p, q)
12.1168 - | A fm => Or (f p, q) | Closed nat => Or (f p, q)
12.1169 - | NClosed nat => Or (f p, q))
12.1170 - end));
12.1171 + (if eq_fm q T then T
12.1172 + else (if eq_fm q F then f p
12.1173 + else (case f p of T => T | F => q | Lt _ => Or (f p, q)
12.1174 + | Le _ => Or (f p, q) | Gt _ => Or (f p, q)
12.1175 + | Ge _ => Or (f p, q) | Eq _ => Or (f p, q)
12.1176 + | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q)
12.1177 + | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q)
12.1178 + | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q)
12.1179 + | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q)
12.1180 + | E _ => Or (f p, q) | A _ => Or (f p, q)
12.1181 + | Closed _ => Or (f p, q) | NClosed _ => Or (f p, q))));
12.1182
12.1183 fun foldr f [] a = a
12.1184 | foldr f (x :: xs) a = f x (foldr f xs a);
12.1185 @@ -562,18 +768,17 @@
12.1186 fun dj f p = evaldjf f (disjuncts p);
12.1187
12.1188 fun disj p q =
12.1189 - (if eqop eq_fma p T orelse eqop eq_fma q T then T
12.1190 - else (if eqop eq_fma p F then q
12.1191 - else (if eqop eq_fma q F then p else Or (p, q))));
12.1192 + (if eq_fm p T orelse eq_fm q T then T
12.1193 + else (if eq_fm p F then q else (if eq_fm q F then p else Or (p, q))));
12.1194
12.1195 fun minus_nat n m = IntInf.max (0, (IntInf.- (n, m)));
12.1196
12.1197 -fun decrnum (Bound n) = Bound (minus_nat n 1)
12.1198 +fun decrnum (Bound n) = Bound (minus_nat n (1 : IntInf.int))
12.1199 | decrnum (Neg a) = Neg (decrnum a)
12.1200 | decrnum (Add (a, b)) = Add (decrnum a, decrnum b)
12.1201 | decrnum (Sub (a, b)) = Sub (decrnum a, decrnum b)
12.1202 | decrnum (Mul (c, a)) = Mul (c, decrnum a)
12.1203 - | decrnum (Cn (n, i, a)) = Cn (minus_nat n 1, i, decrnum a)
12.1204 + | decrnum (Cn (n, i, a)) = Cn (minus_nat n (1 : IntInf.int), i, decrnum a)
12.1205 | decrnum (C u) = C u;
12.1206
12.1207 fun decr (Lt a) = Lt (decrnum a)
12.1208 @@ -596,20 +801,20 @@
12.1209 | decr (Closed aq) = Closed aq
12.1210 | decr (NClosed ar) = NClosed ar;
12.1211
12.1212 -fun concat [] = []
12.1213 - | concat (x :: xs) = append x (concat xs);
12.1214 -
12.1215 -fun split f (a, b) = f a b;
12.1216 +fun concat_map f [] = []
12.1217 + | concat_map f (x :: xs) = append (f x) (concat_map f xs);
12.1218
12.1219 fun numsubst0 t (C c) = C c
12.1220 - | numsubst0 t (Bound n) = (if eqop eq_nat n 0 then t else Bound n)
12.1221 + | numsubst0 t (Bound n) =
12.1222 + (if ((n : IntInf.int) = (0 : IntInf.int)) then t else Bound n)
12.1223 | numsubst0 t (Neg a) = Neg (numsubst0 t a)
12.1224 | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b)
12.1225 | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b)
12.1226 | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a)
12.1227 | numsubst0 t (Cn (v, i, a)) =
12.1228 - (if eqop eq_nat v 0 then Add (Mul (i, t), numsubst0 t a)
12.1229 - else Cn (suc (minus_nat v 1), i, numsubst0 t a));
12.1230 + (if ((v : IntInf.int) = (0 : IntInf.int))
12.1231 + then Add (Mul (i, t), numsubst0 t a)
12.1232 + else Cn (suc (minus_nat v (1 : IntInf.int)), i, numsubst0 t a));
12.1233
12.1234 fun subst0 t T = T
12.1235 | subst0 t F = F
12.1236 @@ -679,49 +884,417 @@
12.1237 | minusinf (Closed ap) = Closed ap
12.1238 | minusinf (NClosed aq) = NClosed aq
12.1239 | minusinf (Lt (Cn (cm, c, e))) =
12.1240 - (if eqop eq_nat cm 0 then T else Lt (Cn (suc (minus_nat cm 1), c, e)))
12.1241 + (if ((cm : IntInf.int) = (0 : IntInf.int)) then T
12.1242 + else Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e)))
12.1243 | minusinf (Le (Cn (dm, c, e))) =
12.1244 - (if eqop eq_nat dm 0 then T else Le (Cn (suc (minus_nat dm 1), c, e)))
12.1245 + (if ((dm : IntInf.int) = (0 : IntInf.int)) then T
12.1246 + else Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e)))
12.1247 | minusinf (Gt (Cn (em, c, e))) =
12.1248 - (if eqop eq_nat em 0 then F else Gt (Cn (suc (minus_nat em 1), c, e)))
12.1249 + (if ((em : IntInf.int) = (0 : IntInf.int)) then F
12.1250 + else Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e)))
12.1251 | minusinf (Ge (Cn (fm, c, e))) =
12.1252 - (if eqop eq_nat fm 0 then F else Ge (Cn (suc (minus_nat fm 1), c, e)))
12.1253 + (if ((fm : IntInf.int) = (0 : IntInf.int)) then F
12.1254 + else Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e)))
12.1255 | minusinf (Eq (Cn (gm, c, e))) =
12.1256 - (if eqop eq_nat gm 0 then F else Eq (Cn (suc (minus_nat gm 1), c, e)))
12.1257 + (if ((gm : IntInf.int) = (0 : IntInf.int)) then F
12.1258 + else Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e)))
12.1259 | minusinf (NEq (Cn (hm, c, e))) =
12.1260 - (if eqop eq_nat hm 0 then T else NEq (Cn (suc (minus_nat hm 1), c, e)));
12.1261 + (if ((hm : IntInf.int) = (0 : IntInf.int)) then T
12.1262 + else NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e)));
12.1263
12.1264 val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
12.1265
12.1266 +val zero_int : IntInf.int = (0 : IntInf.int);
12.1267 +
12.1268 +type 'a zero = {zero : 'a};
12.1269 +val zero = #zero : 'a zero -> 'a;
12.1270 +
12.1271 +val zero_inta = {zero = zero_int} : IntInf.int zero;
12.1272 +
12.1273 +type 'a times = {times : 'a -> 'a -> 'a};
12.1274 +val times = #times : 'a times -> 'a -> 'a -> 'a;
12.1275 +
12.1276 +type 'a no_zero_divisors =
12.1277 + {times_no_zero_divisors : 'a times, zero_no_zero_divisors : 'a zero};
12.1278 +val times_no_zero_divisors = #times_no_zero_divisors :
12.1279 + 'a no_zero_divisors -> 'a times;
12.1280 +val zero_no_zero_divisors = #zero_no_zero_divisors :
12.1281 + 'a no_zero_divisors -> 'a zero;
12.1282 +
12.1283 +val times_int = {times = (fn a => fn b => IntInf.* (a, b))} : IntInf.int times;
12.1284 +
12.1285 +val no_zero_divisors_int =
12.1286 + {times_no_zero_divisors = times_int, zero_no_zero_divisors = zero_inta} :
12.1287 + IntInf.int no_zero_divisors;
12.1288 +
12.1289 +type 'a one = {one : 'a};
12.1290 +val one = #one : 'a one -> 'a;
12.1291 +
12.1292 +type 'a zero_neq_one = {one_zero_neq_one : 'a one, zero_zero_neq_one : 'a zero};
12.1293 +val one_zero_neq_one = #one_zero_neq_one : 'a zero_neq_one -> 'a one;
12.1294 +val zero_zero_neq_one = #zero_zero_neq_one : 'a zero_neq_one -> 'a zero;
12.1295 +
12.1296 +type 'a semigroup_mult = {times_semigroup_mult : 'a times};
12.1297 +val times_semigroup_mult = #times_semigroup_mult :
12.1298 + 'a semigroup_mult -> 'a times;
12.1299 +
12.1300 +type 'a plus = {plus : 'a -> 'a -> 'a};
12.1301 +val plus = #plus : 'a plus -> 'a -> 'a -> 'a;
12.1302 +
12.1303 +type 'a semigroup_add = {plus_semigroup_add : 'a plus};
12.1304 +val plus_semigroup_add = #plus_semigroup_add : 'a semigroup_add -> 'a plus;
12.1305 +
12.1306 +type 'a ab_semigroup_add = {semigroup_add_ab_semigroup_add : 'a semigroup_add};
12.1307 +val semigroup_add_ab_semigroup_add = #semigroup_add_ab_semigroup_add :
12.1308 + 'a ab_semigroup_add -> 'a semigroup_add;
12.1309 +
12.1310 +type 'a semiring =
12.1311 + {ab_semigroup_add_semiring : 'a ab_semigroup_add,
12.1312 + semigroup_mult_semiring : 'a semigroup_mult};
12.1313 +val ab_semigroup_add_semiring = #ab_semigroup_add_semiring :
12.1314 + 'a semiring -> 'a ab_semigroup_add;
12.1315 +val semigroup_mult_semiring = #semigroup_mult_semiring :
12.1316 + 'a semiring -> 'a semigroup_mult;
12.1317 +
12.1318 +type 'a mult_zero = {times_mult_zero : 'a times, zero_mult_zero : 'a zero};
12.1319 +val times_mult_zero = #times_mult_zero : 'a mult_zero -> 'a times;
12.1320 +val zero_mult_zero = #zero_mult_zero : 'a mult_zero -> 'a zero;
12.1321 +
12.1322 +type 'a monoid_add =
12.1323 + {semigroup_add_monoid_add : 'a semigroup_add, zero_monoid_add : 'a zero};
12.1324 +val semigroup_add_monoid_add = #semigroup_add_monoid_add :
12.1325 + 'a monoid_add -> 'a semigroup_add;
12.1326 +val zero_monoid_add = #zero_monoid_add : 'a monoid_add -> 'a zero;
12.1327 +
12.1328 +type 'a comm_monoid_add =
12.1329 + {ab_semigroup_add_comm_monoid_add : 'a ab_semigroup_add,
12.1330 + monoid_add_comm_monoid_add : 'a monoid_add};
12.1331 +val ab_semigroup_add_comm_monoid_add = #ab_semigroup_add_comm_monoid_add :
12.1332 + 'a comm_monoid_add -> 'a ab_semigroup_add;
12.1333 +val monoid_add_comm_monoid_add = #monoid_add_comm_monoid_add :
12.1334 + 'a comm_monoid_add -> 'a monoid_add;
12.1335 +
12.1336 +type 'a semiring_0 =
12.1337 + {comm_monoid_add_semiring_0 : 'a comm_monoid_add,
12.1338 + mult_zero_semiring_0 : 'a mult_zero, semiring_semiring_0 : 'a semiring};
12.1339 +val comm_monoid_add_semiring_0 = #comm_monoid_add_semiring_0 :
12.1340 + 'a semiring_0 -> 'a comm_monoid_add;
12.1341 +val mult_zero_semiring_0 = #mult_zero_semiring_0 :
12.1342 + 'a semiring_0 -> 'a mult_zero;
12.1343 +val semiring_semiring_0 = #semiring_semiring_0 : 'a semiring_0 -> 'a semiring;
12.1344 +
12.1345 +type 'a power = {one_power : 'a one, times_power : 'a times};
12.1346 +val one_power = #one_power : 'a power -> 'a one;
12.1347 +val times_power = #times_power : 'a power -> 'a times;
12.1348 +
12.1349 +type 'a monoid_mult =
12.1350 + {semigroup_mult_monoid_mult : 'a semigroup_mult,
12.1351 + power_monoid_mult : 'a power};
12.1352 +val semigroup_mult_monoid_mult = #semigroup_mult_monoid_mult :
12.1353 + 'a monoid_mult -> 'a semigroup_mult;
12.1354 +val power_monoid_mult = #power_monoid_mult : 'a monoid_mult -> 'a power;
12.1355 +
12.1356 +type 'a semiring_1 =
12.1357 + {monoid_mult_semiring_1 : 'a monoid_mult,
12.1358 + semiring_0_semiring_1 : 'a semiring_0,
12.1359 + zero_neq_one_semiring_1 : 'a zero_neq_one};
12.1360 +val monoid_mult_semiring_1 = #monoid_mult_semiring_1 :
12.1361 + 'a semiring_1 -> 'a monoid_mult;
12.1362 +val semiring_0_semiring_1 = #semiring_0_semiring_1 :
12.1363 + 'a semiring_1 -> 'a semiring_0;
12.1364 +val zero_neq_one_semiring_1 = #zero_neq_one_semiring_1 :
12.1365 + 'a semiring_1 -> 'a zero_neq_one;
12.1366 +
12.1367 +type 'a cancel_semigroup_add =
12.1368 + {semigroup_add_cancel_semigroup_add : 'a semigroup_add};
12.1369 +val semigroup_add_cancel_semigroup_add = #semigroup_add_cancel_semigroup_add :
12.1370 + 'a cancel_semigroup_add -> 'a semigroup_add;
12.1371 +
12.1372 +type 'a cancel_ab_semigroup_add =
12.1373 + {ab_semigroup_add_cancel_ab_semigroup_add : 'a ab_semigroup_add,
12.1374 + cancel_semigroup_add_cancel_ab_semigroup_add : 'a cancel_semigroup_add};
12.1375 +val ab_semigroup_add_cancel_ab_semigroup_add =
12.1376 + #ab_semigroup_add_cancel_ab_semigroup_add :
12.1377 + 'a cancel_ab_semigroup_add -> 'a ab_semigroup_add;
12.1378 +val cancel_semigroup_add_cancel_ab_semigroup_add =
12.1379 + #cancel_semigroup_add_cancel_ab_semigroup_add :
12.1380 + 'a cancel_ab_semigroup_add -> 'a cancel_semigroup_add;
12.1381 +
12.1382 +type 'a cancel_comm_monoid_add =
12.1383 + {cancel_ab_semigroup_add_cancel_comm_monoid_add : 'a cancel_ab_semigroup_add,
12.1384 + comm_monoid_add_cancel_comm_monoid_add : 'a comm_monoid_add};
12.1385 +val cancel_ab_semigroup_add_cancel_comm_monoid_add =
12.1386 + #cancel_ab_semigroup_add_cancel_comm_monoid_add :
12.1387 + 'a cancel_comm_monoid_add -> 'a cancel_ab_semigroup_add;
12.1388 +val comm_monoid_add_cancel_comm_monoid_add =
12.1389 + #comm_monoid_add_cancel_comm_monoid_add :
12.1390 + 'a cancel_comm_monoid_add -> 'a comm_monoid_add;
12.1391 +
12.1392 +type 'a semiring_0_cancel =
12.1393 + {cancel_comm_monoid_add_semiring_0_cancel : 'a cancel_comm_monoid_add,
12.1394 + semiring_0_semiring_0_cancel : 'a semiring_0};
12.1395 +val cancel_comm_monoid_add_semiring_0_cancel =
12.1396 + #cancel_comm_monoid_add_semiring_0_cancel :
12.1397 + 'a semiring_0_cancel -> 'a cancel_comm_monoid_add;
12.1398 +val semiring_0_semiring_0_cancel = #semiring_0_semiring_0_cancel :
12.1399 + 'a semiring_0_cancel -> 'a semiring_0;
12.1400 +
12.1401 +type 'a semiring_1_cancel =
12.1402 + {semiring_0_cancel_semiring_1_cancel : 'a semiring_0_cancel,
12.1403 + semiring_1_semiring_1_cancel : 'a semiring_1};
12.1404 +val semiring_0_cancel_semiring_1_cancel = #semiring_0_cancel_semiring_1_cancel :
12.1405 + 'a semiring_1_cancel -> 'a semiring_0_cancel;
12.1406 +val semiring_1_semiring_1_cancel = #semiring_1_semiring_1_cancel :
12.1407 + 'a semiring_1_cancel -> 'a semiring_1;
12.1408 +
12.1409 +type 'a dvd = {times_dvd : 'a times};
12.1410 +val times_dvd = #times_dvd : 'a dvd -> 'a times;
12.1411 +
12.1412 +type 'a ab_semigroup_mult =
12.1413 + {semigroup_mult_ab_semigroup_mult : 'a semigroup_mult};
12.1414 +val semigroup_mult_ab_semigroup_mult = #semigroup_mult_ab_semigroup_mult :
12.1415 + 'a ab_semigroup_mult -> 'a semigroup_mult;
12.1416 +
12.1417 +type 'a comm_semiring =
12.1418 + {ab_semigroup_mult_comm_semiring : 'a ab_semigroup_mult,
12.1419 + semiring_comm_semiring : 'a semiring};
12.1420 +val ab_semigroup_mult_comm_semiring = #ab_semigroup_mult_comm_semiring :
12.1421 + 'a comm_semiring -> 'a ab_semigroup_mult;
12.1422 +val semiring_comm_semiring = #semiring_comm_semiring :
12.1423 + 'a comm_semiring -> 'a semiring;
12.1424 +
12.1425 +type 'a comm_semiring_0 =
12.1426 + {comm_semiring_comm_semiring_0 : 'a comm_semiring,
12.1427 + semiring_0_comm_semiring_0 : 'a semiring_0};
12.1428 +val comm_semiring_comm_semiring_0 = #comm_semiring_comm_semiring_0 :
12.1429 + 'a comm_semiring_0 -> 'a comm_semiring;
12.1430 +val semiring_0_comm_semiring_0 = #semiring_0_comm_semiring_0 :
12.1431 + 'a comm_semiring_0 -> 'a semiring_0;
12.1432 +
12.1433 +type 'a comm_monoid_mult =
12.1434 + {ab_semigroup_mult_comm_monoid_mult : 'a ab_semigroup_mult,
12.1435 + monoid_mult_comm_monoid_mult : 'a monoid_mult};
12.1436 +val ab_semigroup_mult_comm_monoid_mult = #ab_semigroup_mult_comm_monoid_mult :
12.1437 + 'a comm_monoid_mult -> 'a ab_semigroup_mult;
12.1438 +val monoid_mult_comm_monoid_mult = #monoid_mult_comm_monoid_mult :
12.1439 + 'a comm_monoid_mult -> 'a monoid_mult;
12.1440 +
12.1441 +type 'a comm_semiring_1 =
12.1442 + {comm_monoid_mult_comm_semiring_1 : 'a comm_monoid_mult,
12.1443 + comm_semiring_0_comm_semiring_1 : 'a comm_semiring_0,
12.1444 + dvd_comm_semiring_1 : 'a dvd, semiring_1_comm_semiring_1 : 'a semiring_1};
12.1445 +val comm_monoid_mult_comm_semiring_1 = #comm_monoid_mult_comm_semiring_1 :
12.1446 + 'a comm_semiring_1 -> 'a comm_monoid_mult;
12.1447 +val comm_semiring_0_comm_semiring_1 = #comm_semiring_0_comm_semiring_1 :
12.1448 + 'a comm_semiring_1 -> 'a comm_semiring_0;
12.1449 +val dvd_comm_semiring_1 = #dvd_comm_semiring_1 : 'a comm_semiring_1 -> 'a dvd;
12.1450 +val semiring_1_comm_semiring_1 = #semiring_1_comm_semiring_1 :
12.1451 + 'a comm_semiring_1 -> 'a semiring_1;
12.1452 +
12.1453 +type 'a comm_semiring_0_cancel =
12.1454 + {comm_semiring_0_comm_semiring_0_cancel : 'a comm_semiring_0,
12.1455 + semiring_0_cancel_comm_semiring_0_cancel : 'a semiring_0_cancel};
12.1456 +val comm_semiring_0_comm_semiring_0_cancel =
12.1457 + #comm_semiring_0_comm_semiring_0_cancel :
12.1458 + 'a comm_semiring_0_cancel -> 'a comm_semiring_0;
12.1459 +val semiring_0_cancel_comm_semiring_0_cancel =
12.1460 + #semiring_0_cancel_comm_semiring_0_cancel :
12.1461 + 'a comm_semiring_0_cancel -> 'a semiring_0_cancel;
12.1462 +
12.1463 +type 'a comm_semiring_1_cancel =
12.1464 + {comm_semiring_0_cancel_comm_semiring_1_cancel : 'a comm_semiring_0_cancel,
12.1465 + comm_semiring_1_comm_semiring_1_cancel : 'a comm_semiring_1,
12.1466 + semiring_1_cancel_comm_semiring_1_cancel : 'a semiring_1_cancel};
12.1467 +val comm_semiring_0_cancel_comm_semiring_1_cancel =
12.1468 + #comm_semiring_0_cancel_comm_semiring_1_cancel :
12.1469 + 'a comm_semiring_1_cancel -> 'a comm_semiring_0_cancel;
12.1470 +val comm_semiring_1_comm_semiring_1_cancel =
12.1471 + #comm_semiring_1_comm_semiring_1_cancel :
12.1472 + 'a comm_semiring_1_cancel -> 'a comm_semiring_1;
12.1473 +val semiring_1_cancel_comm_semiring_1_cancel =
12.1474 + #semiring_1_cancel_comm_semiring_1_cancel :
12.1475 + 'a comm_semiring_1_cancel -> 'a semiring_1_cancel;
12.1476 +
12.1477 +type 'a diva = {dvd_div : 'a dvd, diva : 'a -> 'a -> 'a, moda : 'a -> 'a -> 'a};
12.1478 +val dvd_div = #dvd_div : 'a diva -> 'a dvd;
12.1479 +val diva = #diva : 'a diva -> 'a -> 'a -> 'a;
12.1480 +val moda = #moda : 'a diva -> 'a -> 'a -> 'a;
12.1481 +
12.1482 +type 'a semiring_div =
12.1483 + {div_semiring_div : 'a diva,
12.1484 + comm_semiring_1_cancel_semiring_div : 'a comm_semiring_1_cancel,
12.1485 + no_zero_divisors_semiring_div : 'a no_zero_divisors};
12.1486 +val div_semiring_div = #div_semiring_div : 'a semiring_div -> 'a diva;
12.1487 +val comm_semiring_1_cancel_semiring_div = #comm_semiring_1_cancel_semiring_div :
12.1488 + 'a semiring_div -> 'a comm_semiring_1_cancel;
12.1489 +val no_zero_divisors_semiring_div = #no_zero_divisors_semiring_div :
12.1490 + 'a semiring_div -> 'a no_zero_divisors;
12.1491 +
12.1492 +val one_int : IntInf.int = (1 : IntInf.int);
12.1493 +
12.1494 +val one_inta = {one = one_int} : IntInf.int one;
12.1495 +
12.1496 +val zero_neq_one_int =
12.1497 + {one_zero_neq_one = one_inta, zero_zero_neq_one = zero_inta} :
12.1498 + IntInf.int zero_neq_one;
12.1499 +
12.1500 +val semigroup_mult_int = {times_semigroup_mult = times_int} :
12.1501 + IntInf.int semigroup_mult;
12.1502 +
12.1503 +val plus_int = {plus = (fn a => fn b => IntInf.+ (a, b))} : IntInf.int plus;
12.1504 +
12.1505 +val semigroup_add_int = {plus_semigroup_add = plus_int} :
12.1506 + IntInf.int semigroup_add;
12.1507 +
12.1508 +val ab_semigroup_add_int = {semigroup_add_ab_semigroup_add = semigroup_add_int}
12.1509 + : IntInf.int ab_semigroup_add;
12.1510 +
12.1511 +val semiring_int =
12.1512 + {ab_semigroup_add_semiring = ab_semigroup_add_int,
12.1513 + semigroup_mult_semiring = semigroup_mult_int}
12.1514 + : IntInf.int semiring;
12.1515 +
12.1516 +val mult_zero_int = {times_mult_zero = times_int, zero_mult_zero = zero_inta} :
12.1517 + IntInf.int mult_zero;
12.1518 +
12.1519 +val monoid_add_int =
12.1520 + {semigroup_add_monoid_add = semigroup_add_int, zero_monoid_add = zero_inta} :
12.1521 + IntInf.int monoid_add;
12.1522 +
12.1523 +val comm_monoid_add_int =
12.1524 + {ab_semigroup_add_comm_monoid_add = ab_semigroup_add_int,
12.1525 + monoid_add_comm_monoid_add = monoid_add_int}
12.1526 + : IntInf.int comm_monoid_add;
12.1527 +
12.1528 +val semiring_0_int =
12.1529 + {comm_monoid_add_semiring_0 = comm_monoid_add_int,
12.1530 + mult_zero_semiring_0 = mult_zero_int, semiring_semiring_0 = semiring_int}
12.1531 + : IntInf.int semiring_0;
12.1532 +
12.1533 +val power_int = {one_power = one_inta, times_power = times_int} :
12.1534 + IntInf.int power;
12.1535 +
12.1536 +val monoid_mult_int =
12.1537 + {semigroup_mult_monoid_mult = semigroup_mult_int,
12.1538 + power_monoid_mult = power_int}
12.1539 + : IntInf.int monoid_mult;
12.1540 +
12.1541 +val semiring_1_int =
12.1542 + {monoid_mult_semiring_1 = monoid_mult_int,
12.1543 + semiring_0_semiring_1 = semiring_0_int,
12.1544 + zero_neq_one_semiring_1 = zero_neq_one_int}
12.1545 + : IntInf.int semiring_1;
12.1546 +
12.1547 +val cancel_semigroup_add_int =
12.1548 + {semigroup_add_cancel_semigroup_add = semigroup_add_int} :
12.1549 + IntInf.int cancel_semigroup_add;
12.1550 +
12.1551 +val cancel_ab_semigroup_add_int =
12.1552 + {ab_semigroup_add_cancel_ab_semigroup_add = ab_semigroup_add_int,
12.1553 + cancel_semigroup_add_cancel_ab_semigroup_add = cancel_semigroup_add_int}
12.1554 + : IntInf.int cancel_ab_semigroup_add;
12.1555 +
12.1556 +val cancel_comm_monoid_add_int =
12.1557 + {cancel_ab_semigroup_add_cancel_comm_monoid_add = cancel_ab_semigroup_add_int,
12.1558 + comm_monoid_add_cancel_comm_monoid_add = comm_monoid_add_int}
12.1559 + : IntInf.int cancel_comm_monoid_add;
12.1560 +
12.1561 +val semiring_0_cancel_int =
12.1562 + {cancel_comm_monoid_add_semiring_0_cancel = cancel_comm_monoid_add_int,
12.1563 + semiring_0_semiring_0_cancel = semiring_0_int}
12.1564 + : IntInf.int semiring_0_cancel;
12.1565 +
12.1566 +val semiring_1_cancel_int =
12.1567 + {semiring_0_cancel_semiring_1_cancel = semiring_0_cancel_int,
12.1568 + semiring_1_semiring_1_cancel = semiring_1_int}
12.1569 + : IntInf.int semiring_1_cancel;
12.1570 +
12.1571 +val dvd_int = {times_dvd = times_int} : IntInf.int dvd;
12.1572 +
12.1573 +val ab_semigroup_mult_int =
12.1574 + {semigroup_mult_ab_semigroup_mult = semigroup_mult_int} :
12.1575 + IntInf.int ab_semigroup_mult;
12.1576 +
12.1577 +val comm_semiring_int =
12.1578 + {ab_semigroup_mult_comm_semiring = ab_semigroup_mult_int,
12.1579 + semiring_comm_semiring = semiring_int}
12.1580 + : IntInf.int comm_semiring;
12.1581 +
12.1582 +val comm_semiring_0_int =
12.1583 + {comm_semiring_comm_semiring_0 = comm_semiring_int,
12.1584 + semiring_0_comm_semiring_0 = semiring_0_int}
12.1585 + : IntInf.int comm_semiring_0;
12.1586 +
12.1587 +val comm_monoid_mult_int =
12.1588 + {ab_semigroup_mult_comm_monoid_mult = ab_semigroup_mult_int,
12.1589 + monoid_mult_comm_monoid_mult = monoid_mult_int}
12.1590 + : IntInf.int comm_monoid_mult;
12.1591 +
12.1592 +val comm_semiring_1_int =
12.1593 + {comm_monoid_mult_comm_semiring_1 = comm_monoid_mult_int,
12.1594 + comm_semiring_0_comm_semiring_1 = comm_semiring_0_int,
12.1595 + dvd_comm_semiring_1 = dvd_int, semiring_1_comm_semiring_1 = semiring_1_int}
12.1596 + : IntInf.int comm_semiring_1;
12.1597 +
12.1598 +val comm_semiring_0_cancel_int =
12.1599 + {comm_semiring_0_comm_semiring_0_cancel = comm_semiring_0_int,
12.1600 + semiring_0_cancel_comm_semiring_0_cancel = semiring_0_cancel_int}
12.1601 + : IntInf.int comm_semiring_0_cancel;
12.1602 +
12.1603 +val comm_semiring_1_cancel_int =
12.1604 + {comm_semiring_0_cancel_comm_semiring_1_cancel = comm_semiring_0_cancel_int,
12.1605 + comm_semiring_1_comm_semiring_1_cancel = comm_semiring_1_int,
12.1606 + semiring_1_cancel_comm_semiring_1_cancel = semiring_1_cancel_int}
12.1607 + : IntInf.int comm_semiring_1_cancel;
12.1608 +
12.1609 +fun abs_int i = (if IntInf.< (i, (0 : IntInf.int)) then IntInf.~ i else i);
12.1610 +
12.1611 +fun split f (a, b) = f a b;
12.1612 +
12.1613 fun sgn_int i =
12.1614 - (if eqop eq_int i (0 : IntInf.int) then (0 : IntInf.int)
12.1615 + (if ((i : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int)
12.1616 else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int)
12.1617 else IntInf.~ (1 : IntInf.int)));
12.1618
12.1619 fun apsnd f (x, y) = (x, f y);
12.1620
12.1621 -fun divmoda k l =
12.1622 - (if eqop eq_int k (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
12.1623 - else (if eqop eq_int l (0 : IntInf.int) then ((0 : IntInf.int), k)
12.1624 +fun divmod_int k l =
12.1625 + (if ((k : IntInf.int) = (0 : IntInf.int))
12.1626 + then ((0 : IntInf.int), (0 : IntInf.int))
12.1627 + else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k)
12.1628 else apsnd (fn a => IntInf.* (sgn_int l, a))
12.1629 - (if eqop eq_int (sgn_int k) (sgn_int l)
12.1630 - then (fn k => fn l => IntInf.divMod (IntInf.abs k,
12.1631 - IntInf.abs l))
12.1632 - k l
12.1633 + (if (((sgn_int k) : IntInf.int) = (sgn_int l))
12.1634 + then IntInf.divMod (IntInf.abs k, IntInf.abs l)
12.1635 else let
12.1636 - val a =
12.1637 - (fn k => fn l => IntInf.divMod (IntInf.abs k,
12.1638 - IntInf.abs l))
12.1639 - k l;
12.1640 - val (r, s) = a;
12.1641 + val (r, s) =
12.1642 + IntInf.divMod (IntInf.abs k, IntInf.abs l);
12.1643 in
12.1644 - (if eqop eq_int s (0 : IntInf.int)
12.1645 + (if ((s : IntInf.int) = (0 : IntInf.int))
12.1646 then (IntInf.~ r, (0 : IntInf.int))
12.1647 else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
12.1648 IntInf.- (abs_int l, s)))
12.1649 end)));
12.1650
12.1651 -fun mod_int a b = snd (divmoda a b);
12.1652 +fun snd (a, b) = b;
12.1653 +
12.1654 +fun mod_int a b = snd (divmod_int a b);
12.1655 +
12.1656 +fun fst (a, b) = a;
12.1657 +
12.1658 +fun div_int a b = fst (divmod_int a b);
12.1659 +
12.1660 +val div_inta = {dvd_div = dvd_int, diva = div_int, moda = mod_int} :
12.1661 + IntInf.int diva;
12.1662 +
12.1663 +val semiring_div_int =
12.1664 + {div_semiring_div = div_inta,
12.1665 + comm_semiring_1_cancel_semiring_div = comm_semiring_1_cancel_int,
12.1666 + no_zero_divisors_semiring_div = no_zero_divisors_int}
12.1667 + : IntInf.int semiring_div;
12.1668 +
12.1669 +fun dvd (A1_, A2_) a b =
12.1670 + eqa A2_ (moda (div_semiring_div A1_) b a)
12.1671 + (zero ((zero_no_zero_divisors o no_zero_divisors_semiring_div) A1_));
12.1672
12.1673 fun num_case f1 f2 f3 f4 f5 f6 f7 (Mul (inta, num)) = f7 inta num
12.1674 | num_case f1 f2 f3 f4 f5 f6 f7 (Sub (num1, num2)) = f6 num1 num2
12.1675 @@ -742,11 +1315,11 @@
12.1676 fun numneg t = nummul (IntInf.~ (1 : IntInf.int)) t;
12.1677
12.1678 fun numadd (Cn (n1, c1, r1), Cn (n2, c2, r2)) =
12.1679 - (if eqop eq_nat n1 n2
12.1680 + (if ((n1 : IntInf.int) = n2)
12.1681 then let
12.1682 val c = IntInf.+ (c1, c2);
12.1683 in
12.1684 - (if eqop eq_int c (0 : IntInf.int) then numadd (r1, r2)
12.1685 + (if ((c : IntInf.int) = (0 : IntInf.int)) then numadd (r1, r2)
12.1686 else Cn (n1, c, numadd (r1, r2)))
12.1687 end
12.1688 else (if IntInf.<= (n1, n2)
12.1689 @@ -807,10 +1380,8 @@
12.1690 | numadd (Mul (at, au), Sub (hp, hq)) = Add (Mul (at, au), Sub (hp, hq))
12.1691 | numadd (Mul (at, au), Mul (hr, hs)) = Add (Mul (at, au), Mul (hr, hs));
12.1692
12.1693 -val eq_numa = {eq = eq_num} : num eq;
12.1694 -
12.1695 fun numsub s t =
12.1696 - (if eqop eq_numa s t then C (0 : IntInf.int) else numadd (s, numneg t));
12.1697 + (if eq_num s t then C (0 : IntInf.int) else numadd (s, numneg t));
12.1698
12.1699 fun simpnum (C j) = C j
12.1700 | simpnum (Bound n) = Cn (n, (1 : IntInf.int), C (0 : IntInf.int))
12.1701 @@ -818,7 +1389,7 @@
12.1702 | simpnum (Add (t, s)) = numadd (simpnum t, simpnum s)
12.1703 | simpnum (Sub (t, s)) = numsub (simpnum t) (simpnum s)
12.1704 | simpnum (Mul (i, t)) =
12.1705 - (if eqop eq_int i (0 : IntInf.int) then C (0 : IntInf.int)
12.1706 + (if ((i : IntInf.int) = (0 : IntInf.int)) then C (0 : IntInf.int)
12.1707 else nummul i (simpnum t))
12.1708 | simpnum (Cn (v, va, vb)) = Cn (v, va, vb);
12.1709
12.1710 @@ -843,23 +1414,20 @@
12.1711 | nota (NClosed v) = Not (NClosed v);
12.1712
12.1713 fun iffa p q =
12.1714 - (if eqop eq_fma p q then T
12.1715 - else (if eqop eq_fma p (nota q) orelse eqop eq_fma (nota p) q then F
12.1716 - else (if eqop eq_fma p F then nota q
12.1717 - else (if eqop eq_fma q F then nota p
12.1718 - else (if eqop eq_fma p T then q
12.1719 - else (if eqop eq_fma q T then p
12.1720 - else Iff (p, q)))))));
12.1721 + (if eq_fm p q then T
12.1722 + else (if eq_fm p (nota q) orelse eq_fm (nota p) q then F
12.1723 + else (if eq_fm p F then nota q
12.1724 + else (if eq_fm q F then nota p
12.1725 + else (if eq_fm p T then q
12.1726 + else (if eq_fm q T then p else Iff (p, q)))))));
12.1727
12.1728 fun impa p q =
12.1729 - (if eqop eq_fma p F orelse eqop eq_fma q T then T
12.1730 - else (if eqop eq_fma p T then q
12.1731 - else (if eqop eq_fma q F then nota p else Imp (p, q))));
12.1732 + (if eq_fm p F orelse eq_fm q T then T
12.1733 + else (if eq_fm p T then q else (if eq_fm q F then nota p else Imp (p, q))));
12.1734
12.1735 fun conj p q =
12.1736 - (if eqop eq_fma p F orelse eqop eq_fma q F then F
12.1737 - else (if eqop eq_fma p T then q
12.1738 - else (if eqop eq_fma q T then p else And (p, q))));
12.1739 + (if eq_fm p F orelse eq_fm q F then F
12.1740 + else (if eq_fm p T then q else (if eq_fm q T then p else And (p, q))));
12.1741
12.1742 fun simpfm (And (p, q)) = conj (simpfm p) (simpfm q)
12.1743 | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q)
12.1744 @@ -868,91 +1436,80 @@
12.1745 | simpfm (Not p) = nota (simpfm p)
12.1746 | simpfm (Lt a) =
12.1747 let
12.1748 - val a' = simpnum a;
12.1749 + val aa = simpnum a;
12.1750 in
12.1751 - (case a' of C v => (if IntInf.< (v, (0 : IntInf.int)) then T else F)
12.1752 - | Bound nat => Lt a' | Cn (nat, inta, num) => Lt a' | Neg num => Lt a'
12.1753 - | Add (num1, num2) => Lt a' | Sub (num1, num2) => Lt a'
12.1754 - | Mul (inta, num) => Lt a')
12.1755 + (case aa of C v => (if IntInf.< (v, (0 : IntInf.int)) then T else F)
12.1756 + | Bound _ => Lt aa | Cn (_, _, _) => Lt aa | Neg _ => Lt aa
12.1757 + | Add (_, _) => Lt aa | Sub (_, _) => Lt aa | Mul (_, _) => Lt aa)
12.1758 end
12.1759 | simpfm (Le a) =
12.1760 let
12.1761 - val a' = simpnum a;
12.1762 + val aa = simpnum a;
12.1763 in
12.1764 - (case a' of C v => (if IntInf.<= (v, (0 : IntInf.int)) then T else F)
12.1765 - | Bound nat => Le a' | Cn (nat, inta, num) => Le a' | Neg num => Le a'
12.1766 - | Add (num1, num2) => Le a' | Sub (num1, num2) => Le a'
12.1767 - | Mul (inta, num) => Le a')
12.1768 + (case aa of C v => (if IntInf.<= (v, (0 : IntInf.int)) then T else F)
12.1769 + | Bound _ => Le aa | Cn (_, _, _) => Le aa | Neg _ => Le aa
12.1770 + | Add (_, _) => Le aa | Sub (_, _) => Le aa | Mul (_, _) => Le aa)
12.1771 end
12.1772 | simpfm (Gt a) =
12.1773 let
12.1774 - val a' = simpnum a;
12.1775 + val aa = simpnum a;
12.1776 in
12.1777 - (case a' of C v => (if IntInf.< ((0 : IntInf.int), v) then T else F)
12.1778 - | Bound nat => Gt a' | Cn (nat, inta, num) => Gt a' | Neg num => Gt a'
12.1779 - | Add (num1, num2) => Gt a' | Sub (num1, num2) => Gt a'
12.1780 - | Mul (inta, num) => Gt a')
12.1781 + (case aa of C v => (if IntInf.< ((0 : IntInf.int), v) then T else F)
12.1782 + | Bound _ => Gt aa | Cn (_, _, _) => Gt aa | Neg _ => Gt aa
12.1783 + | Add (_, _) => Gt aa | Sub (_, _) => Gt aa | Mul (_, _) => Gt aa)
12.1784 end
12.1785 | simpfm (Ge a) =
12.1786 let
12.1787 - val a' = simpnum a;
12.1788 + val aa = simpnum a;
12.1789 in
12.1790 - (case a' of C v => (if IntInf.<= ((0 : IntInf.int), v) then T else F)
12.1791 - | Bound nat => Ge a' | Cn (nat, inta, num) => Ge a' | Neg num => Ge a'
12.1792 - | Add (num1, num2) => Ge a' | Sub (num1, num2) => Ge a'
12.1793 - | Mul (inta, num) => Ge a')
12.1794 + (case aa of C v => (if IntInf.<= ((0 : IntInf.int), v) then T else F)
12.1795 + | Bound _ => Ge aa | Cn (_, _, _) => Ge aa | Neg _ => Ge aa
12.1796 + | Add (_, _) => Ge aa | Sub (_, _) => Ge aa | Mul (_, _) => Ge aa)
12.1797 end
12.1798 | simpfm (Eq a) =
12.1799 let
12.1800 - val a' = simpnum a;
12.1801 + val aa = simpnum a;
12.1802 in
12.1803 - (case a' of C v => (if eqop eq_int v (0 : IntInf.int) then T else F)
12.1804 - | Bound nat => Eq a' | Cn (nat, inta, num) => Eq a' | Neg num => Eq a'
12.1805 - | Add (num1, num2) => Eq a' | Sub (num1, num2) => Eq a'
12.1806 - | Mul (inta, num) => Eq a')
12.1807 + (case aa
12.1808 + of C v => (if ((v : IntInf.int) = (0 : IntInf.int)) then T else F)
12.1809 + | Bound _ => Eq aa | Cn (_, _, _) => Eq aa | Neg _ => Eq aa
12.1810 + | Add (_, _) => Eq aa | Sub (_, _) => Eq aa | Mul (_, _) => Eq aa)
12.1811 end
12.1812 | simpfm (NEq a) =
12.1813 let
12.1814 - val a' = simpnum a;
12.1815 + val aa = simpnum a;
12.1816 in
12.1817 - (case a' of C v => (if not (eqop eq_int v (0 : IntInf.int)) then T else F)
12.1818 - | Bound nat => NEq a' | Cn (nat, inta, num) => NEq a'
12.1819 - | Neg num => NEq a' | Add (num1, num2) => NEq a'
12.1820 - | Sub (num1, num2) => NEq a' | Mul (inta, num) => NEq a')
12.1821 + (case aa
12.1822 + of C v => (if not ((v : IntInf.int) = (0 : IntInf.int)) then T else F)
12.1823 + | Bound _ => NEq aa | Cn (_, _, _) => NEq aa | Neg _ => NEq aa
12.1824 + | Add (_, _) => NEq aa | Sub (_, _) => NEq aa | Mul (_, _) => NEq aa)
12.1825 end
12.1826 | simpfm (Dvd (i, a)) =
12.1827 - (if eqop eq_int i (0 : IntInf.int) then simpfm (Eq a)
12.1828 - else (if eqop eq_int (abs_int i) (1 : IntInf.int) then T
12.1829 + (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (Eq a)
12.1830 + else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then T
12.1831 else let
12.1832 - val a' = simpnum a;
12.1833 + val aa = simpnum a;
12.1834 in
12.1835 - (case a'
12.1836 - of C v =>
12.1837 - (if eqop eq_int (mod_int v i) (0 : IntInf.int) then T
12.1838 - else F)
12.1839 - | Bound nat => Dvd (i, a')
12.1840 - | Cn (nat, inta, num) => Dvd (i, a')
12.1841 - | Neg num => Dvd (i, a')
12.1842 - | Add (num1, num2) => Dvd (i, a')
12.1843 - | Sub (num1, num2) => Dvd (i, a')
12.1844 - | Mul (inta, num) => Dvd (i, a'))
12.1845 + (case aa
12.1846 + of C v =>
12.1847 + (if dvd (semiring_div_int, eq_int) i v then T else F)
12.1848 + | Bound _ => Dvd (i, aa) | Cn (_, _, _) => Dvd (i, aa)
12.1849 + | Neg _ => Dvd (i, aa) | Add (_, _) => Dvd (i, aa)
12.1850 + | Sub (_, _) => Dvd (i, aa) | Mul (_, _) => Dvd (i, aa))
12.1851 end))
12.1852 | simpfm (NDvd (i, a)) =
12.1853 - (if eqop eq_int i (0 : IntInf.int) then simpfm (NEq a)
12.1854 - else (if eqop eq_int (abs_int i) (1 : IntInf.int) then F
12.1855 + (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (NEq a)
12.1856 + else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then F
12.1857 else let
12.1858 - val a' = simpnum a;
12.1859 + val aa = simpnum a;
12.1860 in
12.1861 - (case a'
12.1862 - of C v =>
12.1863 - (if not (eqop eq_int (mod_int v i) (0 : IntInf.int))
12.1864 - then T else F)
12.1865 - | Bound nat => NDvd (i, a')
12.1866 - | Cn (nat, inta, num) => NDvd (i, a')
12.1867 - | Neg num => NDvd (i, a')
12.1868 - | Add (num1, num2) => NDvd (i, a')
12.1869 - | Sub (num1, num2) => NDvd (i, a')
12.1870 - | Mul (inta, num) => NDvd (i, a'))
12.1871 + (case aa
12.1872 + of C v =>
12.1873 + (if not (dvd (semiring_div_int, eq_int) i v) then T
12.1874 + else F)
12.1875 + | Bound _ => NDvd (i, aa) | Cn (_, _, _) => NDvd (i, aa)
12.1876 + | Neg _ => NDvd (i, aa) | Add (_, _) => NDvd (i, aa)
12.1877 + | Sub (_, _) => NDvd (i, aa) | Mul (_, _) => NDvd (i, aa))
12.1878 end))
12.1879 | simpfm T = T
12.1880 | simpfm F = F
12.1881 @@ -1025,32 +1582,40 @@
12.1882 | mirror (Closed ap) = Closed ap
12.1883 | mirror (NClosed aq) = NClosed aq
12.1884 | mirror (Lt (Cn (cm, c, e))) =
12.1885 - (if eqop eq_nat cm 0 then Gt (Cn (0, c, Neg e))
12.1886 - else Lt (Cn (suc (minus_nat cm 1), c, e)))
12.1887 + (if ((cm : IntInf.int) = (0 : IntInf.int))
12.1888 + then Gt (Cn ((0 : IntInf.int), c, Neg e))
12.1889 + else Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e)))
12.1890 | mirror (Le (Cn (dm, c, e))) =
12.1891 - (if eqop eq_nat dm 0 then Ge (Cn (0, c, Neg e))
12.1892 - else Le (Cn (suc (minus_nat dm 1), c, e)))
12.1893 + (if ((dm : IntInf.int) = (0 : IntInf.int))
12.1894 + then Ge (Cn ((0 : IntInf.int), c, Neg e))
12.1895 + else Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e)))
12.1896 | mirror (Gt (Cn (em, c, e))) =
12.1897 - (if eqop eq_nat em 0 then Lt (Cn (0, c, Neg e))
12.1898 - else Gt (Cn (suc (minus_nat em 1), c, e)))
12.1899 + (if ((em : IntInf.int) = (0 : IntInf.int))
12.1900 + then Lt (Cn ((0 : IntInf.int), c, Neg e))
12.1901 + else Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e)))
12.1902 | mirror (Ge (Cn (fm, c, e))) =
12.1903 - (if eqop eq_nat fm 0 then Le (Cn (0, c, Neg e))
12.1904 - else Ge (Cn (suc (minus_nat fm 1), c, e)))
12.1905 + (if ((fm : IntInf.int) = (0 : IntInf.int))
12.1906 + then Le (Cn ((0 : IntInf.int), c, Neg e))
12.1907 + else Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e)))
12.1908 | mirror (Eq (Cn (gm, c, e))) =
12.1909 - (if eqop eq_nat gm 0 then Eq (Cn (0, c, Neg e))
12.1910 - else Eq (Cn (suc (minus_nat gm 1), c, e)))
12.1911 + (if ((gm : IntInf.int) = (0 : IntInf.int))
12.1912 + then Eq (Cn ((0 : IntInf.int), c, Neg e))
12.1913 + else Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e)))
12.1914 | mirror (NEq (Cn (hm, c, e))) =
12.1915 - (if eqop eq_nat hm 0 then NEq (Cn (0, c, Neg e))
12.1916 - else NEq (Cn (suc (minus_nat hm 1), c, e)))
12.1917 + (if ((hm : IntInf.int) = (0 : IntInf.int))
12.1918 + then NEq (Cn ((0 : IntInf.int), c, Neg e))
12.1919 + else NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e)))
12.1920 | mirror (Dvd (i, Cn (im, c, e))) =
12.1921 - (if eqop eq_nat im 0 then Dvd (i, Cn (0, c, Neg e))
12.1922 - else Dvd (i, Cn (suc (minus_nat im 1), c, e)))
12.1923 + (if ((im : IntInf.int) = (0 : IntInf.int))
12.1924 + then Dvd (i, Cn ((0 : IntInf.int), c, Neg e))
12.1925 + else Dvd (i, Cn (suc (minus_nat im (1 : IntInf.int)), c, e)))
12.1926 | mirror (NDvd (i, Cn (jm, c, e))) =
12.1927 - (if eqop eq_nat jm 0 then NDvd (i, Cn (0, c, Neg e))
12.1928 - else NDvd (i, Cn (suc (minus_nat jm 1), c, e)));
12.1929 + (if ((jm : IntInf.int) = (0 : IntInf.int))
12.1930 + then NDvd (i, Cn ((0 : IntInf.int), c, Neg e))
12.1931 + else NDvd (i, Cn (suc (minus_nat jm (1 : IntInf.int)), c, e)));
12.1932
12.1933 -fun size_list [] = 0
12.1934 - | size_list (a :: lista) = IntInf.+ (size_list lista, suc 0);
12.1935 +fun size_list [] = (0 : IntInf.int)
12.1936 + | size_list (a :: lista) = IntInf.+ (size_list lista, suc (0 : IntInf.int));
12.1937
12.1938 fun alpha (And (p, q)) = append (alpha p) (alpha q)
12.1939 | alpha (Or (p, q)) = append (alpha p) (alpha q)
12.1940 @@ -1101,14 +1666,20 @@
12.1941 | alpha (A ao) = []
12.1942 | alpha (Closed ap) = []
12.1943 | alpha (NClosed aq) = []
12.1944 - | alpha (Lt (Cn (cm, c, e))) = (if eqop eq_nat cm 0 then [e] else [])
12.1945 + | alpha (Lt (Cn (cm, c, e))) =
12.1946 + (if ((cm : IntInf.int) = (0 : IntInf.int)) then [e] else [])
12.1947 | alpha (Le (Cn (dm, c, e))) =
12.1948 - (if eqop eq_nat dm 0 then [Add (C (~1 : IntInf.int), e)] else [])
12.1949 - | alpha (Gt (Cn (em, c, e))) = (if eqop eq_nat em 0 then [] else [])
12.1950 - | alpha (Ge (Cn (fm, c, e))) = (if eqop eq_nat fm 0 then [] else [])
12.1951 + (if ((dm : IntInf.int) = (0 : IntInf.int))
12.1952 + then [Add (C (~1 : IntInf.int), e)] else [])
12.1953 + | alpha (Gt (Cn (em, c, e))) =
12.1954 + (if ((em : IntInf.int) = (0 : IntInf.int)) then [] else [])
12.1955 + | alpha (Ge (Cn (fm, c, e))) =
12.1956 + (if ((fm : IntInf.int) = (0 : IntInf.int)) then [] else [])
12.1957 | alpha (Eq (Cn (gm, c, e))) =
12.1958 - (if eqop eq_nat gm 0 then [Add (C (~1 : IntInf.int), e)] else [])
12.1959 - | alpha (NEq (Cn (hm, c, e))) = (if eqop eq_nat hm 0 then [e] else []);
12.1960 + (if ((gm : IntInf.int) = (0 : IntInf.int))
12.1961 + then [Add (C (~1 : IntInf.int), e)] else [])
12.1962 + | alpha (NEq (Cn (hm, c, e))) =
12.1963 + (if ((hm : IntInf.int) = (0 : IntInf.int)) then [e] else []);
12.1964
12.1965 fun beta (And (p, q)) = append (beta p) (beta q)
12.1966 | beta (Or (p, q)) = append (beta p) (beta q)
12.1967 @@ -1159,24 +1730,39 @@
12.1968 | beta (A ao) = []
12.1969 | beta (Closed ap) = []
12.1970 | beta (NClosed aq) = []
12.1971 - | beta (Lt (Cn (cm, c, e))) = (if eqop eq_nat cm 0 then [] else [])
12.1972 - | beta (Le (Cn (dm, c, e))) = (if eqop eq_nat dm 0 then [] else [])
12.1973 - | beta (Gt (Cn (em, c, e))) = (if eqop eq_nat em 0 then [Neg e] else [])
12.1974 + | beta (Lt (Cn (cm, c, e))) =
12.1975 + (if ((cm : IntInf.int) = (0 : IntInf.int)) then [] else [])
12.1976 + | beta (Le (Cn (dm, c, e))) =
12.1977 + (if ((dm : IntInf.int) = (0 : IntInf.int)) then [] else [])
12.1978 + | beta (Gt (Cn (em, c, e))) =
12.1979 + (if ((em : IntInf.int) = (0 : IntInf.int)) then [Neg e] else [])
12.1980 | beta (Ge (Cn (fm, c, e))) =
12.1981 - (if eqop eq_nat fm 0 then [Sub (C (~1 : IntInf.int), e)] else [])
12.1982 + (if ((fm : IntInf.int) = (0 : IntInf.int))
12.1983 + then [Sub (C (~1 : IntInf.int), e)] else [])
12.1984 | beta (Eq (Cn (gm, c, e))) =
12.1985 - (if eqop eq_nat gm 0 then [Sub (C (~1 : IntInf.int), e)] else [])
12.1986 - | beta (NEq (Cn (hm, c, e))) = (if eqop eq_nat hm 0 then [Neg e] else []);
12.1987 + (if ((gm : IntInf.int) = (0 : IntInf.int))
12.1988 + then [Sub (C (~1 : IntInf.int), e)] else [])
12.1989 + | beta (NEq (Cn (hm, c, e))) =
12.1990 + (if ((hm : IntInf.int) = (0 : IntInf.int)) then [Neg e] else []);
12.1991 +
12.1992 +val eq_numa = {eq = eq_num} : num eq;
12.1993
12.1994 fun member A_ x [] = false
12.1995 - | member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;
12.1996 + | member A_ x (y :: ys) = eqa A_ x y orelse member A_ x ys;
12.1997
12.1998 fun remdups A_ [] = []
12.1999 | remdups A_ (x :: xs) =
12.2000 (if member A_ x xs then remdups A_ xs else x :: remdups A_ xs);
12.2001
12.2002 -fun delta (And (p, q)) = zlcm (delta p) (delta q)
12.2003 - | delta (Or (p, q)) = zlcm (delta p) (delta q)
12.2004 +fun gcd_int k l =
12.2005 + abs_int
12.2006 + (if ((l : IntInf.int) = (0 : IntInf.int)) then k
12.2007 + else gcd_int l (mod_int (abs_int k) (abs_int l)));
12.2008 +
12.2009 +fun lcm_int a b = div_int (IntInf.* (abs_int a, abs_int b)) (gcd_int a b);
12.2010 +
12.2011 +fun delta (And (p, q)) = lcm_int (delta p) (delta q)
12.2012 + | delta (Or (p, q)) = lcm_int (delta p) (delta q)
12.2013 | delta T = (1 : IntInf.int)
12.2014 | delta F = (1 : IntInf.int)
12.2015 | delta (Lt u) = (1 : IntInf.int)
12.2016 @@ -1205,110 +1791,117 @@
12.2017 | delta (Closed ap) = (1 : IntInf.int)
12.2018 | delta (NClosed aq) = (1 : IntInf.int)
12.2019 | delta (Dvd (i, Cn (cm, c, e))) =
12.2020 - (if eqop eq_nat cm 0 then i else (1 : IntInf.int))
12.2021 + (if ((cm : IntInf.int) = (0 : IntInf.int)) then i else (1 : IntInf.int))
12.2022 | delta (NDvd (i, Cn (dm, c, e))) =
12.2023 - (if eqop eq_nat dm 0 then i else (1 : IntInf.int));
12.2024 -
12.2025 -fun div_int a b = fst (divmoda a b);
12.2026 + (if ((dm : IntInf.int) = (0 : IntInf.int)) then i else (1 : IntInf.int));
12.2027
12.2028 fun a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k))
12.2029 | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k))
12.2030 - | a_beta T = (fn k => T)
12.2031 - | a_beta F = (fn k => F)
12.2032 - | a_beta (Lt (C bo)) = (fn k => Lt (C bo))
12.2033 - | a_beta (Lt (Bound bp)) = (fn k => Lt (Bound bp))
12.2034 - | a_beta (Lt (Neg bt)) = (fn k => Lt (Neg bt))
12.2035 - | a_beta (Lt (Add (bu, bv))) = (fn k => Lt (Add (bu, bv)))
12.2036 - | a_beta (Lt (Sub (bw, bx))) = (fn k => Lt (Sub (bw, bx)))
12.2037 - | a_beta (Lt (Mul (by, bz))) = (fn k => Lt (Mul (by, bz)))
12.2038 - | a_beta (Le (C co)) = (fn k => Le (C co))
12.2039 - | a_beta (Le (Bound cp)) = (fn k => Le (Bound cp))
12.2040 - | a_beta (Le (Neg ct)) = (fn k => Le (Neg ct))
12.2041 - | a_beta (Le (Add (cu, cv))) = (fn k => Le (Add (cu, cv)))
12.2042 - | a_beta (Le (Sub (cw, cx))) = (fn k => Le (Sub (cw, cx)))
12.2043 - | a_beta (Le (Mul (cy, cz))) = (fn k => Le (Mul (cy, cz)))
12.2044 - | a_beta (Gt (C doa)) = (fn k => Gt (C doa))
12.2045 - | a_beta (Gt (Bound dp)) = (fn k => Gt (Bound dp))
12.2046 - | a_beta (Gt (Neg dt)) = (fn k => Gt (Neg dt))
12.2047 - | a_beta (Gt (Add (du, dv))) = (fn k => Gt (Add (du, dv)))
12.2048 - | a_beta (Gt (Sub (dw, dx))) = (fn k => Gt (Sub (dw, dx)))
12.2049 - | a_beta (Gt (Mul (dy, dz))) = (fn k => Gt (Mul (dy, dz)))
12.2050 - | a_beta (Ge (C eo)) = (fn k => Ge (C eo))
12.2051 - | a_beta (Ge (Bound ep)) = (fn k => Ge (Bound ep))
12.2052 - | a_beta (Ge (Neg et)) = (fn k => Ge (Neg et))
12.2053 - | a_beta (Ge (Add (eu, ev))) = (fn k => Ge (Add (eu, ev)))
12.2054 - | a_beta (Ge (Sub (ew, ex))) = (fn k => Ge (Sub (ew, ex)))
12.2055 - | a_beta (Ge (Mul (ey, ez))) = (fn k => Ge (Mul (ey, ez)))
12.2056 - | a_beta (Eq (C fo)) = (fn k => Eq (C fo))
12.2057 - | a_beta (Eq (Bound fp)) = (fn k => Eq (Bound fp))
12.2058 - | a_beta (Eq (Neg ft)) = (fn k => Eq (Neg ft))
12.2059 - | a_beta (Eq (Add (fu, fv))) = (fn k => Eq (Add (fu, fv)))
12.2060 - | a_beta (Eq (Sub (fw, fx))) = (fn k => Eq (Sub (fw, fx)))
12.2061 - | a_beta (Eq (Mul (fy, fz))) = (fn k => Eq (Mul (fy, fz)))
12.2062 - | a_beta (NEq (C go)) = (fn k => NEq (C go))
12.2063 - | a_beta (NEq (Bound gp)) = (fn k => NEq (Bound gp))
12.2064 - | a_beta (NEq (Neg gt)) = (fn k => NEq (Neg gt))
12.2065 - | a_beta (NEq (Add (gu, gv))) = (fn k => NEq (Add (gu, gv)))
12.2066 - | a_beta (NEq (Sub (gw, gx))) = (fn k => NEq (Sub (gw, gx)))
12.2067 - | a_beta (NEq (Mul (gy, gz))) = (fn k => NEq (Mul (gy, gz)))
12.2068 - | a_beta (Dvd (aa, C ho)) = (fn k => Dvd (aa, C ho))
12.2069 - | a_beta (Dvd (aa, Bound hp)) = (fn k => Dvd (aa, Bound hp))
12.2070 - | a_beta (Dvd (aa, Neg ht)) = (fn k => Dvd (aa, Neg ht))
12.2071 - | a_beta (Dvd (aa, Add (hu, hv))) = (fn k => Dvd (aa, Add (hu, hv)))
12.2072 - | a_beta (Dvd (aa, Sub (hw, hx))) = (fn k => Dvd (aa, Sub (hw, hx)))
12.2073 - | a_beta (Dvd (aa, Mul (hy, hz))) = (fn k => Dvd (aa, Mul (hy, hz)))
12.2074 - | a_beta (NDvd (ac, C io)) = (fn k => NDvd (ac, C io))
12.2075 - | a_beta (NDvd (ac, Bound ip)) = (fn k => NDvd (ac, Bound ip))
12.2076 - | a_beta (NDvd (ac, Neg it)) = (fn k => NDvd (ac, Neg it))
12.2077 - | a_beta (NDvd (ac, Add (iu, iv))) = (fn k => NDvd (ac, Add (iu, iv)))
12.2078 - | a_beta (NDvd (ac, Sub (iw, ix))) = (fn k => NDvd (ac, Sub (iw, ix)))
12.2079 - | a_beta (NDvd (ac, Mul (iy, iz))) = (fn k => NDvd (ac, Mul (iy, iz)))
12.2080 - | a_beta (Not ae) = (fn k => Not ae)
12.2081 - | a_beta (Imp (aj, ak)) = (fn k => Imp (aj, ak))
12.2082 - | a_beta (Iff (al, am)) = (fn k => Iff (al, am))
12.2083 - | a_beta (E an) = (fn k => E an)
12.2084 - | a_beta (A ao) = (fn k => A ao)
12.2085 - | a_beta (Closed ap) = (fn k => Closed ap)
12.2086 - | a_beta (NClosed aq) = (fn k => NClosed aq)
12.2087 + | a_beta T = (fn _ => T)
12.2088 + | a_beta F = (fn _ => F)
12.2089 + | a_beta (Lt (C bo)) = (fn _ => Lt (C bo))
12.2090 + | a_beta (Lt (Bound bp)) = (fn _ => Lt (Bound bp))
12.2091 + | a_beta (Lt (Neg bt)) = (fn _ => Lt (Neg bt))
12.2092 + | a_beta (Lt (Add (bu, bv))) = (fn _ => Lt (Add (bu, bv)))
12.2093 + | a_beta (Lt (Sub (bw, bx))) = (fn _ => Lt (Sub (bw, bx)))
12.2094 + | a_beta (Lt (Mul (by, bz))) = (fn _ => Lt (Mul (by, bz)))
12.2095 + | a_beta (Le (C co)) = (fn _ => Le (C co))
12.2096 + | a_beta (Le (Bound cp)) = (fn _ => Le (Bound cp))
12.2097 + | a_beta (Le (Neg ct)) = (fn _ => Le (Neg ct))
12.2098 + | a_beta (Le (Add (cu, cv))) = (fn _ => Le (Add (cu, cv)))
12.2099 + | a_beta (Le (Sub (cw, cx))) = (fn _ => Le (Sub (cw, cx)))
12.2100 + | a_beta (Le (Mul (cy, cz))) = (fn _ => Le (Mul (cy, cz)))
12.2101 + | a_beta (Gt (C doa)) = (fn _ => Gt (C doa))
12.2102 + | a_beta (Gt (Bound dp)) = (fn _ => Gt (Bound dp))
12.2103 + | a_beta (Gt (Neg dt)) = (fn _ => Gt (Neg dt))
12.2104 + | a_beta (Gt (Add (du, dv))) = (fn _ => Gt (Add (du, dv)))
12.2105 + | a_beta (Gt (Sub (dw, dx))) = (fn _ => Gt (Sub (dw, dx)))
12.2106 + | a_beta (Gt (Mul (dy, dz))) = (fn _ => Gt (Mul (dy, dz)))
12.2107 + | a_beta (Ge (C eo)) = (fn _ => Ge (C eo))
12.2108 + | a_beta (Ge (Bound ep)) = (fn _ => Ge (Bound ep))
12.2109 + | a_beta (Ge (Neg et)) = (fn _ => Ge (Neg et))
12.2110 + | a_beta (Ge (Add (eu, ev))) = (fn _ => Ge (Add (eu, ev)))
12.2111 + | a_beta (Ge (Sub (ew, ex))) = (fn _ => Ge (Sub (ew, ex)))
12.2112 + | a_beta (Ge (Mul (ey, ez))) = (fn _ => Ge (Mul (ey, ez)))
12.2113 + | a_beta (Eq (C fo)) = (fn _ => Eq (C fo))
12.2114 + | a_beta (Eq (Bound fp)) = (fn _ => Eq (Bound fp))
12.2115 + | a_beta (Eq (Neg ft)) = (fn _ => Eq (Neg ft))
12.2116 + | a_beta (Eq (Add (fu, fv))) = (fn _ => Eq (Add (fu, fv)))
12.2117 + | a_beta (Eq (Sub (fw, fx))) = (fn _ => Eq (Sub (fw, fx)))
12.2118 + | a_beta (Eq (Mul (fy, fz))) = (fn _ => Eq (Mul (fy, fz)))
12.2119 + | a_beta (NEq (C go)) = (fn _ => NEq (C go))
12.2120 + | a_beta (NEq (Bound gp)) = (fn _ => NEq (Bound gp))
12.2121 + | a_beta (NEq (Neg gt)) = (fn _ => NEq (Neg gt))
12.2122 + | a_beta (NEq (Add (gu, gv))) = (fn _ => NEq (Add (gu, gv)))
12.2123 + | a_beta (NEq (Sub (gw, gx))) = (fn _ => NEq (Sub (gw, gx)))
12.2124 + | a_beta (NEq (Mul (gy, gz))) = (fn _ => NEq (Mul (gy, gz)))
12.2125 + | a_beta (Dvd (aa, C ho)) = (fn _ => Dvd (aa, C ho))
12.2126 + | a_beta (Dvd (aa, Bound hp)) = (fn _ => Dvd (aa, Bound hp))
12.2127 + | a_beta (Dvd (aa, Neg ht)) = (fn _ => Dvd (aa, Neg ht))
12.2128 + | a_beta (Dvd (aa, Add (hu, hv))) = (fn _ => Dvd (aa, Add (hu, hv)))
12.2129 + | a_beta (Dvd (aa, Sub (hw, hx))) = (fn _ => Dvd (aa, Sub (hw, hx)))
12.2130 + | a_beta (Dvd (aa, Mul (hy, hz))) = (fn _ => Dvd (aa, Mul (hy, hz)))
12.2131 + | a_beta (NDvd (ac, C io)) = (fn _ => NDvd (ac, C io))
12.2132 + | a_beta (NDvd (ac, Bound ip)) = (fn _ => NDvd (ac, Bound ip))
12.2133 + | a_beta (NDvd (ac, Neg it)) = (fn _ => NDvd (ac, Neg it))
12.2134 + | a_beta (NDvd (ac, Add (iu, iv))) = (fn _ => NDvd (ac, Add (iu, iv)))
12.2135 + | a_beta (NDvd (ac, Sub (iw, ix))) = (fn _ => NDvd (ac, Sub (iw, ix)))
12.2136 + | a_beta (NDvd (ac, Mul (iy, iz))) = (fn _ => NDvd (ac, Mul (iy, iz)))
12.2137 + | a_beta (Not ae) = (fn _ => Not ae)
12.2138 + | a_beta (Imp (aj, ak)) = (fn _ => Imp (aj, ak))
12.2139 + | a_beta (Iff (al, am)) = (fn _ => Iff (al, am))
12.2140 + | a_beta (E an) = (fn _ => E an)
12.2141 + | a_beta (A ao) = (fn _ => A ao)
12.2142 + | a_beta (Closed ap) = (fn _ => Closed ap)
12.2143 + | a_beta (NClosed aq) = (fn _ => NClosed aq)
12.2144 | a_beta (Lt (Cn (cm, c, e))) =
12.2145 - (if eqop eq_nat cm 0
12.2146 - then (fn k => Lt (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2147 - else (fn k => Lt (Cn (suc (minus_nat cm 1), c, e))))
12.2148 + (if ((cm : IntInf.int) = (0 : IntInf.int))
12.2149 + then (fn k =>
12.2150 + Lt (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e))))
12.2151 + else (fn _ => Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e))))
12.2152 | a_beta (Le (Cn (dm, c, e))) =
12.2153 - (if eqop eq_nat dm 0
12.2154 - then (fn k => Le (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2155 - else (fn k => Le (Cn (suc (minus_nat dm 1), c, e))))
12.2156 + (if ((dm : IntInf.int) = (0 : IntInf.int))
12.2157 + then (fn k =>
12.2158 + Le (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e))))
12.2159 + else (fn _ => Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e))))
12.2160 | a_beta (Gt (Cn (em, c, e))) =
12.2161 - (if eqop eq_nat em 0
12.2162 - then (fn k => Gt (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2163 - else (fn k => Gt (Cn (suc (minus_nat em 1), c, e))))
12.2164 + (if ((em : IntInf.int) = (0 : IntInf.int))
12.2165 + then (fn k =>
12.2166 + Gt (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e))))
12.2167 + else (fn _ => Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e))))
12.2168 | a_beta (Ge (Cn (fm, c, e))) =
12.2169 - (if eqop eq_nat fm 0
12.2170 - then (fn k => Ge (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2171 - else (fn k => Ge (Cn (suc (minus_nat fm 1), c, e))))
12.2172 + (if ((fm : IntInf.int) = (0 : IntInf.int))
12.2173 + then (fn k =>
12.2174 + Ge (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e))))
12.2175 + else (fn _ => Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e))))
12.2176 | a_beta (Eq (Cn (gm, c, e))) =
12.2177 - (if eqop eq_nat gm 0
12.2178 - then (fn k => Eq (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2179 - else (fn k => Eq (Cn (suc (minus_nat gm 1), c, e))))
12.2180 + (if ((gm : IntInf.int) = (0 : IntInf.int))
12.2181 + then (fn k =>
12.2182 + Eq (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e))))
12.2183 + else (fn _ => Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e))))
12.2184 | a_beta (NEq (Cn (hm, c, e))) =
12.2185 - (if eqop eq_nat hm 0
12.2186 - then (fn k => NEq (Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2187 - else (fn k => NEq (Cn (suc (minus_nat hm 1), c, e))))
12.2188 + (if ((hm : IntInf.int) = (0 : IntInf.int))
12.2189 + then (fn k =>
12.2190 + NEq (Cn ((0 : IntInf.int), (1 : IntInf.int),
12.2191 + Mul (div_int k c, e))))
12.2192 + else (fn _ => NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e))))
12.2193 | a_beta (Dvd (i, Cn (im, c, e))) =
12.2194 - (if eqop eq_nat im 0
12.2195 + (if ((im : IntInf.int) = (0 : IntInf.int))
12.2196 then (fn k =>
12.2197 Dvd (IntInf.* (div_int k c, i),
12.2198 - Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2199 - else (fn k => Dvd (i, Cn (suc (minus_nat im 1), c, e))))
12.2200 + Cn ((0 : IntInf.int), (1 : IntInf.int),
12.2201 + Mul (div_int k c, e))))
12.2202 + else (fn _ => Dvd (i, Cn (suc (minus_nat im (1 : IntInf.int)), c, e))))
12.2203 | a_beta (NDvd (i, Cn (jm, c, e))) =
12.2204 - (if eqop eq_nat jm 0
12.2205 + (if ((jm : IntInf.int) = (0 : IntInf.int))
12.2206 then (fn k =>
12.2207 NDvd (IntInf.* (div_int k c, i),
12.2208 - Cn (0, (1 : IntInf.int), Mul (div_int k c, e))))
12.2209 - else (fn k => NDvd (i, Cn (suc (minus_nat jm 1), c, e))));
12.2210 + Cn ((0 : IntInf.int), (1 : IntInf.int),
12.2211 + Mul (div_int k c, e))))
12.2212 + else (fn _ => NDvd (i, Cn (suc (minus_nat jm (1 : IntInf.int)), c, e))));
12.2213
12.2214 -fun zeta (And (p, q)) = zlcm (zeta p) (zeta q)
12.2215 - | zeta (Or (p, q)) = zlcm (zeta p) (zeta q)
12.2216 +fun zeta (And (p, q)) = lcm_int (zeta p) (zeta q)
12.2217 + | zeta (Or (p, q)) = lcm_int (zeta p) (zeta q)
12.2218 | zeta T = (1 : IntInf.int)
12.2219 | zeta F = (1 : IntInf.int)
12.2220 | zeta (Lt (C bo)) = (1 : IntInf.int)
12.2221 @@ -1367,64 +1960,59 @@
12.2222 | zeta (Closed ap) = (1 : IntInf.int)
12.2223 | zeta (NClosed aq) = (1 : IntInf.int)
12.2224 | zeta (Lt (Cn (cm, c, e))) =
12.2225 - (if eqop eq_nat cm 0 then c else (1 : IntInf.int))
12.2226 + (if ((cm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2227 | zeta (Le (Cn (dm, c, e))) =
12.2228 - (if eqop eq_nat dm 0 then c else (1 : IntInf.int))
12.2229 + (if ((dm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2230 | zeta (Gt (Cn (em, c, e))) =
12.2231 - (if eqop eq_nat em 0 then c else (1 : IntInf.int))
12.2232 + (if ((em : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2233 | zeta (Ge (Cn (fm, c, e))) =
12.2234 - (if eqop eq_nat fm 0 then c else (1 : IntInf.int))
12.2235 + (if ((fm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2236 | zeta (Eq (Cn (gm, c, e))) =
12.2237 - (if eqop eq_nat gm 0 then c else (1 : IntInf.int))
12.2238 + (if ((gm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2239 | zeta (NEq (Cn (hm, c, e))) =
12.2240 - (if eqop eq_nat hm 0 then c else (1 : IntInf.int))
12.2241 + (if ((hm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2242 | zeta (Dvd (i, Cn (im, c, e))) =
12.2243 - (if eqop eq_nat im 0 then c else (1 : IntInf.int))
12.2244 + (if ((im : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int))
12.2245 | zeta (NDvd (i, Cn (jm, c, e))) =
12.2246 - (if eqop eq_nat jm 0 then c else (1 : IntInf.int));
12.2247 + (if ((jm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int));
12.2248
12.2249 fun zsplit0 (C c) = ((0 : IntInf.int), C c)
12.2250 | zsplit0 (Bound n) =
12.2251 - (if eqop eq_nat n 0 then ((1 : IntInf.int), C (0 : IntInf.int))
12.2252 + (if ((n : IntInf.int) = (0 : IntInf.int))
12.2253 + then ((1 : IntInf.int), C (0 : IntInf.int))
12.2254 else ((0 : IntInf.int), Bound n))
12.2255 | zsplit0 (Cn (n, i, a)) =
12.2256 let
12.2257 - val aa = zsplit0 a;
12.2258 - val (i', a') = aa;
12.2259 + val (ia, aa) = zsplit0 a;
12.2260 in
12.2261 - (if eqop eq_nat n 0 then (IntInf.+ (i, i'), a') else (i', Cn (n, i, a')))
12.2262 + (if ((n : IntInf.int) = (0 : IntInf.int)) then (IntInf.+ (i, ia), aa)
12.2263 + else (ia, Cn (n, i, aa)))
12.2264 end
12.2265 | zsplit0 (Neg a) =
12.2266 let
12.2267 - val aa = zsplit0 a;
12.2268 - val (i', a') = aa;
12.2269 + val (i, aa) = zsplit0 a;
12.2270 in
12.2271 - (IntInf.~ i', Neg a')
12.2272 + (IntInf.~ i, Neg aa)
12.2273 end
12.2274 | zsplit0 (Add (a, b)) =
12.2275 let
12.2276 - val aa = zsplit0 a;
12.2277 - val (ia, a') = aa;
12.2278 - val ab = zsplit0 b;
12.2279 - val (ib, b') = ab;
12.2280 + val (ia, aa) = zsplit0 a;
12.2281 + val (ib, ba) = zsplit0 b;
12.2282 in
12.2283 - (IntInf.+ (ia, ib), Add (a', b'))
12.2284 + (IntInf.+ (ia, ib), Add (aa, ba))
12.2285 end
12.2286 | zsplit0 (Sub (a, b)) =
12.2287 let
12.2288 - val aa = zsplit0 a;
12.2289 - val (ia, a') = aa;
12.2290 - val ab = zsplit0 b;
12.2291 - val (ib, b') = ab;
12.2292 + val (ia, aa) = zsplit0 a;
12.2293 + val (ib, ba) = zsplit0 b;
12.2294 in
12.2295 - (IntInf.- (ia, ib), Sub (a', b'))
12.2296 + (IntInf.- (ia, ib), Sub (aa, ba))
12.2297 end
12.2298 | zsplit0 (Mul (i, a)) =
12.2299 let
12.2300 - val aa = zsplit0 a;
12.2301 - val (i', a') = aa;
12.2302 + val (ia, aa) = zsplit0 a;
12.2303 in
12.2304 - (IntInf.* (i, i'), Mul (i, a'))
12.2305 + (IntInf.* (i, ia), Mul (i, aa))
12.2306 end;
12.2307
12.2308 fun zlfm (And (p, q)) = And (zlfm p, zlfm q)
12.2309 @@ -1434,79 +2022,79 @@
12.2310 Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q)))
12.2311 | zlfm (Lt a) =
12.2312 let
12.2313 - val aa = zsplit0 a;
12.2314 - val (c, r) = aa;
12.2315 + val (c, r) = zsplit0 a;
12.2316 in
12.2317 - (if eqop eq_int c (0 : IntInf.int) then Lt r
12.2318 - else (if IntInf.< ((0 : IntInf.int), c) then Lt (Cn (0, c, r))
12.2319 - else Gt (Cn (0, IntInf.~ c, Neg r))))
12.2320 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Lt r
12.2321 + else (if IntInf.< ((0 : IntInf.int), c)
12.2322 + then Lt (Cn ((0 : IntInf.int), c, r))
12.2323 + else Gt (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2324 end
12.2325 | zlfm (Le a) =
12.2326 let
12.2327 - val aa = zsplit0 a;
12.2328 - val (c, r) = aa;
12.2329 + val (c, r) = zsplit0 a;
12.2330 in
12.2331 - (if eqop eq_int c (0 : IntInf.int) then Le r
12.2332 - else (if IntInf.< ((0 : IntInf.int), c) then Le (Cn (0, c, r))
12.2333 - else Ge (Cn (0, IntInf.~ c, Neg r))))
12.2334 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Le r
12.2335 + else (if IntInf.< ((0 : IntInf.int), c)
12.2336 + then Le (Cn ((0 : IntInf.int), c, r))
12.2337 + else Ge (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2338 end
12.2339 | zlfm (Gt a) =
12.2340 let
12.2341 - val aa = zsplit0 a;
12.2342 - val (c, r) = aa;
12.2343 + val (c, r) = zsplit0 a;
12.2344 in
12.2345 - (if eqop eq_int c (0 : IntInf.int) then Gt r
12.2346 - else (if IntInf.< ((0 : IntInf.int), c) then Gt (Cn (0, c, r))
12.2347 - else Lt (Cn (0, IntInf.~ c, Neg r))))
12.2348 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Gt r
12.2349 + else (if IntInf.< ((0 : IntInf.int), c)
12.2350 + then Gt (Cn ((0 : IntInf.int), c, r))
12.2351 + else Lt (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2352 end
12.2353 | zlfm (Ge a) =
12.2354 let
12.2355 - val aa = zsplit0 a;
12.2356 - val (c, r) = aa;
12.2357 + val (c, r) = zsplit0 a;
12.2358 in
12.2359 - (if eqop eq_int c (0 : IntInf.int) then Ge r
12.2360 - else (if IntInf.< ((0 : IntInf.int), c) then Ge (Cn (0, c, r))
12.2361 - else Le (Cn (0, IntInf.~ c, Neg r))))
12.2362 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Ge r
12.2363 + else (if IntInf.< ((0 : IntInf.int), c)
12.2364 + then Ge (Cn ((0 : IntInf.int), c, r))
12.2365 + else Le (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2366 end
12.2367 | zlfm (Eq a) =
12.2368 let
12.2369 - val aa = zsplit0 a;
12.2370 - val (c, r) = aa;
12.2371 + val (c, r) = zsplit0 a;
12.2372 in
12.2373 - (if eqop eq_int c (0 : IntInf.int) then Eq r
12.2374 - else (if IntInf.< ((0 : IntInf.int), c) then Eq (Cn (0, c, r))
12.2375 - else Eq (Cn (0, IntInf.~ c, Neg r))))
12.2376 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Eq r
12.2377 + else (if IntInf.< ((0 : IntInf.int), c)
12.2378 + then Eq (Cn ((0 : IntInf.int), c, r))
12.2379 + else Eq (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2380 end
12.2381 | zlfm (NEq a) =
12.2382 let
12.2383 - val aa = zsplit0 a;
12.2384 - val (c, r) = aa;
12.2385 + val (c, r) = zsplit0 a;
12.2386 in
12.2387 - (if eqop eq_int c (0 : IntInf.int) then NEq r
12.2388 - else (if IntInf.< ((0 : IntInf.int), c) then NEq (Cn (0, c, r))
12.2389 - else NEq (Cn (0, IntInf.~ c, Neg r))))
12.2390 + (if ((c : IntInf.int) = (0 : IntInf.int)) then NEq r
12.2391 + else (if IntInf.< ((0 : IntInf.int), c)
12.2392 + then NEq (Cn ((0 : IntInf.int), c, r))
12.2393 + else NEq (Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2394 end
12.2395 | zlfm (Dvd (i, a)) =
12.2396 - (if eqop eq_int i (0 : IntInf.int) then zlfm (Eq a)
12.2397 + (if ((i : IntInf.int) = (0 : IntInf.int)) then zlfm (Eq a)
12.2398 else let
12.2399 - val aa = zsplit0 a;
12.2400 - val (c, r) = aa;
12.2401 + val (c, r) = zsplit0 a;
12.2402 in
12.2403 - (if eqop eq_int c (0 : IntInf.int) then Dvd (abs_int i, r)
12.2404 + (if ((c : IntInf.int) = (0 : IntInf.int)) then Dvd (abs_int i, r)
12.2405 else (if IntInf.< ((0 : IntInf.int), c)
12.2406 - then Dvd (abs_int i, Cn (0, c, r))
12.2407 - else Dvd (abs_int i, Cn (0, IntInf.~ c, Neg r))))
12.2408 + then Dvd (abs_int i, Cn ((0 : IntInf.int), c, r))
12.2409 + else Dvd (abs_int i,
12.2410 + Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2411 end)
12.2412 | zlfm (NDvd (i, a)) =
12.2413 - (if eqop eq_int i (0 : IntInf.int) then zlfm (NEq a)
12.2414 + (if ((i : IntInf.int) = (0 : IntInf.int)) then zlfm (NEq a)
12.2415 else let
12.2416 - val aa = zsplit0 a;
12.2417 - val (c, r) = aa;
12.2418 + val (c, r) = zsplit0 a;
12.2419 in
12.2420 - (if eqop eq_int c (0 : IntInf.int) then NDvd (abs_int i, r)
12.2421 + (if ((c : IntInf.int) = (0 : IntInf.int)) then NDvd (abs_int i, r)
12.2422 else (if IntInf.< ((0 : IntInf.int), c)
12.2423 - then NDvd (abs_int i, Cn (0, c, r))
12.2424 - else NDvd (abs_int i, Cn (0, IntInf.~ c, Neg r))))
12.2425 + then NDvd (abs_int i, Cn ((0 : IntInf.int), c, r))
12.2426 + else NDvd (abs_int i,
12.2427 + Cn ((0 : IntInf.int), IntInf.~ c, Neg r))))
12.2428 end)
12.2429 | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q))
12.2430 | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q))
12.2431 @@ -1537,10 +2125,11 @@
12.2432
12.2433 fun unita p =
12.2434 let
12.2435 - val p' = zlfm p;
12.2436 - val l = zeta p';
12.2437 + val pa = zlfm p;
12.2438 + val l = zeta pa;
12.2439 val q =
12.2440 - And (Dvd (l, Cn (0, (1 : IntInf.int), C (0 : IntInf.int))), a_beta p' l);
12.2441 + And (Dvd (l, Cn ((0 : IntInf.int), (1 : IntInf.int), C (0 : IntInf.int))),
12.2442 + a_beta pa l);
12.2443 val d = delta q;
12.2444 val b = remdups eq_numa (map simpnum (beta q));
12.2445 val a = remdups eq_numa (map simpnum (alpha q));
12.2446 @@ -1551,18 +2140,16 @@
12.2447
12.2448 fun cooper p =
12.2449 let
12.2450 - val a = unita p;
12.2451 - val (q, aa) = a;
12.2452 - val (b, d) = aa;
12.2453 + val (q, (b, d)) = unita p;
12.2454 val js = iupt (1 : IntInf.int) d;
12.2455 val mq = simpfm (minusinf q);
12.2456 val md = evaldjf (fn j => simpfm (subst0 (C j) mq)) js;
12.2457 in
12.2458 - (if eqop eq_fma md T then T
12.2459 + (if eq_fm md T then T
12.2460 else let
12.2461 val qd =
12.2462 - evaldjf (fn ab as (ba, j) => simpfm (subst0 (Add (ba, C j)) q))
12.2463 - (concat (map (fn ba => map (fn ab => (ba, ab)) js) b));
12.2464 + evaldjf (fn (ba, j) => simpfm (subst0 (Add (ba, C j)) q))
12.2465 + (concat_map (fn ba => map (fn a => (ba, a)) js) b);
12.2466 in
12.2467 decr (disj md qd)
12.2468 end)
12.2469 @@ -1669,37 +2256,19 @@
12.2470 | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe))
12.2471 | qelim (Imp (p, q)) = (fn qe => impa (qelim p qe) (qelim q qe))
12.2472 | qelim (Iff (p, q)) = (fn qe => iffa (qelim p qe) (qelim q qe))
12.2473 - | qelim T = (fn y => simpfm T)
12.2474 - | qelim F = (fn y => simpfm F)
12.2475 - | qelim (Lt u) = (fn y => simpfm (Lt u))
12.2476 - | qelim (Le v) = (fn y => simpfm (Le v))
12.2477 - | qelim (Gt w) = (fn y => simpfm (Gt w))
12.2478 - | qelim (Ge x) = (fn y => simpfm (Ge x))
12.2479 - | qelim (Eq y) = (fn ya => simpfm (Eq y))
12.2480 - | qelim (NEq z) = (fn y => simpfm (NEq z))
12.2481 - | qelim (Dvd (aa, ab)) = (fn y => simpfm (Dvd (aa, ab)))
12.2482 - | qelim (NDvd (ac, ad)) = (fn y => simpfm (NDvd (ac, ad)))
12.2483 - | qelim (Closed ap) = (fn y => simpfm (Closed ap))
12.2484 - | qelim (NClosed aq) = (fn y => simpfm (NClosed aq));
12.2485 + | qelim T = (fn _ => simpfm T)
12.2486 + | qelim F = (fn _ => simpfm F)
12.2487 + | qelim (Lt u) = (fn _ => simpfm (Lt u))
12.2488 + | qelim (Le v) = (fn _ => simpfm (Le v))
12.2489 + | qelim (Gt w) = (fn _ => simpfm (Gt w))
12.2490 + | qelim (Ge x) = (fn _ => simpfm (Ge x))
12.2491 + | qelim (Eq y) = (fn _ => simpfm (Eq y))
12.2492 + | qelim (NEq z) = (fn _ => simpfm (NEq z))
12.2493 + | qelim (Dvd (aa, ab)) = (fn _ => simpfm (Dvd (aa, ab)))
12.2494 + | qelim (NDvd (ac, ad)) = (fn _ => simpfm (NDvd (ac, ad)))
12.2495 + | qelim (Closed ap) = (fn _ => simpfm (Closed ap))
12.2496 + | qelim (NClosed aq) = (fn _ => simpfm (NClosed aq));
12.2497
12.2498 fun pa p = qelim (prep p) cooper;
12.2499
12.2500 -fun neg z = IntInf.< (z, (0 : IntInf.int));
12.2501 -
12.2502 -fun nat_aux i n =
12.2503 - (if IntInf.<= (i, (0 : IntInf.int)) then n
12.2504 - else nat_aux (IntInf.- (i, (1 : IntInf.int))) (suc n));
12.2505 -
12.2506 -fun adjust b =
12.2507 - (fn a as (q, r) =>
12.2508 - (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
12.2509 - then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
12.2510 - IntInf.- (r, b))
12.2511 - else (IntInf.* ((2 : IntInf.int), q), r)));
12.2512 -
12.2513 -fun posDivAlg a b =
12.2514 - (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
12.2515 - then ((0 : IntInf.int), a)
12.2516 - else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
12.2517 -
12.2518 -end; (*struct GeneratedCooper*)
12.2519 +end; (*struct Generated_Cooper*)
13.1 --- a/src/Tools/Code/code_eval.ML Thu Apr 29 17:50:11 2010 +0200
13.2 +++ b/src/Tools/Code/code_eval.ML Thu Apr 29 18:41:38 2010 +0200
13.3 @@ -1,4 +1,4 @@
13.4 -(* Title: Tools/code/code_eval.ML_
13.5 +(* Title: Tools/code/code_eval.ML
13.6 Author: Florian Haftmann, TU Muenchen
13.7
13.8 Runtime services building on code generation into implementation language SML.
13.9 @@ -97,19 +97,6 @@
13.10 fun print_const const all_struct_name tycos_map consts_map =
13.11 (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
13.12
13.13 -fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
13.14 - let
13.15 - val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
13.16 - fun check_base name name'' =
13.17 - if upperize (Long_Name.base_name name) = upperize name''
13.18 - then () else error ("Name as printed " ^ quote name''
13.19 - ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
13.20 - val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
13.21 - val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
13.22 - val _ = check_base tyco tyco'';
13.23 - val _ = map2 check_base constrs constrs'';
13.24 - in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
13.25 -
13.26 fun print_code is_first print_it ctxt =
13.27 let
13.28 val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
13.29 @@ -128,18 +115,6 @@
13.30 val background' = register_const const background;
13.31 in (print_code is_first (print_const const), background') end;
13.32
13.33 -fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background =
13.34 - let
13.35 - val thy = ProofContext.theory_of background;
13.36 - val tyco = Sign.intern_type thy raw_tyco;
13.37 - val constrs = map (Code.check_const thy) raw_constrs;
13.38 - val constrs' = (map fst o snd o Code.get_type thy) tyco;
13.39 - val _ = if eq_set (op =) (constrs, constrs') then ()
13.40 - else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
13.41 - val is_first = is_first_occ background;
13.42 - val background' = register_datatype tyco constrs background;
13.43 - in (print_code is_first (print_datatype tyco constrs), background') end;
13.44 -
13.45 end; (*local*)
13.46
13.47
13.48 @@ -226,10 +201,6 @@
13.49 (** Isar setup **)
13.50
13.51 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
13.52 -val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
13.53 - (Args.type_name true --| Scan.lift (Args.$$$ "=")
13.54 - -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
13.55 - >> ml_code_datatype_antiq);
13.56
13.57 local
13.58
13.59 @@ -238,7 +209,6 @@
13.60
13.61 val datatypesK = "datatypes";
13.62 val functionsK = "functions";
13.63 -val module_nameK = "module_name";
13.64 val fileK = "file";
13.65 val andK = "and"
13.66
13.67 @@ -250,12 +220,11 @@
13.68
13.69 val _ =
13.70 OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
13.71 - K.thy_decl (Scan.optional (P.$$$ datatypesK |-- (parse_datatype
13.72 + K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
13.73 ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
13.74 -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
13.75 - --| P.$$$ module_nameK -- P.name
13.76 -- Scan.option (P.$$$ fileK |-- P.name)
13.77 - >> (fn (((raw_datatypes, raw_functions), module_name), some_file) => Toplevel.theory
13.78 + >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
13.79 (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
13.80
13.81 end; (*local*)
14.1 --- a/src/Tools/Code/code_haskell.ML Thu Apr 29 17:50:11 2010 +0200
14.2 +++ b/src/Tools/Code/code_haskell.ML Thu Apr 29 18:41:38 2010 +0200
14.3 @@ -309,10 +309,10 @@
14.4
14.5 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
14.6 raw_reserved includes raw_module_alias
14.7 - syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program cs destination =
14.8 + syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
14.9 let
14.10 - val stmt_names = Code_Target.stmt_names_of_destination destination;
14.11 - val module_name = if null stmt_names then raw_module_name else SOME "Code";
14.12 + val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
14.13 + val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
14.14 val reserved = fold (insert (op =) o fst) includes raw_reserved;
14.15 val (deresolver, hs_program) = haskell_program_of_program labelled_name
14.16 module_name module_prefix reserved raw_module_alias program;
14.17 @@ -365,13 +365,13 @@
14.18 );
14.19 in print_module module_name' content end;
14.20 fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
14.21 - (fn (name, (_, SOME stmt)) => if null stmt_names
14.22 - orelse member (op =) stmt_names name
14.23 + (fn (name, (_, SOME stmt)) => if null presentation_stmt_names
14.24 + orelse member (op =) presentation_stmt_names name
14.25 then SOME (print_stmt false (name, stmt))
14.26 else NONE
14.27 | (_, (_, NONE)) => NONE) stmts);
14.28 val serialize_module =
14.29 - if null stmt_names then serialize_module1 else pair "" o serialize_module2;
14.30 + if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2;
14.31 fun check_destination destination =
14.32 (File.check destination; destination);
14.33 fun write_module destination (modlname, content) =
15.1 --- a/src/Tools/Code/code_ml.ML Thu Apr 29 17:50:11 2010 +0200
15.2 +++ b/src/Tools/Code/code_ml.ML Thu Apr 29 18:41:38 2010 +0200
15.3 @@ -1,4 +1,4 @@
15.4 -(* Title: Tools/code/code_ml.ML_
15.5 +(* Title: Tools/code/code_ml.ML
15.6 Author: Florian Haftmann, TU Muenchen
15.7
15.8 Serializer for SML and OCaml.
16.1 --- a/src/Tools/Code/code_scala.ML Thu Apr 29 17:50:11 2010 +0200
16.2 +++ b/src/Tools/Code/code_scala.ML Thu Apr 29 18:41:38 2010 +0200
16.3 @@ -340,10 +340,10 @@
16.4
16.5 fun serialize_scala raw_module_name labelled_name
16.6 raw_reserved includes raw_module_alias
16.7 - _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program cs destination =
16.8 + _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
16.9 let
16.10 - val stmt_names = Code_Target.stmt_names_of_destination destination;
16.11 - val module_name = if null stmt_names then raw_module_name else SOME "Code";
16.12 + val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
16.13 + val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
16.14 val reserved = fold (insert (op =) o fst) includes raw_reserved;
16.15 val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
16.16 module_name reserved raw_module_alias program;
17.1 --- a/src/Tools/Code/code_target.ML Thu Apr 29 17:50:11 2010 +0200
17.2 +++ b/src/Tools/Code/code_target.ML Thu Apr 29 18:41:38 2010 +0200
17.3 @@ -279,7 +279,7 @@
17.4 (Symtab.lookup module_alias) (Symtab.lookup class')
17.5 (Symtab.lookup tyco') (Symtab.lookup const')
17.6 (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
17.7 - program4 names2
17.8 + program4 names1
17.9 end;
17.10
17.11 fun mount_serializer thy alt_serializer target some_width module args naming program names =