30 end; |
30 end; |
31 |
31 |
32 |
32 |
33 (* for use when there are no prems to the subgoal *) |
33 (* for use when there are no prems to the subgoal *) |
34 (* does a case split on the given variable *) |
34 (* does a case split on the given variable *) |
35 fun mk_casesplit_goal_thm sgn (vstr,ty) gt = |
35 fun mk_casesplit_goal_thm ctxt (vstr,ty) gt = |
36 let |
36 let |
37 val x = Free(vstr,ty) |
37 val thy = Proof_Context.theory_of ctxt; |
|
38 |
|
39 val x = Free(vstr,ty); |
38 val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); |
40 val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); |
39 |
41 |
40 val ctermify = Thm.global_cterm_of sgn; |
42 val case_thm = case_thm_of_ty thy ty; |
41 val ctypify = Thm.global_ctyp_of sgn; |
|
42 val case_thm = case_thm_of_ty sgn ty; |
|
43 |
43 |
44 val abs_ct = ctermify abst; |
44 val abs_ct = Thm.cterm_of ctxt abst; |
45 val free_ct = ctermify x; |
45 val free_ct = Thm.cterm_of ctxt x; |
46 |
46 |
47 val (Pv, Dv, type_insts) = |
47 val (Pv, Dv, type_insts) = |
48 case (Thm.concl_of case_thm) of |
48 case (Thm.concl_of case_thm) of |
49 (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => |
49 (_ $ (Pv $ (Dv as Var(D, Dty)))) => |
50 (Pv, Dv, |
50 (Pv, Dv, |
51 Sign.typ_match sgn (Dty, ty) Vartab.empty) |
51 Sign.typ_match thy (Dty, ty) Vartab.empty) |
52 | _ => error "not a valid case thm"; |
52 | _ => error "not a valid case thm"; |
53 val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) |
53 val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) |
54 (Vartab.dest type_insts); |
54 (Vartab.dest type_insts); |
55 val cPv = ctermify (Envir.subst_term_types type_insts Pv); |
55 val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv); |
56 val cDv = ctermify (Envir.subst_term_types type_insts Dv); |
56 val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv); |
57 in |
57 in |
58 Conv.fconv_rule Drule.beta_eta_conversion |
58 Conv.fconv_rule Drule.beta_eta_conversion |
59 (case_thm |
59 (case_thm |
60 |> Thm.instantiate (type_cinsts, []) |
60 |> Thm.instantiate (type_cinsts, []) |
61 |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])) |
61 |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])) |
115 case split done during recdef's case analysis, this would avoid us |
115 case split done during recdef's case analysis, this would avoid us |
116 having to (re)search for variables to split. *) |
116 having to (re)search for variables to split. *) |
117 fun splitto ctxt splitths genth = |
117 fun splitto ctxt splitths genth = |
118 let |
118 let |
119 val _ = not (null splitths) orelse error "splitto: no given splitths"; |
119 val _ = not (null splitths) orelse error "splitto: no given splitths"; |
120 val thy = Thm.theory_of_thm genth; |
|
121 |
120 |
122 (* check if we are a member of splitths - FIXME: quicker and |
121 (* check if we are a member of splitths - FIXME: quicker and |
123 more flexible with discrim net. *) |
122 more flexible with discrim net. *) |
124 fun solve_by_splitth th split = |
123 fun solve_by_splitth th split = |
125 Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; |
124 Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; |
132 map (Display.string_of_thm ctxt) splitths @ ["\n--"])); |
131 map (Display.string_of_thm ctxt) splitths @ ["\n--"])); |
133 error "splitto: cannot find variable to split on") |
132 error "splitto: cannot find variable to split on") |
134 | SOME v => |
133 | SOME v => |
135 let |
134 let |
136 val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th))); |
135 val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th))); |
137 val split_thm = mk_casesplit_goal_thm thy v gt; |
136 val split_thm = mk_casesplit_goal_thm ctxt v gt; |
138 val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm; |
137 val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm; |
139 in |
138 in |
140 expf (map recsplitf subthms) |
139 expf (map recsplitf subthms) |
141 end) |
140 end) |
142 |
141 |