--- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Jul 03 14:32:55 2015 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Jul 03 14:41:55 2015 +0200
@@ -18,7 +18,7 @@
val subtractProver : Proof.context -> term -> cterm -> thm -> thm
val distinct_simproc : string list -> simproc
- val discharge : thm list -> thm -> thm
+ val discharge : Proof.context -> thm list -> thm -> thm
end;
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
@@ -140,18 +140,14 @@
in mtch env (t, ct) end;
-fun discharge prems rule =
+fun discharge ctxt prems rule =
let
- val thy = Thm.theory_of_thm (hd prems);
val (tyinsts,insts) =
fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []);
-
val tyinsts' =
- map (fn (v, (S, U)) =>
- (Thm.global_ctyp_of thy (TVar (v, S)), Thm.global_ctyp_of thy U)) tyinsts;
+ map (fn (v, (S, U)) => apply2 (Thm.ctyp_of ctxt) (TVar (v, S), U)) tyinsts;
val insts' =
- map (fn (idxn, ct) =>
- (Thm.global_cterm_of thy (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
+ map (fn (idxn, ct) => (Thm.cterm_of ctxt (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
val rule' = Thm.instantiate (tyinsts', insts') rule;
in fold Thm.elim_implies prems rule' end;
@@ -203,7 +199,7 @@
let
val rule =
(case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right})
- in dist_subtree ps (discharge [thm] rule) end;
+ in dist_subtree ps (discharge ctxt [thm] rule) end;
val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
val dist_subtree_thm = dist_subtree ps dist_thm;
@@ -227,7 +223,7 @@
instantiate ctxt
[(Thm.ctyp_of_cterm x_in_set_left, xT)]
[(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
- in discharge [in_set_l] in_set_left' end
+ in discharge ctxt [in_set_l] in_set_left' end
| Right :: ps' =>
let
val in_set_r = in_set ps' r;
@@ -235,15 +231,17 @@
instantiate ctxt
[(Thm.ctyp_of_cterm x_in_set_right, xT)]
[(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
- in discharge [in_set_r] in_set_right' end)
+ in discharge ctxt [in_set_r] in_set_right' end)
end;
fun in_set' [] = raise TERM ("distinctTreeProver", [])
| in_set' (Left :: ps) = in_set ps l
| in_set' (Right :: ps) = in_set ps r;
- fun distinct_lr node_in_set Left = discharge [dist_subtree_thm, node_in_set] @{thm distinct_left}
- | distinct_lr node_in_set Right = discharge [dist_subtree_thm, node_in_set] @{thm distinct_right}
+ fun distinct_lr node_in_set Left =
+ discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_left}
+ | distinct_lr node_in_set Right =
+ discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_right}
val (swap, neq) =
(case x_rest of
@@ -262,22 +260,24 @@
in
(case xr of
Left =>
- (false, discharge [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right})
+ (false,
+ discharge ctxt [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right})
| Right =>
- (true, discharge [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right}))
+ (true,
+ discharge ctxt [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right}))
end));
- in if swap then discharge [neq] @{thm swap_neq} else neq end;
+ in if swap then discharge ctxt [neq] @{thm swap_neq} else neq end;
-fun deleteProver dist_thm [] = @{thm delete_root} OF [dist_thm]
- | deleteProver dist_thm (p::ps) =
+fun deleteProver _ dist_thm [] = @{thm delete_root} OF [dist_thm]
+ | deleteProver ctxt dist_thm (p::ps) =
let
val dist_rule =
(case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right});
- val dist_thm' = discharge [dist_thm] dist_rule;
+ val dist_thm' = discharge ctxt [dist_thm] dist_rule;
val del_rule = (case p of Left => @{thm delete_left} | Right => @{thm delete_right});
- val del = deleteProver dist_thm' ps;
- in discharge [dist_thm, del] del_rule end;
+ val del = deleteProver ctxt dist_thm' ps;
+ in discharge ctxt [dist_thm, del] del_rule end;
local
val (alpha, v) =
@@ -303,13 +303,13 @@
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
val ps = the (find_tree x (Thm.term_of ct'));
- val del_tree = deleteProver dist_thm ps;
- val dist_thm' = discharge [del_tree, dist_thm] @{thm delete_Some_all_distinct};
+ val del_tree = deleteProver ctxt dist_thm ps;
+ val dist_thm' = discharge ctxt [del_tree, dist_thm] @{thm delete_Some_all_distinct};
val sub_l = subtractProver ctxt (Thm.term_of cl) cl (dist_thm');
val sub_r =
subtractProver ctxt (Thm.term_of cr) cr
- (discharge [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res});
- in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end;
+ (discharge ctxt [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res});
+ in discharge ctxt [del_tree, sub_l, sub_r] @{thm subtract_Node} end;
end;