1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Value_Abbreviation 8 9imports Main 10 11keywords "value_abbreviation" :: thy_decl 12 13begin 14 15text \<open>Computing values and saving as abbreviations. 16 17Useful in program verification to handle some configuration constant 18(e.g. n = 4) which may change. This mechanism can be used to give 19names (abbreviations) to other related constants (e.g. 2 ^ n, 2 ^ n - 1, 20[1 .. n], rev [1 .. n]) which may appear repeatedly. 21\<close> 22 23ML \<open> 24structure Value_Abbreviation = struct 25fun value_and_abbreviation mode name expr int ctxt = let 26 val decl = (name, NONE, Mixfix.NoSyn) 27 val expr = Syntax.read_term ctxt expr 28 val eval_expr =Value_Command.value ctxt expr 29 val lhs = Free (Binding.name_of name, fastype_of expr) 30 val eq = Logic.mk_equals (lhs, eval_expr) 31 val ctxt = Specification.abbreviation mode (SOME decl) [] eq int ctxt 32 val pretty_eq = Syntax.pretty_term ctxt eq 33 in Pretty.writeln pretty_eq; ctxt end 34 35val _ = 36 Outer_Syntax.local_theory' @{command_keyword value_abbreviation} 37 "setup abbreviation for evaluated value" 38 (Parse.syntax_mode -- Parse.binding -- Parse.term 39 >> (fn ((mode, name), expr) => value_and_abbreviation mode name expr)); 40 41end 42\<close> 43 44text \<open>Testing it out. 45Unfortunately locale/experiment/notepad all won't work here because 46the code equation setup is all global. 47\<close> 48 49definition 50 "value_abbreviation_test_config_constant_1 = (24 :: nat)" 51 52definition 53 "value_abbreviation_test_config_constant_2 = (5 :: nat)" 54 55value_abbreviation (input) 56 value_abbreviation_test_important_magic_number 57 "((2 :: int) ^ value_abbreviation_test_config_constant_1) 58 - (2 ^ value_abbreviation_test_config_constant_2)" 59 60value_abbreviation (input) 61 value_abbreviation_test_range_of_options 62 "rev [int value_abbreviation_test_config_constant_2 63 .. int value_abbreviation_test_config_constant_1]" 64 65end 66