24 val ids2str: term -> string list |
24 val ids2str: term -> string list |
25 val ins_concl: term -> term -> term |
25 val ins_concl: term -> term -> term |
26 val inst_abs: term -> term |
26 val inst_abs: term -> term |
27 val inst_bdv: (term * term) list -> term -> term |
27 val inst_bdv: (term * term) list -> term -> term |
28 |
28 |
|
29 val mk_frac: typ -> int * (int * int) -> term |
29 val term_of_num: typ -> int -> term |
30 val term_of_num: typ -> int -> term |
30 val num_of_term: term -> int |
31 val num_of_term: term -> int |
31 val int_of_str: string -> int |
32 val int_of_str: string -> int |
32 val isastr_of_int: int -> string |
33 val isastr_of_int: int -> string |
33 val int_opt_of_string: string -> int option (* belongs to TermC *) |
34 val int_opt_of_string: string -> int option |
34 |
35 |
35 val isalist2list: term -> term list |
36 val isalist2list: term -> term list |
36 val list2isalist: typ -> term list -> term |
37 val list2isalist: typ -> term list -> term |
37 val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *) |
38 val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *) |
38 |
39 |
48 val is_list: term -> bool |
49 val is_list: term -> bool |
49 val is_bool_list: term -> bool |
50 val is_bool_list: term -> bool |
50 val dest_listT: typ -> typ |
51 val dest_listT: typ -> typ |
51 val is_num: term -> bool |
52 val is_num: term -> bool |
52 val is_num': string -> bool |
53 val is_num': string -> bool |
|
54 val string_of_num: term -> string |
53 val variable_constant_pair: term * term -> bool |
55 val variable_constant_pair: term * term -> bool |
54 |
56 |
55 val mk_add: term -> term -> term |
57 val mk_add: term -> term -> term |
56 val mk_free: typ -> string -> term |
58 val mk_free: typ -> string -> term |
57 val mk_equality: term * term -> term |
59 val mk_equality: term * term -> term |
86 |
88 |
87 val numbers_to_string: term -> term |
89 val numbers_to_string: term -> term |
88 val uminus_to_string: term -> term |
90 val uminus_to_string: term -> term |
89 |
91 |
90 val var2free: term -> term |
92 val var2free: term -> term |
91 val vars: term -> term list (* recognises numerals, should replace "fun vars_of" *) |
93 val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*) |
92 val vars': term list -> term list |
94 val vars': term list -> term list |
93 val vars_of: term -> term list (* deprecated *) |
95 val vars_of: term -> term list (* deprecated TODOO: see differences in test/../termC.sml*) |
94 val dest_list': term -> term list |
96 val dest_list': term -> term list |
95 val negates: term -> term -> bool |
97 val negates: term -> term -> bool |
96 |
98 |
97 \<^isac_test>\<open> |
99 \<^isac_test>\<open> |
|
100 val mk_negative: typ -> term -> term |
98 val scala_of_term: term -> string |
101 val scala_of_term: term -> string |
99 val atomtyp(*<-- atom_typ TODO*): typ -> unit |
102 val atomtyp(*<-- atom_typ TODO*): typ -> unit |
100 val atomty: term -> unit |
103 val atomty: term -> unit |
101 val atomw: term -> unit |
104 val atomw: term -> unit |
102 val atomt: term -> unit |
105 val atomt: term -> unit |
241 |
244 |
242 fun str_of_int n = |
245 fun str_of_int n = |
243 if n < 0 then "-" ^ ((string_of_int o abs) n) |
246 if n < 0 then "-" ^ ((string_of_int o abs) n) |
244 else string_of_int n; |
247 else string_of_int n; |
245 val int_of_str = Value.parse_int; |
248 val int_of_str = Value.parse_int; |
246 |
|
247 val int_opt_of_string = ThmC_Def.int_opt_of_string |
249 val int_opt_of_string = ThmC_Def.int_opt_of_string |
248 |
|
249 fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false; |
250 fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false; |
250 fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false; |
251 |
251 fun term_of_num ntyp n = Free (str_of_int n, ntyp); |
252 fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true |
252 fun num_of_term (t as (Free (istr, _))) = |
253 | is_num (Const ("Groups.uminus_class.uminus", _) $ |
253 (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t])) |
254 (Const ("Num.numeral_class.numeral", _) $ _)) = true |
254 | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t]) |
255 | is_num (Const ("Groups.one_class.one", _)) = true |
|
256 | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true |
|
257 | is_num (Const ("Groups.zero_class.zero", _)) = true |
|
258 | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true |
|
259 | is_num _ = false; |
|
260 |
|
261 fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int) |
|
262 |
|
263 fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t |
|
264 fun mk_frac T (sg, (i1, i2)) = |
|
265 if sg = 1 then |
|
266 if i2 = 1 then HOLogic.mk_number T i1 |
|
267 else Const ("Rings.divide_class.divide", T --> T --> T) $ |
|
268 HOLogic.mk_number T i1 $ HOLogic.mk_number T i2 |
|
269 else (*take negative*) |
|
270 if i2 = 1 then mk_negative T (HOLogic.mk_number T i1) |
|
271 else Const ("Rings.divide_class.divide", T --> T --> T) $ |
|
272 mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2 |
|
273 |
|
274 val term_of_num = HOLogic.mk_number; |
|
275 fun num_of_term t = t |> HOLogic.dest_number |> snd; |
255 |
276 |
256 fun is_const (Const _) = true | is_const _ = false; |
277 fun is_const (Const _) = true | is_const _ = false; |
257 fun is_variable (t as Free _) = not (is_num t) |
278 fun is_variable (t as Free _) = not (is_num t) |
258 | is_variable _ = false; |
279 | is_variable _ = false; |
259 fun is_Free (Free _) = true | is_Free _ = false; |
280 fun is_Free (Free _) = true | is_Free _ = false; |
270 else false |
291 else false |
271 |
292 |
272 fun vars t = |
293 fun vars t = |
273 let |
294 let |
274 fun scan vs (Const _) = vs |
295 fun scan vs (Const _) = vs |
275 | scan vs (t as Free (s, _)) = if is_num' s then vs else t :: vs |
296 | scan vs (t as Free _) = (*if is_num' s then vs else*) t :: vs |
276 | scan vs (t as Var _) = t :: vs |
297 | scan vs (t as Var _) = t :: vs |
277 | scan vs (Bound _) = vs |
298 | scan vs (Bound _) = vs |
278 | scan vs (Abs (_, _, t)) = scan vs t |
299 | scan vs (Abs (_, _, t)) = scan vs t |
279 | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2) |
300 | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2) |
280 in ((distinct op =) o (scan [])) t end; |
301 in ((distinct op =) o (scan [])) t end; |
433 fun pairt t1 t2 = Const ("Product_Type.Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2; |
454 fun pairt t1 t2 = Const ("Product_Type.Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2; |
434 |
455 |
435 fun mk_factroot op_(*=thy.sqrt*) T fact root = |
456 fun mk_factroot op_(*=thy.sqrt*) T fact root = |
436 Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $ |
457 Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $ |
437 (Const (op_, T --> T) $ term_of_num T root); |
458 (Const (op_, T --> T) $ term_of_num T root); |
438 fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ Free (str_of_int n, ntyp); |
459 fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ HOLogic.mk_number ntyp n; |
439 fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ Free (str_of_int n, ntyp) $ v; |
460 fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ HOLogic.mk_number ntyp n $ v; |
440 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 = |
461 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 = |
441 Const (op_, Top) $ Free (str_of_int n1, T1) $ Free (str_of_int n2, T2); |
462 Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2; |
442 fun mk_thmid thmid n1 n2 = |
463 fun mk_thmid thmid n1 n2 = |
443 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2); |
464 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2); |
444 fun mk_add t1 t2 = |
465 fun mk_add t1 t2 = |
445 let |
466 let |
446 val (T1, T2) = (type_of t1, type_of t2) |
467 val (T1, T2) = (type_of t1, type_of t2) |
524 WN130613 probably compare to |
545 WN130613 probably compare to |
525 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
546 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
526 fun parse_patt thy str = (thy, str) |
547 fun parse_patt thy str = (thy, str) |
527 |>> ThyC.to_ctxt |
548 |>> ThyC.to_ctxt |
528 |-> Proof_Context.read_term_pattern |
549 |-> Proof_Context.read_term_pattern |
529 |> numbers_to_string (*TODO drop*) |
550 (*|> numbers_to_string TODO drop*) |
530 |> typ_a2real; (*TODO drop*) |
551 |> typ_a2real; (*TODO drop*) |
531 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
552 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
532 |
553 |
533 fun is_atom (Const ("Float.Float",_) $ _) = true |
554 fun is_atom (Const ("Float.Float",_) $ _) = true |
534 | is_atom (Const _) = true |
555 | is_atom (Const _) = true |
569 | var_for vs (t1 $ t2) id = (var_for vs t1 id) @ (var_for vs t2 id) |
590 | var_for vs (t1 $ t2) id = (var_for vs t1 id) @ (var_for vs t2 id) |
570 |
591 |
571 val poly_consts = (* TODO: adopt syntax-const from Isabelle*) |
592 val poly_consts = (* TODO: adopt syntax-const from Isabelle*) |
572 ["Groups.plus_class.plus", "Groups.minus_class.minus", |
593 ["Groups.plus_class.plus", "Groups.minus_class.minus", |
573 "Rings.divide_class.divide", "Groups.times_class.times", |
594 "Rings.divide_class.divide", "Groups.times_class.times", |
574 "Transcendental.powr"]; |
595 "Transcendental.powr", |
|
596 "Num.numeral_class.numeral", "Num.num.Bit0", "Num.num.Bit1", "Num.num.One", |
|
597 "Groups.uminus_class.uminus", "Groups.one_class.one"]; |
575 (* treat Free, Const, Var as variables in polynomials *) |
598 (* treat Free, Const, Var as variables in polynomials *) |
576 fun vars_of t = |
599 fun vars_of t = |
577 let |
600 let |
578 val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord |
601 val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord |
579 in (map (var_for [] t) var_ids) |> flat |> distinct op = end |
602 in (map (var_for [] t) var_ids) |> flat |> distinct op = end |