--- a/src/HOL/Library/comm_ring.ML Fri Oct 30 01:32:06 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Author: Amine Chaieb
-
-Tactic for solving equalities over commutative rings.
-*)
-
-signature COMM_RING =
-sig
- val comm_ring_tac : Proof.context -> int -> tactic
- val setup : theory -> theory
-end
-
-structure CommRing: COMM_RING =
-struct
-
-(* The Cring exception for erronous uses of cring_tac *)
-exception CRing of string;
-
-(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name HOL.zero}, T);
-fun cring_one T = Const (@{const_name HOL.one}, T);
-
-(* reification functions *)
-(* add two polynom expressions *)
-fun polT t = Type ("Commutative_Ring.pol", [t]);
-fun polexT t = Type ("Commutative_Ring.polex", [t]);
-
-(* pol *)
-fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
-fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
-fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
-
-(* polex *)
-fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
-fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
-fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
-fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
-fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
-fun polex_pow t = Const ("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 vs t = pol_Pc T $ t;
-
-(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
- polex_add T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
- polex_sub T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
- polex_mul T $ reif_polex T vs a $ reif_polex T vs b
- | reif_polex T vs (Const (@{const_name HOL.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 thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
- if Sign.of_sort thy (T, cr_sort) then
- let
- val fs = OldTerm.term_frees eq;
- val cvs = cterm_of thy (HOLogic.mk_list T fs);
- val clhs = cterm_of thy (reif_polex T fs lhs);
- val crhs = cterm_of thy (reif_polex T fs rhs);
- val ca = ctyp_of thy T;
- in (ca, cvs, clhs, crhs) end
- else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
- | reif_eq _ _ = raise CRing "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 =
- [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
- @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
-
-fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
- let
- val thy = ProofContext.theory_of ctxt;
- val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*)
- addsimps cring_simps;
- val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
- val norm_eq_th =
- simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
- in
- cut_rules_tac [norm_eq_th] i
- THEN (simp_tac cring_ss i)
- THEN (simp_tac cring_ss i)
- end);
-
-val setup =
- Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
- "reflective decision procedure for equalities over commutative rings" #>
- Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
- "method for proving algebraic properties (same as comm_ring)";
-
-end;