src/HOL/Tools/groebner.ML
changeset 38549 d0385f2764d8
parent 37744 3daaf23b9ab4
child 38558 32ad17fe2b9c
equal deleted inserted replaced
38548:dea0d2cca822 38549:d0385f2764d8
   393 (* Overall parametrized universal procedure for (semi)rings.                 *)
   393 (* Overall parametrized universal procedure for (semi)rings.                 *)
   394 (* We return an ideal_conv and the actual ring prover.                       *)
   394 (* We return an ideal_conv and the actual ring prover.                       *)
   395 
   395 
   396 fun refute_disj rfn tm =
   396 fun refute_disj rfn tm =
   397  case term_of tm of
   397  case term_of tm of
   398   Const("op |",_)$l$r =>
   398   Const(@{const_name "op |"},_)$l$r =>
   399    compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   399    compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   400   | _ => rfn tm ;
   400   | _ => rfn tm ;
   401 
   401 
   402 val notnotD = @{thm notnotD};
   402 val notnotD = @{thm notnotD};
   403 fun mk_binop ct x y = capply (capply ct x) y
   403 fun mk_binop ct x y = capply (capply ct x) y
   404 
   404 
   405 val mk_comb = capply;
   405 val mk_comb = capply;
   406 fun is_neg t =
   406 fun is_neg t =
   407     case term_of t of
   407     case term_of t of
   408       (Const("Not",_)$p) => true
   408       (Const(@{const_name "Not"},_)$p) => true
   409     | _  => false;
   409     | _  => false;
   410 fun is_eq t =
   410 fun is_eq t =
   411  case term_of t of
   411  case term_of t of
   412  (Const("op =",_)$_$_) => true
   412  (Const(@{const_name "op ="},_)$_$_) => true
   413 | _  => false;
   413 | _  => false;
   414 
   414 
   415 fun end_itlist f l =
   415 fun end_itlist f l =
   416   case l of
   416   case l of
   417         []     => error "end_itlist"
   417         []     => error "end_itlist"
   428  end;
   428  end;
   429 
   429 
   430 val strip_exists =
   430 val strip_exists =
   431  let fun h (acc, t) =
   431  let fun h (acc, t) =
   432       case (term_of t) of
   432       case (term_of t) of
   433        Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   433        Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   434      | _ => (acc,t)
   434      | _ => (acc,t)
   435  in fn t => h ([],t)
   435  in fn t => h ([],t)
   436  end;
   436  end;
   437 
   437 
   438 fun is_forall t =
   438 fun is_forall t =
   439  case term_of t of
   439  case term_of t of
   440   (Const("All",_)$Abs(_,_,_)) => true
   440   (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
   441 | _ => false;
   441 | _ => false;
   442 
   442 
   443 val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   443 val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   444 val bool_simps = @{thms bool_simps};
   444 val bool_simps = @{thms bool_simps};
   445 val nnf_simps = @{thms nnf_simps};
   445 val nnf_simps = @{thms nnf_simps};
   520       EX quantifiers are rearranged differently *)
   520       EX quantifiers are rearranged differently *)
   521  fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   521  fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   522  fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   522  fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   523 
   523 
   524 fun choose v th th' = case concl_of th of 
   524 fun choose v th th' = case concl_of th of 
   525   @{term Trueprop} $ (Const("Ex",_)$_) => 
   525   @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) => 
   526    let
   526    let
   527     val p = (funpow 2 Thm.dest_arg o cprop_of) th
   527     val p = (funpow 2 Thm.dest_arg o cprop_of) th
   528     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   528     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   529     val th0 = fconv_rule (Thm.beta_conversion true)
   529     val th0 = fconv_rule (Thm.beta_conversion true)
   530         (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   530         (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   921 end;
   921 end;
   922 
   922 
   923 
   923 
   924 fun find_term bounds tm =
   924 fun find_term bounds tm =
   925   (case term_of tm of
   925   (case term_of tm of
   926     Const ("op =", T) $ _ $ _ =>
   926     Const (@{const_name "op ="}, T) $ _ $ _ =>
   927       if domain_type T = HOLogic.boolT then find_args bounds tm
   927       if domain_type T = HOLogic.boolT then find_args bounds tm
   928       else dest_arg tm
   928       else dest_arg tm
   929   | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
   929   | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
   930   | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
   930   | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
   931   | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
   931   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
   932   | Const ("op &", _) $ _ $ _ => find_args bounds tm
   932   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   933   | Const ("op |", _) $ _ $ _ => find_args bounds tm
   933   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   934   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   934   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
   935   | @{term "op ==>"} $_$_ => find_args bounds tm
   935   | @{term "op ==>"} $_$_ => find_args bounds tm
   936   | Const("op ==",_)$_$_ => find_args bounds tm
   936   | Const("op ==",_)$_$_ => find_args bounds tm
   937   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
   937   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
   938   | _ => raise TERM ("find_term", []))
   938   | _ => raise TERM ("find_term", []))
   939 and find_args bounds tm =
   939 and find_args bounds tm =
   983         | CTERM _ => no_tac
   983         | CTERM _ => no_tac
   984         | THM _ => no_tac);
   984         | THM _ => no_tac);
   985 
   985 
   986 local
   986 local
   987  fun lhs t = case term_of t of
   987  fun lhs t = case term_of t of
   988   Const("op =",_)$_$_ => Thm.dest_arg1 t
   988   Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
   989  | _=> raise CTERM ("ideal_tac - lhs",[t])
   989  | _=> raise CTERM ("ideal_tac - lhs",[t])
   990  fun exitac NONE = no_tac
   990  fun exitac NONE = no_tac
   991    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
   991    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
   992 in 
   992 in 
   993 fun ideal_tac add_ths del_ths ctxt = 
   993 fun ideal_tac add_ths del_ths ctxt =