src/Provers/Arith/combine_numerals.ML
 changeset 9191 300bd596d696 parent 8816 31b4fb3d8d60 child 9571 c869d1886a32
equal inserted replaced
9190:b86ff604729f 9191:300bd596d696
`    62 				     t::past,  terms)`
`    62 				     t::past,  terms)`
`    63       end;`
`    63       end;`
`    64 `
`    64 `
`    65 (*the simplification procedure*)`
`    65 (*the simplification procedure*)`
`    66 fun proc sg _ t =`
`    66 fun proc sg _ t =`
`    67   let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t)`
`    67   let (*first freeze any Vars in the term to prevent flex-flex problems*)`
`       `
`    68       val rand_s = gensym"_"`
`       `
`    69       fun mk_inst (var as Var((a,i),T))  = `
`       `
`    70 	    (var,  Free((a ^ rand_s ^ string_of_int i), T))`
`       `
`    71       val t' = subst_atomic (map mk_inst (term_vars t)) t`
`       `
`    72       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')`
`    68       val reshape =  (*Move i*u to the front and put j*u into standard form`
`    73       val reshape =  (*Move i*u to the front and put j*u into standard form`
`    69 		       i + #m + j + k == #m + i + (j + k) *)`
`    74 		       i + #m + j + k == #m + i + (j + k) *)`
`    70 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)`
`    75 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)`
`    71 		raise TERM("combine_numerals", []) `
`    76 		raise TERM("combine_numerals", []) `
`    72 	    else Data.prove_conv [Data.norm_tac] sg `
`    77 	    else Data.prove_conv [Data.norm_tac] sg `
`    73 			(t, `
`    78 			(t', `
`    74 			 Data.mk_sum ([Data.mk_coeff(m,u),`
`    79 			 Data.mk_sum ([Data.mk_coeff(m,u),`
`    75 				       Data.mk_coeff(n,u)] @ terms))`
`    80 				       Data.mk_coeff(n,u)] @ terms))`
`    76   in`
`    81   in`
`    77       apsome Data.simplify_meta_eq`
`    82       apsome Data.simplify_meta_eq`
`    78 	 (Data.prove_conv `
`    83 	 (Data.prove_conv `
`    79 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,`
`    84 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,`
`    80 	     Data.numeral_simp_tac] sg`
`    85 	     Data.numeral_simp_tac] sg`
`    81 	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))`
`    86 	    (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))`
`    82   end`
`    87   end`
`    83   handle TERM _ => None`
`    88   handle TERM _ => None`
`    84        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)`
`    89        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)`
`    85 			     Undeclared type constructor "Numeral.bin"*)`
`    90 			     Undeclared type constructor "Numeral.bin"*)`
`    86 `
`    91 `