71 _ $ (Const("op <->",_)$_$_) $ _ => th |
71 _ $ (Const("op <->",_)$_$_) $ _ => th |
72 | _ $ (Const("op =",_)$_$_) $ _ => th |
72 | _ $ (Const("op =",_)$_$_) $ _ => th |
73 | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F |
73 | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F |
74 | _ => make_iff_T th; |
74 | _ => make_iff_T th; |
75 |
75 |
76 fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*) |
|
77 _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp) |
|
78 | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @ |
|
79 atomize(th RS conjunct2) |
|
80 | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec) |
|
81 | _ $ (Const("True",_)) $ _ => [] |
|
82 | _ $ (Const("False",_)) $ _ => [] |
|
83 | _ => [th]; |
|
84 |
76 |
85 fun mk_rew_rules th = map mk_eq (atomize th); |
77 val mksimps_pairs = |
|
78 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
79 ("All", [spec]), ("True", []), ("False", [])]; |
|
80 |
|
81 fun mk_atomize pairs = |
|
82 let fun atoms th = |
|
83 (case concl_of th of |
|
84 Const("Trueprop",_) $ p => |
|
85 (case head_of p of |
|
86 Const(a,_) => |
|
87 (case assoc(pairs,a) of |
|
88 Some(rls) => flat (map atoms ([th] RL rls)) |
|
89 | None => [th]) |
|
90 | _ => [th]) |
|
91 | _ => [th]) |
|
92 in atoms end; |
|
93 |
|
94 fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th); |
86 |
95 |
87 (*destruct function for analysing equations*) |
96 (*destruct function for analysing equations*) |
88 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs) |
97 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs) |
89 | dest_red t = raise TERM("FOL/dest_red", [t]); |
98 | dest_red t = raise TERM("FOL/dest_red", [t]); |
90 |
99 |