50 |
50 |
51 fun norm_def thm = |
51 fun norm_def thm = |
52 (case Thm.prop_of thm of |
52 (case Thm.prop_of thm of |
53 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
53 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
54 norm_def (thm RS @{thm fun_cong}) |
54 norm_def (thm RS @{thm fun_cong}) |
55 | Const (@{const_name "=="}, _) $ _ $ Abs _ => |
55 | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => |
56 norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
56 norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
57 | _ => thm) |
57 | _ => thm) |
58 |
58 |
59 |
59 |
60 (** atomization **) |
60 (** atomization **) |
61 |
61 |
62 fun atomize_conv ctxt ct = |
62 fun atomize_conv ctxt ct = |
63 (case Thm.term_of ct of |
63 (case Thm.term_of ct of |
64 @{const "==>"} $ _ $ _ => |
64 @{const Pure.imp} $ _ $ _ => |
65 Conv.binop_conv (atomize_conv ctxt) then_conv |
65 Conv.binop_conv (atomize_conv ctxt) then_conv |
66 Conv.rewr_conv @{thm atomize_imp} |
66 Conv.rewr_conv @{thm atomize_imp} |
67 | Const (@{const_name "=="}, _) $ _ $ _ => |
67 | Const (@{const_name Pure.eq}, _) $ _ $ _ => |
68 Conv.binop_conv (atomize_conv ctxt) then_conv |
68 Conv.binop_conv (atomize_conv ctxt) then_conv |
69 Conv.rewr_conv @{thm atomize_eq} |
69 Conv.rewr_conv @{thm atomize_eq} |
70 | Const (@{const_name all}, _) $ Abs _ => |
70 | Const (@{const_name Pure.all}, _) $ Abs _ => |
71 Conv.binder_conv (atomize_conv o snd) ctxt then_conv |
71 Conv.binder_conv (atomize_conv o snd) ctxt then_conv |
72 Conv.rewr_conv @{thm atomize_all} |
72 Conv.rewr_conv @{thm atomize_all} |
73 | _ => Conv.all_conv) ct |
73 | _ => Conv.all_conv) ct |
74 |
74 |
75 val setup_atomize = |
75 val setup_atomize = |
76 fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, |
76 fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, |
77 @{const_name "=="}, @{const_name all}, @{const_name Trueprop}] |
77 @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}] |
78 |
78 |
79 |
79 |
80 (** unfold special quantifiers **) |
80 (** unfold special quantifiers **) |
81 |
81 |
82 local |
82 local |