src/FOL/simpdata.ML
changeset 4188 1025a27b08f9
parent 4094 9e501199ec01
child 4189 b8c7a6bc6c16
equal deleted inserted replaced
4187:2fafec5868fe 4188:1025a27b08f9
   245    fails if there is no equaliy or if an equality is already at the front *)
   245    fails if there is no equaliy or if an equality is already at the front *)
   246 local
   246 local
   247   fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
   247   fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
   248     | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
   248     | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
   249     | is_eq _ = false;
   249     | is_eq _ = false;
   250   fun find_eq n [] = None
   250   val find_eq = find_index is_eq;
   251     | find_eq n (t :: ts) = if (is_eq t) then Some n 
       
   252 			    else find_eq (n + 1) ts;
       
   253 in
   251 in
   254 val rot_eq_tac = 
   252 val rot_eq_tac = 
   255      SUBGOAL (fn (Bi,i) => 
   253      SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
   256 	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
   254 		if n>0 then rotate_tac n i else no_tac end)
   257 		  None   => no_tac
       
   258 		| Some 0 => no_tac
       
   259 		| Some n => rotate_tac n i)
       
   260 end;
   255 end;
   261 
   256 
   262 
   257 
   263 fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
   258 fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
   264 				     safe_asm_full_simp_tac ss;
   259 				     safe_asm_full_simp_tac ss;