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