107 fun eq_var bnd novars = |
107 fun eq_var bnd novars = |
108 let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t |
108 let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t |
109 | eq_var_aux k (Const("==>",_) $ A $ B) = |
109 | eq_var_aux k (Const("==>",_) $ A $ B) = |
110 ((k, inspect_pair bnd novars |
110 ((k, inspect_pair bnd novars |
111 (Data.dest_eq (Data.dest_Trueprop A))) |
111 (Data.dest_eq (Data.dest_Trueprop A))) |
112 (*Exception comes from inspect_pair or dest_eq*) |
112 handle TERM _ => eq_var_aux (k+1) B |
113 handle _ => eq_var_aux (k+1) B) |
113 | Match => eq_var_aux (k+1) B) |
114 | eq_var_aux k _ = raise EQ_VAR |
114 | eq_var_aux k _ = raise EQ_VAR |
115 in eq_var_aux 0 end; |
115 in eq_var_aux 0 end; |
116 |
116 |
117 (*For the simpset. Adds ALL suitable equalities, even if not first! |
117 (*For the simpset. Adds ALL suitable equalities, even if not first! |
118 No vars are allowed here, as simpsets are built from meta-assumptions*) |
118 No vars are allowed here, as simpsets are built from meta-assumptions*) |
119 fun mk_eqs bnd th = |
119 fun mk_eqs bnd th = |
120 [ if inspect_pair bnd false (Data.dest_eq |
120 [ if inspect_pair bnd false (Data.dest_eq |
121 (Data.dest_Trueprop (#prop (rep_thm th)))) |
121 (Data.dest_Trueprop (#prop (rep_thm th)))) |
122 then th RS Data.eq_reflection |
122 then th RS Data.eq_reflection |
123 else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
123 else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
124 handle _ => []; (*Exception comes from inspect_pair or dest_eq*) |
124 handle TERM _ => [] | Match => []; |
125 |
125 |
126 local |
126 local |
127 in |
127 in |
128 |
128 |
129 (*Select a suitable equality assumption; substitute throughout the subgoal |
129 (*Select a suitable equality assumption; substitute throughout the subgoal |