38 val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length; |
38 val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length; |
39 in |
39 in |
40 (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st |
40 (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st |
41 end; |
41 end; |
42 |
42 |
43 fun coinduction_tac ctxt raw_vars opt_raw_thm prems st = |
43 fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) => |
44 let |
44 let |
45 val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst; |
45 val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst; |
46 fun find_coinduct t = |
46 fun find_coinduct t = |
47 Induct.find_coinductP ctxt t @ |
47 Induct.find_coinductP ctxt t @ |
48 (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []) |
48 (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []) |
49 val raw_thm = case opt_raw_thm |
49 val raw_thm = |
50 of SOME raw_thm => raw_thm |
50 (case opt_raw_thm of |
51 | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd; |
51 SOME raw_thm => raw_thm |
|
52 | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd); |
52 val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1 |
53 val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1 |
53 val cases = Rule_Cases.get raw_thm |> fst |
54 val cases = Rule_Cases.get raw_thm |> fst |
54 in |
55 in |
55 NO_CASES (HEADGOAL ( |
56 HEADGOAL ( |
56 Object_Logic.rulify_tac ctxt THEN' |
57 Object_Logic.rulify_tac ctxt THEN' |
57 Method.insert_tac prems THEN' |
58 Method.insert_tac prems THEN' |
58 Object_Logic.atomize_prems_tac ctxt THEN' |
59 Object_Logic.atomize_prems_tac ctxt THEN' |
59 DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} => |
60 DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} => |
60 let |
61 let |
108 in |
109 in |
109 HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN |
110 HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN |
110 unfold_thms_tac ctxt eqs |
111 unfold_thms_tac ctxt eqs |
111 end)) ctxt)))]) |
112 end)) ctxt)))]) |
112 end) ctxt) THEN' |
113 end) ctxt) THEN' |
113 K (prune_params_tac ctxt))) st |
114 K (prune_params_tac ctxt)) |
114 |> Seq.maps (fn (_, st) => |
115 #> Seq.maps (fn st => |
115 CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st) |
116 CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st) |
116 end; |
117 end)); |
117 |
118 |
118 local |
119 local |
119 |
120 |
120 val ruleN = "rule" |
121 val ruleN = "rule" |
121 val arbitraryN = "arbitrary" |
122 val arbitraryN = "arbitrary" |