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