1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jun 01 15:41:23 2021 +0200
1.3 @@ -26,11 +26,12 @@
1.4 val inst_abs: term -> term
1.5 val inst_bdv: (term * term) list -> term -> term
1.6
1.7 + val mk_frac: typ -> int * (int * int) -> term
1.8 val term_of_num: typ -> int -> term
1.9 val num_of_term: term -> int
1.10 val int_of_str: string -> int
1.11 val isastr_of_int: int -> string
1.12 - val int_opt_of_string: string -> int option (* belongs to TermC *)
1.13 + val int_opt_of_string: string -> int option
1.14
1.15 val isalist2list: term -> term list
1.16 val list2isalist: typ -> term list -> term
1.17 @@ -50,6 +51,7 @@
1.18 val dest_listT: typ -> typ
1.19 val is_num: term -> bool
1.20 val is_num': string -> bool
1.21 + val string_of_num: term -> string
1.22 val variable_constant_pair: term * term -> bool
1.23
1.24 val mk_add: term -> term -> term
1.25 @@ -88,13 +90,14 @@
1.26 val uminus_to_string: term -> term
1.27
1.28 val var2free: term -> term
1.29 - val vars: term -> term list (* recognises numerals, should replace "fun vars_of" *)
1.30 + val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*)
1.31 val vars': term list -> term list
1.32 - val vars_of: term -> term list (* deprecated *)
1.33 + val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*)
1.34 val dest_list': term -> term list
1.35 val negates: term -> term -> bool
1.36
1.37 \<^isac_test>\<open>
1.38 + val mk_negative: typ -> term -> term
1.39 val scala_of_term: term -> string
1.40 val atomtyp(*<-- atom_typ TODO*): typ -> unit
1.41 val atomty: term -> unit
1.42 @@ -243,15 +246,33 @@
1.43 if n < 0 then "-" ^ ((string_of_int o abs) n)
1.44 else string_of_int n;
1.45 val int_of_str = Value.parse_int;
1.46 +val int_opt_of_string = ThmC_Def.int_opt_of_string
1.47 +fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
1.48
1.49 -val int_opt_of_string = ThmC_Def.int_opt_of_string
1.50 +fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true
1.51 + | is_num (Const ("Groups.uminus_class.uminus", _) $
1.52 + (Const ("Num.numeral_class.numeral", _) $ _)) = true
1.53 + | is_num (Const ("Groups.one_class.one", _)) = true
1.54 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true
1.55 + | is_num (Const ("Groups.zero_class.zero", _)) = true
1.56 + | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true
1.57 + | is_num _ = false;
1.58
1.59 -fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
1.60 -fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
1.61 -fun term_of_num ntyp n = Free (str_of_int n, ntyp);
1.62 -fun num_of_term (t as (Free (istr, _))) =
1.63 - (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
1.64 - | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
1.65 +fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
1.66 +
1.67 +fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t
1.68 +fun mk_frac T (sg, (i1, i2)) =
1.69 + if sg = 1 then
1.70 + if i2 = 1 then HOLogic.mk_number T i1
1.71 + else Const ("Rings.divide_class.divide", T --> T --> T) $
1.72 + HOLogic.mk_number T i1 $ HOLogic.mk_number T i2
1.73 + else (*take negative*)
1.74 + if i2 = 1 then mk_negative T (HOLogic.mk_number T i1)
1.75 + else Const ("Rings.divide_class.divide", T --> T --> T) $
1.76 + mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
1.77 +
1.78 +val term_of_num = HOLogic.mk_number;
1.79 +fun num_of_term t = t |> HOLogic.dest_number |> snd;
1.80
1.81 fun is_const (Const _) = true | is_const _ = false;
1.82 fun is_variable (t as Free _) = not (is_num t)
1.83 @@ -272,7 +293,7 @@
1.84 fun vars t =
1.85 let
1.86 fun scan vs (Const _) = vs
1.87 - | scan vs (t as Free (s, _)) = if is_num' s then vs else t :: vs
1.88 + | scan vs (t as Free _) = (*if is_num' s then vs else*) t :: vs
1.89 | scan vs (t as Var _) = t :: vs
1.90 | scan vs (Bound _) = vs
1.91 | scan vs (Abs (_, _, t)) = scan vs t
1.92 @@ -435,10 +456,10 @@
1.93 fun mk_factroot op_(*=thy.sqrt*) T fact root =
1.94 Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
1.95 (Const (op_, T --> T) $ term_of_num T root);
1.96 -fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ Free (str_of_int n, ntyp);
1.97 -fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ Free (str_of_int n, ntyp) $ v;
1.98 +fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ HOLogic.mk_number ntyp n;
1.99 +fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ HOLogic.mk_number ntyp n $ v;
1.100 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
1.101 - Const (op_, Top) $ Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
1.102 + Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
1.103 fun mk_thmid thmid n1 n2 =
1.104 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
1.105 fun mk_add t1 t2 =
1.106 @@ -526,7 +547,7 @@
1.107 fun parse_patt thy str = (thy, str)
1.108 |>> ThyC.to_ctxt
1.109 |-> Proof_Context.read_term_pattern
1.110 - |> numbers_to_string (*TODO drop*)
1.111 +(*|> numbers_to_string TODO drop*)
1.112 |> typ_a2real; (*TODO drop*)
1.113 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.114
1.115 @@ -571,7 +592,9 @@
1.116 val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
1.117 ["Groups.plus_class.plus", "Groups.minus_class.minus",
1.118 "Rings.divide_class.divide", "Groups.times_class.times",
1.119 - "Transcendental.powr"];
1.120 + "Transcendental.powr",
1.121 + "Num.numeral_class.numeral", "Num.num.Bit0", "Num.num.Bit1", "Num.num.One",
1.122 + "Groups.uminus_class.uminus", "Groups.one_class.one"];
1.123 (* treat Free, Const, Var as variables in polynomials *)
1.124 fun vars_of t =
1.125 let
1.126 @@ -614,4 +637,4 @@
1.127 in trm' end
1.128
1.129
1.130 -end
1.131 \ No newline at end of file
1.132 +end