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