src/Provers/Arith/combine_numerals.ML
changeset 20044 92cc2f4c7335
parent 17412 e26cb20ef0cc
child 20114 a1bb4bc68ff3
equal deleted inserted replaced
20043:036128013178 20044:92cc2f4c7335
    25   val mk_coeff: IntInf.int * term -> term
    25   val mk_coeff: IntInf.int * term -> term
    26   val dest_coeff: term -> IntInf.int * term
    26   val dest_coeff: term -> IntInf.int * term
    27   (*rules*)
    27   (*rules*)
    28   val left_distrib: thm
    28   val left_distrib: thm
    29   (*proof tools*)
    29   (*proof tools*)
    30   val prove_conv: tactic list -> theory -> string list -> term * term -> thm option
    30   val prove_conv: tactic list -> Proof.context -> string list -> term * term -> thm option
    31   val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    31   val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    32   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    32   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    33   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    33   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    34   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    34   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    35 end;
    35 end;
    36 
    36 
    37 
    37 
    38 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    38 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    39   sig
    39   sig
    40   val proc: theory -> simpset -> term -> thm option
    40   val proc: simpset -> term -> thm option
    41   end 
    41   end 
    42 =
    42 =
    43 struct
    43 struct
    44 
    44 
    45 (*Remove the first occurrence of #m*u from the term list*)
    45 (*Remove the first occurrence of #m*u from the term list*)
    62 		| NONE => find_repeated (Termtab.update (u, n) tab, 
    62 		| NONE => find_repeated (Termtab.update (u, n) tab, 
    63 					 t::past,  terms))
    63 					 t::past,  terms))
    64 	| NONE => find_repeated (tab, t::past, terms);
    64 	| NONE => find_repeated (tab, t::past, terms);
    65 
    65 
    66 (*the simplification procedure*)
    66 (*the simplification procedure*)
    67 fun proc thy ss t =
    67 fun proc ss t =
    68   let (*first freeze any Vars in the term to prevent flex-flex problems*)
    68   let
       
    69       val ctxt = Simplifier.the_context ss;
       
    70       (*first freeze any Vars in the term to prevent flex-flex problems*)
    69       val (t', xs) = Term.adhoc_freeze_vars t
    71       val (t', xs) = Term.adhoc_freeze_vars t
    70       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    72       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    71       val T = Term.fastype_of u
    73       val T = Term.fastype_of u
    72       val reshape =  (*Move i*u to the front and put j*u into standard form
    74       val reshape =  (*Move i*u to the front and put j*u into standard form
    73 		       i + #m + j + k == #m + i + (j + k) *)
    75 		       i + #m + j + k == #m + i + (j + k) *)
    74 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    76 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    75 		raise TERM("combine_numerals", []) 
    77 		raise TERM("combine_numerals", []) 
    76 	    else Data.prove_conv [Data.norm_tac ss] thy xs
    78 	    else Data.prove_conv [Data.norm_tac ss] ctxt xs
    77 			(t', 
    79 			(t', 
    78 			 Data.mk_sum T ([Data.mk_coeff(m,u),
    80 			 Data.mk_sum T ([Data.mk_coeff(m,u),
    79 				         Data.mk_coeff(n,u)] @ terms))
    81 				         Data.mk_coeff(n,u)] @ terms))
    80   in
    82   in
    81       Option.map (Data.simplify_meta_eq ss)
    83       Option.map (Data.simplify_meta_eq ss)
    82 	 (Data.prove_conv 
    84 	 (Data.prove_conv 
    83 	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    85 	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    84 	     Data.numeral_simp_tac ss] thy xs
    86 	     Data.numeral_simp_tac ss] ctxt xs
    85 	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    87 	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    86   end
    88   end
    87   handle TERM _ => NONE
    89   handle TERM _ => NONE
    88        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    90        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    89 			     Undeclared type constructor "Numeral.bin"*)
    91 			     Undeclared type constructor "Numeral.bin"*)