# HG changeset patch # User wenzelm # Date 1433158356 -7200 # Node ID a3f565b8ba767d2fd9e915f2c1ff5e3c706d9f99 # Parent 68699e576d515fefbd2b0e5c032ee9194d94850a clarified context; diff -r 68699e576d51 -r a3f565b8ba76 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Mon Jun 01 11:47:25 2015 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Jun 01 13:32:36 2015 +0200 @@ -10,12 +10,12 @@ val find_tree : term -> term -> direction list option val neq_to_eq_False : thm - val distinctTreeProver : thm -> direction list -> direction list -> thm + val distinctTreeProver : Proof.context -> thm -> direction list -> direction list -> thm val neq_x_y : Proof.context -> term -> term -> string -> thm option val distinctFieldSolver : string list -> solver val distinctTree_tac : string list -> Proof.context -> int -> tactic - val distinct_implProver : thm -> cterm -> thm - val subtractProver : term -> cterm -> thm -> thm + val distinct_implProver : Proof.context -> thm -> cterm -> thm + val subtractProver : Proof.context -> term -> cterm -> thm -> thm val distinct_simproc : string list -> simproc val discharge : thm list -> thm -> thm @@ -88,14 +88,12 @@ (* Wrapper around Thm.instantiate. The type instiations of instTs are applied to * the right hand sides of insts *) -fun instantiate instTs insts = +fun instantiate ctxt instTs insts = let val instTs' = map (fn (T, U) => (dest_TVar (Thm.typ_of T), Thm.typ_of U)) instTs; fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T'); fun mapT_and_recertify ct = - let - val thy = Thm.theory_of_cterm ct; - in (Thm.global_cterm_of thy (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))) end; + (Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))); val insts' = map (apfst mapT_and_recertify) insts; in Thm.instantiate (instTs, insts') end; @@ -198,7 +196,7 @@ otherwise all_distinct_left_right *) -fun distinctTreeProver dist_thm x_path y_path = +fun distinctTreeProver ctxt dist_thm x_path y_path = let fun dist_subtree [] thm = thm | dist_subtree (p :: ps) thm = @@ -219,14 +217,14 @@ in (case ps of [] => - instantiate + instantiate ctxt [(Thm.ctyp_of_cterm x_in_set_root, xT)] [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root} | Left :: ps' => let val in_set_l = in_set ps' l; val in_set_left' = - instantiate + 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 @@ -234,7 +232,7 @@ let val in_set_r = in_set ps' r; val in_set_right' = - instantiate + 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) @@ -291,35 +289,34 @@ in (alpha, #1 (dest_Var (Thm.term_of ct))) end; in -fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm = +fun subtractProver ctxt (Const (@{const_name Tip}, T)) ct dist_thm = let val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; - val thy = Thm.theory_of_cterm ct; val [alphaI] = #2 (dest_Type T); in Thm.instantiate - ([(alpha, Thm.global_ctyp_of thy alphaI)], - [(Thm.global_cterm_of thy (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip} + ([(alpha, Thm.ctyp_of ctxt alphaI)], + [(Thm.cterm_of ctxt (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip} end - | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm = + | subtractProver ctxt (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm = let 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 sub_l = subtractProver (Thm.term_of cl) cl (dist_thm'); + val sub_l = subtractProver ctxt (Thm.term_of cl) cl (dist_thm'); val sub_r = - subtractProver (Thm.term_of cr) cr + 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; end; -fun distinct_implProver dist_thm ct = +fun distinct_implProver ctxt dist_thm ct = let val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; - val sub = subtractProver (Thm.term_of ctree) ctree dist_thm; + val sub = subtractProver ctxt (Thm.term_of ctree) ctree dist_thm; in @{thm subtract_Some_all_distinct} OF [sub, dist_thm] end; fun get_fst_success f [] = NONE @@ -335,7 +332,7 @@ val tree = Thm.term_of ctree; val x_path = the (find_tree x tree); val y_path = the (find_tree y tree); - val thm = distinctTreeProver dist_thm x_path y_path; + val thm = distinctTreeProver ctxt dist_thm x_path y_path; in SOME thm end handle Option.Option => NONE); diff -r 68699e576d51 -r a3f565b8ba76 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Mon Jun 01 11:47:25 2015 +0200 +++ b/src/HOL/Statespace/state_space.ML Mon Jun 01 13:32:36 2015 +0200 @@ -194,7 +194,7 @@ val tree = Thm.term_of ctree; val x_path = the (DistinctTreeProver.find_tree x tree); val y_path = the (DistinctTreeProver.find_tree y tree); - val thm = DistinctTreeProver.distinctTreeProver dist_thm x_path y_path; + val thm = DistinctTreeProver.distinctTreeProver ctxt dist_thm x_path y_path; in SOME thm end handle Option.Option => NONE) @@ -221,7 +221,7 @@ fun solve_tac ctxt = CSUBGOAL (fn (goal, i) => let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; - val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; + val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal; in rtac rule i end); fun tac ctxt =