# HG changeset patch # User wenzelm # Date 1320585641 -3600 # Node ID e794026122669305cad12bfb6f7c6352b69e79d7 # Parent c0704e988526e2e52113b892e9c6292300d10368 inlined antiquotations; diff -r c0704e988526 -r e79402612266 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sun Nov 06 14:09:24 2011 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Nov 06 14:20:41 2011 +0100 @@ -24,18 +24,7 @@ structure DistinctTreeProver : DISTINCT_TREE_PROVER = struct -val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left}; -val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right}; - -val distinct_left = @{thm DistinctTreeProver.distinct_left}; -val distinct_right = @{thm DistinctTreeProver.distinct_right}; -val distinct_left_right = @{thm DistinctTreeProver.distinct_left_right}; -val in_set_root = @{thm DistinctTreeProver.in_set_root}; -val in_set_left = @{thm DistinctTreeProver.in_set_left}; -val in_set_right = @{thm DistinctTreeProver.in_set_right}; - -val swap_neq = @{thm DistinctTreeProver.swap_neq}; -val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False}; +val neq_to_eq_False = @{thm neq_to_eq_False}; datatype direction = Left | Right; @@ -180,7 +169,7 @@ val (l_in_set_root, x_in_set_root, r_in_set_root) = let val (Node_l_x_d, r) = - cprop_of in_set_root + cprop_of @{thm in_set_root} |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb; @@ -190,7 +179,7 @@ val (x_in_set_left, r_in_set_left) = let val (Node_l_x_d, r) = - cprop_of in_set_left + cprop_of @{thm in_set_left} |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2; @@ -199,7 +188,7 @@ val (x_in_set_right, l_in_set_right) = let val (Node_l, x) = - cprop_of in_set_right + cprop_of @{thm in_set_right} |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 @@ -221,7 +210,8 @@ fun dist_subtree [] thm = thm | dist_subtree (p :: ps) thm = let - val rule = (case p of Left => all_distinct_left | Right => all_distinct_right) + val rule = + (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}) in dist_subtree ps (discharge [thm] rule) end; val (ps, x_rest, y_rest) = split_common_prefix x_path y_path; @@ -238,14 +228,14 @@ [] => instantiate [(ctyp_of_term x_in_set_root, xT)] - [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] in_set_root + [(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 [(ctyp_of_term x_in_set_left, xT)] - [(x_in_set_left, x), (r_in_set_left, r)] in_set_left; + [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left}; in discharge [in_set_l] in_set_left' end | Right :: ps' => let @@ -253,7 +243,7 @@ val in_set_right' = instantiate [(ctyp_of_term x_in_set_right, xT)] - [(x_in_set_right, x), (l_in_set_right, l)] in_set_right; + [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right}; in discharge [in_set_r] in_set_right' end) end; @@ -261,8 +251,8 @@ | 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] distinct_left - | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right + 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} val (swap, neq) = (case x_rest of @@ -280,35 +270,29 @@ val y_in_set = in_set' y_rest; in (case xr of - Left => (false, discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right) - | Right => (true, discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right)) + Left => + (false, discharge [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})) end)); - in if swap then discharge [neq] swap_neq else neq end; + in if swap then discharge [neq] @{thm swap_neq} else neq end; -val delete_root = @{thm delete_root}; -val delete_left = @{thm delete_left}; -val delete_right = @{thm delete_right}; - -fun deleteProver dist_thm [] = delete_root OF [dist_thm] +fun deleteProver dist_thm [] = @{thm delete_root} OF [dist_thm] | deleteProver dist_thm (p::ps) = let - val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right); + 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 del_rule = (case p of Left => delete_left | Right => delete_right); + 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 subtract_Tip = @{thm subtract_Tip}; -val subtract_Node = @{thm subtract_Node}; -val delete_Some_all_distinct = @{thm delete_Some_all_distinct}; -val subtract_Some_all_distinct_res = @{thm subtract_Some_all_distinct_res}; - local val (alpha, v) = let val ct = - subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 + @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp; in (alpha, #1 (dest_Var (term_of ct))) end; @@ -322,7 +306,7 @@ in Thm.instantiate ([(alpha, ctyp_of thy alphaI)], - [(cterm_of thy (Var (v, treeT alphaI)), ct')]) subtract_Tip + [(cterm_of thy (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip} end | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm = let @@ -330,22 +314,20 @@ val (_, [cl, _, _, cr]) = Drule.strip_comb ct; val ps = the (find_tree x (term_of ct')); val del_tree = deleteProver dist_thm ps; - val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; + val dist_thm' = discharge [del_tree, dist_thm] @{thm delete_Some_all_distinct}; val sub_l = subtractProver (term_of cl) cl (dist_thm'); val sub_r = subtractProver (term_of cr) cr - (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res); - in discharge [del_tree, sub_l, sub_r] subtract_Node end; + (discharge [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res}); + in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end; end; -val subtract_Some_all_distinct = @{thm subtract_Some_all_distinct}; - fun distinct_implProver dist_thm ct = let val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val sub = subtractProver (term_of ctree) ctree dist_thm; - in subtract_Some_all_distinct OF [sub, dist_thm] end; + in @{thm subtract_Some_all_distinct} OF [sub, dist_thm] end; fun get_fst_success f [] = NONE | get_fst_success f (x :: xs) = @@ -381,7 +363,7 @@ (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) => (case try Simplifier.the_context ss of SOME ctxt => - Option.map (fn neq => neq_to_eq_False OF [neq]) + Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) (get_fst_success (neq_x_y ctxt x y) names) | NONE => NONE));