109 |
109 |
110 fun cong_tac i st = (case Logic.strip_assums_concl |
110 fun cong_tac i st = (case Logic.strip_assums_concl |
111 (List.nth (prems_of st, i - 1)) of |
111 (List.nth (prems_of st, i - 1)) of |
112 _ $ (_ $ (f $ x) $ (g $ y)) => |
112 _ $ (_ $ (f $ x) $ (g $ y)) => |
113 let |
113 let |
114 val cong' = lift_rule (st, i) cong; |
114 val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong; |
115 val _ $ (_ $ (f' $ x') $ (g' $ y')) = |
115 val _ $ (_ $ (f' $ x') $ (g' $ y')) = |
116 Logic.strip_assums_concl (prop_of cong'); |
116 Logic.strip_assums_concl (prop_of cong'); |
117 val insts = map (pairself (cterm_of (#sign (rep_thm st))) o |
117 val insts = map (pairself (cterm_of (#sign (rep_thm st))) o |
118 apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o |
118 apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o |
119 apfst head_of) [(f', f), (g', g), (x', x), (y', y)] |
119 apfst head_of) [(f', f), (g', g), (x', x), (y', y)] |
149 let |
149 let |
150 val sg = Thm.sign_of_thm state; |
150 val sg = Thm.sign_of_thm state; |
151 val prem = List.nth (prems_of state, i - 1); |
151 val prem = List.nth (prems_of state, i - 1); |
152 val params = Logic.strip_params prem; |
152 val params = Logic.strip_params prem; |
153 val (_, Type (tname, _)) = hd (rev params); |
153 val (_, Type (tname, _)) = hd (rev params); |
154 val exhaustion = lift_rule (state, i) (exh_thm_of tname); |
154 val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname); |
155 val prem' = hd (prems_of exhaustion); |
155 val prem' = hd (prems_of exhaustion); |
156 val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem')); |
156 val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem')); |
157 val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs), |
157 val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs), |
158 cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t)) |
158 cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t)) |
159 (Bound 0) params))] exhaustion |
159 (Bound 0) params))] exhaustion |