src/Provers/Arith/combine_numerals.ML
changeset 13484 d8f5d3391766
parent 9646 aa3b82085e07
child 14387 e96d5c42c4b0
equal deleted inserted replaced
13483:0e6adce08fb0 13484:d8f5d3391766
    25   val mk_coeff: int * term -> term
    25   val mk_coeff: int * term -> term
    26   val dest_coeff: term -> int * term
    26   val dest_coeff: term -> 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 -> Sign.sg -> term * term -> thm option
    30   val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
    31   val trans_tac: thm option -> tactic (*applies the initial lemma*)
    31   val trans_tac: thm option -> tactic (*applies the initial lemma*)
    32   val norm_tac: tactic                (*proves the initial lemma*)
    32   val norm_tac: tactic                (*proves the initial lemma*)
    33   val numeral_simp_tac: tactic        (*proves the final theorem*)
    33   val numeral_simp_tac: tactic        (*proves the final theorem*)
    34   val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    34   val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    35 end;
    35 end;
    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 sg _ t =
    67 fun proc sg _ t =
    68   let (*first freeze any Vars in the term to prevent flex-flex problems*)
    68   let (*first freeze any Vars in the term to prevent flex-flex problems*)
    69       val rand_s = gensym"_"
    69       val (t', xs) = Term.adhoc_freeze_vars t;
    70       fun mk_inst (var as Var((a,i),T))  = 
       
    71 	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
       
    72       val t' = subst_atomic (map mk_inst (term_vars t)) t
       
    73       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    70       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    74       val reshape =  (*Move i*u to the front and put j*u into standard form
    71       val reshape =  (*Move i*u to the front and put j*u into standard form
    75 		       i + #m + j + k == #m + i + (j + k) *)
    72 		       i + #m + j + k == #m + i + (j + k) *)
    76 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    73 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    77 		raise TERM("combine_numerals", []) 
    74 		raise TERM("combine_numerals", []) 
    78 	    else Data.prove_conv [Data.norm_tac] sg 
    75 	    else Data.prove_conv [Data.norm_tac] sg xs
    79 			(t', 
    76 			(t', 
    80 			 Data.mk_sum ([Data.mk_coeff(m,u),
    77 			 Data.mk_sum ([Data.mk_coeff(m,u),
    81 				       Data.mk_coeff(n,u)] @ terms))
    78 				       Data.mk_coeff(n,u)] @ terms))
    82   in
    79   in
    83       apsome Data.simplify_meta_eq
    80       apsome Data.simplify_meta_eq
    84 	 (Data.prove_conv 
    81 	 (Data.prove_conv 
    85 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    82 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    86 	     Data.numeral_simp_tac] sg
    83 	     Data.numeral_simp_tac] sg xs
    87 	    (t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    84 	    (t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    88   end
    85   end
    89   handle TERM _ => None
    86   handle TERM _ => None
    90        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
    87        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
    91 			     Undeclared type constructor "Numeral.bin"*)
    88 			     Undeclared type constructor "Numeral.bin"*)