423 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd |
423 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd |
424 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} |
424 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} |
425 val add_frac_num = mk_meta_eq @{thm "add_frac_num"} |
425 val add_frac_num = mk_meta_eq @{thm "add_frac_num"} |
426 val add_num_frac = mk_meta_eq @{thm "add_num_frac"} |
426 val add_num_frac = mk_meta_eq @{thm "add_num_frac"} |
427 |
427 |
428 fun prove_nz ss T t = |
428 fun prove_nz ctxt = |
|
429 let val ss = local_simpset_of ctxt |
|
430 in fn T => fn t => |
429 let |
431 let |
430 val z = instantiate_cterm ([(zT,T)],[]) zr |
432 val z = instantiate_cterm ([(zT,T)],[]) zr |
431 val eq = instantiate_cterm ([(eqT,T)],[]) geq |
433 val eq = instantiate_cterm ([(eqT,T)],[]) geq |
432 val th = Simplifier.rewrite (ss addsimps simp_thms) |
434 val th = Simplifier.rewrite (ss addsimps simp_thms) |
433 (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} |
435 (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} |
434 (Thm.capply (Thm.capply eq t) z))) |
436 (Thm.capply (Thm.capply eq t) z))) |
435 in equal_elim (symmetric th) TrueI |
437 in equal_elim (symmetric th) TrueI |
436 end |
438 end |
437 |
439 end |
438 fun proc phi ss ct = |
440 |
|
441 fun proc ctxt phi ss ct = |
439 let |
442 let |
440 val ((x,y),(w,z)) = |
443 val ((x,y),(w,z)) = |
441 (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct |
444 (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct |
442 val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] |
445 val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] |
443 val T = ctyp_of_term x |
446 val T = ctyp_of_term x |
444 val [y_nz, z_nz] = map (prove_nz ss T) [y, z] |
447 val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] |
445 val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq |
448 val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq |
446 in SOME (implies_elim (implies_elim th y_nz) z_nz) |
449 in SOME (implies_elim (implies_elim th y_nz) z_nz) |
447 end |
450 end |
448 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
451 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
449 |
452 |
450 fun proc2 phi ss ct = |
453 fun proc2 ctxt phi ss ct = |
451 let |
454 let |
452 val (l,r) = Thm.dest_binop ct |
455 val (l,r) = Thm.dest_binop ct |
453 val T = ctyp_of_term l |
456 val T = ctyp_of_term l |
454 in (case (term_of l, term_of r) of |
457 in (case (term_of l, term_of r) of |
455 (Const(@{const_name "HOL.divide"},_)$_$_, _) => |
458 (Const(@{const_name "HOL.divide"},_)$_$_, _) => |
456 let val (x,y) = Thm.dest_binop l val z = r |
459 let val (x,y) = Thm.dest_binop l val z = r |
457 val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
460 val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
458 val ynz = prove_nz ss T y |
461 val ynz = prove_nz ctxt T y |
459 in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) |
462 in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) |
460 end |
463 end |
461 | (_, Const (@{const_name "HOL.divide"},_)$_$_) => |
464 | (_, Const (@{const_name "HOL.divide"},_)$_$_) => |
462 let val (x,y) = Thm.dest_binop r val z = l |
465 let val (x,y) = Thm.dest_binop r val z = l |
463 val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
466 val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
464 val ynz = prove_nz ss T y |
467 val ynz = prove_nz ctxt T y |
465 in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) |
468 in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) |
466 end |
469 end |
467 | _ => NONE) |
470 | _ => NONE) |
468 end |
471 end |
469 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
472 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
518 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} |
521 val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} |
519 in SOME (mk_meta_eq th) end |
522 in SOME (mk_meta_eq th) end |
520 | _ => NONE) |
523 | _ => NONE) |
521 handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE |
524 handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE |
522 |
525 |
523 val add_frac_frac_simproc = |
526 fun add_frac_frac_simproc ctxt = |
524 make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], |
527 make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], |
525 name = "add_frac_frac_simproc", |
528 name = "add_frac_frac_simproc", |
526 proc = proc, identifier = []} |
529 proc = proc ctxt, identifier = []} |
527 |
530 |
528 val add_frac_num_simproc = |
531 fun add_frac_num_simproc ctxt = |
529 make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], |
532 make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], |
530 name = "add_frac_num_simproc", |
533 name = "add_frac_num_simproc", |
531 proc = proc2, identifier = []} |
534 proc = proc2 ctxt, identifier = []} |
532 |
535 |
533 val ord_frac_simproc = |
536 val ord_frac_simproc = |
534 make_simproc |
537 make_simproc |
535 {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, |
538 {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, |
536 @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"}, |
539 @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"}, |
556 @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, |
559 @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, |
557 @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, |
560 @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, |
558 @{thm "diff_def"}, @{thm "minus_divide_left"}, |
561 @{thm "diff_def"}, @{thm "minus_divide_left"}, |
559 @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym] |
562 @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym] |
560 |
563 |
561 val ss = HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} |
564 |
562 addsimps ths addsimps comp_arith addsimps simp_thms |
565 fun comp_conv ctxt = Simplifier.rewrite |
563 addsimprocs field_cancel_numeral_factors |
566 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} |
564 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, |
567 addsimps ths addsimps comp_arith addsimps simp_thms |
565 ord_frac_simproc] |
568 addsimprocs field_cancel_numeral_factors |
566 addcongs [@{thm "if_weak_cong"}] |
569 addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt, |
567 |
570 ord_frac_simproc] |
568 val comp_conv = Simplifier.rewrite ss |
571 addcongs [@{thm "if_weak_cong"}]) |
|
572 |
569 |
573 |
570 fun numeral_is_const ct = |
574 fun numeral_is_const ct = |
571 case term_of ct of |
575 case term_of ct of |
572 Const (@{const_name "HOL.divide"},_) $ a $ b => |
576 Const (@{const_name "HOL.divide"},_) $ a $ b => |
573 can HOLogic.dest_number a andalso can HOLogic.dest_number b |
577 can HOLogic.dest_number a andalso can HOLogic.dest_number b |