src/FOL/simpdata.ML
 changeset 4188 1025a27b08f9 parent 4094 9e501199ec01 child 4189 b8c7a6bc6c16
equal 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;`