--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sun Jan 29 11:49:48 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(* Title: HOL/Decision_Procs/commutative_ring_tac.ML
- Author: Amine Chaieb
-
-Tactic for solving equalities over commutative rings.
-*)
-
-signature COMMUTATIVE_RING_TAC =
-sig
- val tac: Proof.context -> int -> tactic
-end
-
-structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
-struct
-
-(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name Groups.zero}, T);
-fun cring_one T = Const (@{const_name Groups.one}, T);
-
-(* reification functions *)
-(* add two polynom expressions *)
-fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
-fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
-
-(* pol *)
-fun pol_Pc t =
- Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
-fun pol_Pinj t =
- Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
-fun pol_PX t =
- Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
-
-(* polex *)
-fun polex_add t =
- Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
-fun polex_sub t =
- Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
-fun polex_mul t =
- Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
-fun polex_neg t =
- Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
-fun polex_pol t =
- Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
-fun polex_pow t =
- Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
-
-(* reification of polynoms : primitive cring expressions *)
-fun reif_pol T vs (t as Free _) =
- let
- val one = @{term "1::nat"};
- val i = find_index (fn t' => t' = t) vs
- in
- if i = 0 then
- pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
- else
- pol_Pinj T $ HOLogic.mk_nat i $
- (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
- end
- | reif_pol T _ t = pol_Pc T $ t;
-
-(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
- polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
- polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
- polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) =
- polex_neg T $ reif_polex T vs a
- | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
- polex_pow T $ reif_polex T vs a $ n
- | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
-
-(* reification of the equation *)
-val cr_sort = @{sort comm_ring_1};
-
-fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
- if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
- let
- val fs = Misc_Legacy.term_frees eq;
- val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
- val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
- val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
- val ca = Thm.ctyp_of ctxt T;
- in (ca, cvs, clhs, crhs) end
- else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
- | reif_eq _ _ = error "reif_eq: not an equation";
-
-(* The cring tactic *)
-(* Attention: You have to make sure that no t^0 is in the goal!! *)
-(* Use simply rewriting t^0 = 1 *)
-val cring_simps =
- @{thms mkPX_def mkPinj_def sub_def power_add even_iff_mod_2_eq_zero pow_if power_add [symmetric]};
-
-fun tac ctxt = SUBGOAL (fn (g, i) =>
- let
- val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*)
- val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
- val norm_eq_th = (* may collapse to True *)
- simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
- in
- cut_tac norm_eq_th i
- THEN (simp_tac cring_ctxt i)
- THEN TRY(simp_tac cring_ctxt i)
- end);
-
-end;