1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory AddUpdSimps 8 9imports Main 10keywords "add_upd_simps" :: thy_decl 11 12begin 13 14ML \<open> 15fun mk_var_app nm (f $ _) = let 16 val (_, xs) = strip_comb f 17 val n = length xs 18 val T = domain_type (fastype_of f) 19 in mk_var_app nm f $ Free (nm ^ string_of_int n, T) end 20 | mk_var_app _ t = t 21 22fun get_upd_apps (f $ (g $ x)) = if 23 is_Const (head_of f) andalso is_Const (head_of g) 24 andalso domain_type (fastype_of g) = range_type (fastype_of g) 25 then mk_var_app "x" f $ (mk_var_app "y" (g $ x)) 26 :: get_upd_apps f @ get_upd_apps (g $ x) 27 else get_upd_apps f @ get_upd_apps (g $ x) 28 | get_upd_apps (f $ x) = get_upd_apps f @ get_upd_apps x 29 | get_upd_apps (Abs (_, _, t)) = get_upd_apps t 30 | get_upd_apps _ = [] 31 32fun mk_upd_simps ctxt upd_app (simps, done, n) = let 33 val n = n + 1 34 val _ = n <= 5000 orelse raise TERM ("mk_upd_simps: 5000", [upd_app]) 35 val (nm, _) = dest_Const (head_of upd_app) 36 val def = Proof_Context.get_thm ctxt (nm ^ "_def") 37 val rhs = case (mk_var_app "x" upd_app, upd_app) 38 of (f $ _, _ $ (_ $ x)) => f $ x 39 | _ => raise TERM ("mk_upd_simps: impossible", [upd_app]) 40 val prop = HOLogic.mk_eq (upd_app, rhs) |> HOLogic.mk_Trueprop 41 val thm = Thm.trivial (Thm.cterm_of ctxt prop) 42 |> simp_tac (ctxt addsimps [def, @{thm fun_eq_iff}] addsimps simps) 1 43 |> Seq.hd 44 val upd_apps_prem = Thm.prems_of thm |> maps get_upd_apps 45 |> sort_distinct Term_Ord.fast_term_ord 46 |> filter_out (Termtab.defined done) 47 |> filter_out (curry (op =) upd_app) 48 |> filter_out (head_of #> dest_Const #> fst #> String.isPrefix "HOL.") 49 val (simps2, done, n) = fold (mk_upd_simps ctxt) 50 upd_apps_prem (simps, done, n) 51 val thm = Drule.export_without_context thm 52 in if length simps2 <> length simps 53 then mk_upd_simps ctxt upd_app (simps2, done, n) 54 else (if Thm.nprems_of thm = 0 then thm :: simps2 else simps2, 55 Termtab.update (upd_app, ()) done, n) 56 end 57 handle ERROR _ => (warning (fst (dest_Const (head_of upd_app)) ^ ": no def."); 58 (simps, done, n)) 59 60fun mk_upd_simps_tm ctxt t = let 61 val uas = get_upd_apps t |> sort_distinct Term_Ord.fast_term_ord 62 val (simps, _, _) = fold (mk_upd_simps ctxt) uas ([], Termtab.empty, 0) 63 in simps end 64 65fun add_upd_simps t exsimps ctxt = let 66 val thms = mk_upd_simps_tm (ctxt addsimps exsimps) t 67 val _ = map (Thm.pretty_thm ctxt #> Pretty.writeln) thms 68 in if null thms then ctxt 69 else (Local_Theory.notes [((@{binding upd_simps}, []), [(thms, [])])] ctxt |> #2) addsimps thms 70 end 71 72val add_upd_simps_syn = Outer_Syntax.local_theory @{command_keyword "add_upd_simps"} 73 "recursively show updates don't matter to constants" 74 (Parse.term -- Scan.optional 75 (Parse.$$$ "(" |-- Scan.repeat Parse.thm --| Parse.$$$ ")") [] 76 >> (fn (t, simps) => fn ctxt => add_upd_simps (Syntax.read_term ctxt t) 77 (Attrib.eval_thms ctxt simps) ctxt)) 78\<close> 79 80end 81