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