src/Provers/Arith/combine_numerals.ML
changeset 8799 89e9deef4bcb
parent 8774 ad5026ff0c16
child 8816 31b4fb3d8d60
equal deleted inserted replaced
8798:d289a68e74ea 8799:89e9deef4bcb
    25   val dest_coeff: term -> int * term
    25   val dest_coeff: term -> int * term
    26   (*rules*)
    26   (*rules*)
    27   val left_distrib: thm
    27   val left_distrib: thm
    28   (*proof tools*)
    28   (*proof tools*)
    29   val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    29   val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    30   val subst_tac: thm option -> tactic
    30   val trans_tac: thm option -> tactic (*applies the initial lemma*)
    31   val norm_tac: tactic
    31   val norm_tac: tactic                (*proves the initial lemma*)
    32   val numeral_simp_tac: tactic
    32   val numeral_simp_tac: tactic        (*proves the final theorem*)
       
    33   val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    33 end;
    34 end;
    34 
    35 
    35 
    36 
    36 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    37 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    37   sig
    38   sig
    74 	    else Data.prove_conv [Data.norm_tac] sg 
    75 	    else Data.prove_conv [Data.norm_tac] sg 
    75 			(t, 
    76 			(t, 
    76 			 Data.mk_sum ([Data.mk_coeff(m,u),
    77 			 Data.mk_sum ([Data.mk_coeff(m,u),
    77 				       Data.mk_coeff(n,u)] @ terms))
    78 				       Data.mk_coeff(n,u)] @ terms))
    78   in
    79   in
    79       Data.prove_conv 
    80       apsome Data.simplify_meta_eq
    80         [Data.subst_tac reshape, rtac Data.left_distrib 1,
    81 	 (Data.prove_conv 
    81 	 Data.numeral_simp_tac] sg
    82 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    82 	(t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))
    83 	     Data.numeral_simp_tac] sg
       
    84 	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
    83   end
    85   end
    84   handle TERM _ => None
    86   handle TERM _ => None
    85        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
    87        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
    86 			     Undeclared type constructor "Numeral.bin"*)
    88 			     Undeclared type constructor "Numeral.bin"*)
    87 
    89