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