323 fun assert_eqn thy thm = |
323 fun assert_eqn thy thm = |
324 let |
324 let |
325 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm |
325 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm |
326 handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) |
326 handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) |
327 | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); |
327 | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); |
328 fun vars_of t = fold_aterms |
328 fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v |
329 (fn Var (v, _) => insert (op =) v |
329 | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n" |
330 | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n" |
330 ^ Display.string_of_thm thm) |
331 ^ Display.string_of_thm thm) |
331 | _ => I) t []; |
332 | _ => I) t []; |
332 fun tvars_of t = fold_term_types (fn _ => |
333 fun tvars_of t = fold_term_types |
333 fold_atyps (fn TVar (v, _) => insert (op =) v |
334 (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v |
334 | TFree _ => bad_thm |
335 | TFree _ => bad_thm |
|
336 ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t []; |
335 ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t []; |
337 val lhs_vs = vars_of lhs; |
336 val lhs_vs = vars_of lhs; |
338 val rhs_vs = vars_of rhs; |
337 val rhs_vs = vars_of rhs; |
339 val lhs_tvs = tvars_of lhs; |
338 val lhs_tvs = tvars_of lhs; |
340 val rhs_tvs = tvars_of lhs; |
339 val rhs_tvs = tvars_of rhs; |
341 val _ = if null (subtract (op =) lhs_vs rhs_vs) |
340 val _ = if null (subtract (op =) lhs_vs rhs_vs) |
342 then () |
341 then () |
343 else bad_thm ("Free variables on right hand side of rewrite theorem\n" |
342 else bad_thm ("Free variables on right hand side of rewrite theorem\n" |
344 ^ Display.string_of_thm thm); |
343 ^ Display.string_of_thm thm); |
345 val _ = if null (subtract (op =) lhs_tvs rhs_tvs) |
344 val _ = if null (subtract (op =) lhs_tvs rhs_tvs) |