equal
deleted
inserted
replaced
79 fun mk_meta_equation th = |
79 fun mk_meta_equation th = |
80 case prop_of th of |
80 case prop_of th of |
81 Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} |
81 Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} |
82 | _ => th |
82 | _ => th |
83 |
83 |
|
84 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
|
85 |
84 fun full_fun_cong_expand th = |
86 fun full_fun_cong_expand th = |
85 let |
87 let |
86 val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) |
88 val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) |
87 val i = length (binder_types (fastype_of f)) - length args |
89 val i = length (binder_types (fastype_of f)) - length args |
88 in funpow i (fn th => th RS @{thm meta_fun_cong}) th end; |
90 in funpow i (fn th => th RS meta_fun_cong) th end; |
89 |
91 |
90 fun declare_names s xs ctxt = |
92 fun declare_names s xs ctxt = |
91 let |
93 let |
92 val res = Name.names ctxt s xs |
94 val res = Name.names ctxt s xs |
93 in (res, fold Name.declare (map fst res) ctxt) end |
95 in (res, fold Name.declare (map fst res) ctxt) end |