1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(*
12 * This file introduces an experimental "distinct" command that takes
13 * a list of 'n' terms, and generates O(n^2) lemmas for you to prove
14 * that the 'n' terms are all distinct. These proofs can typically be
15 * carried out by an "apply auto" command, giving you O(n^2)
16 * distinctness theorems relatively easily. These new theorems can then
17 * be thrown into a simpset to avoid having to constantly unfold
18 * definitions merely to prove distinctness.
19 *
20 * This may significantly simplify certain proofs where inequality of
21 * defined terms is frequently relied upon.
22 *
23 * The "distinct" command is not really scalable, due to its O(n^2)
24 * proof terms generated. If we wanted to use this in a larger example,
25 * we would probably want a "ordered" command, which forces you to show
26 * that 'n' terms have some ordering, and then automatically derive the
27 * O(n^2) possible proof terms on-the-fly in a simproc (possibly using
28 * Isabelle's existing "order_tac").
29 *)
30theory Distinct_Cmd
31imports Main
32  keywords "distinct" :: thy_goal
33begin
34
35ML {*
36local
37
38(*
39 * Process a parsed binding, converting it from raw tokens (which
40 * can't be passed into Local_Theory.note) into its semantic meaning
41 * (which can).
42 *)
43fun process_binding lthy binding =
44  apsnd (map (Attrib.check_src lthy)) binding
45
46(* Parse the parameters to "distinct". *)
47val distinct_parser =
48  (Scan.optional (Parse_Spec.opt_thm_name ":") Binding.empty_atts
49         -- Scan.repeat1 Parse.term)
50
51(* Generate a prop of the form "a ~= b". *)
52fun mk_inequality_pair a b =
53  HOLogic.mk_eq (a, b)
54  |> HOLogic.mk_not
55  |> HOLogic.mk_Trueprop
56
57(* Generate O(n^2) distinctness goals. *)
58fun gen_distinct_goals terms =
59  map_product
60    (fn a => fn b =>
61        if a = b then NONE
62        else SOME (mk_inequality_pair a b))
63    terms terms
64  |> map_filter I
65  |> map (fn t => (t, []))
66
67(* Given a list of terms, coerce them all into the same type. *)
68fun coerce_terms_to_same_type lthy terms =
69  HOLogic.mk_list dummyT terms
70  |> Syntax.check_term lthy
71  |> HOLogic.dest_list
72
73(* We save the theorems to the context afterwards. *)
74fun after_qed thm_name thms lthy =
75  Local_Theory.note (thm_name, (flat thms)) lthy |> snd
76
77in
78
79val _ =
80   Outer_Syntax.local_theory_to_proof @{command_keyword "distinct"}
81      "prove distinctness of a list of terms"
82      (distinct_parser
83        >> (fn (thm_name, terms) => fn lthy =>
84              Proof.theorem NONE (after_qed (process_binding lthy thm_name)) [
85                  map (Syntax.parse_term lthy) terms
86                  |> coerce_terms_to_same_type lthy
87                  |> gen_distinct_goals
88              ] lthy
89            ))
90
91end
92*}
93
94(* Test. *)
95context
96  fixes A :: nat
97  fixes B :: nat
98  fixes C :: nat
99  assumes x: "A = 1 \<and> B = 2 \<and> C = 3"
100begin
101
102distinct A B C "5" "6" "2 + 11"
103  by (auto simp: x)
104
105end
106
107end
108