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