1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory SimpStrategy
8imports Main
9begin
10
11text \<open>
12Support for defining alternative simplifier strategies for some parts of terms
13or some premises of rewrite rules. The "name" parameter to the simp_strategy
14constant is used to identify which simplification strategy should be used on
15this term. Note that, although names have type nat, it is safe for them to all
16be defined as 0. The important thing is that the simplifier doesn't know they're
17equal.
18\<close>
19
20definition
21  simp_strategy :: "nat \<Rightarrow> ('a :: {}) \<Rightarrow> 'a"
22where
23  "simp_strategy name x \<equiv> x"
24
25text \<open>
26This congruence rule forbids the simplifier from simplifying the arguments of
27simp_strategy normally.
28\<close>
29
30lemma simp_strategy_cong[cong]:
31  "simp_strategy name x = simp_strategy name x"
32  by simp
33
34text \<open>
35This strategy, or rather lack thereof, can be used to forbid simplification.
36\<close>
37
38definition
39  NoSimp :: nat
40where "NoSimp = 0"
41
42text \<open>
43This strategy indicates that a boolean subterm should be simplified only by
44using explicit assumptions of the simpset.
45\<close>
46
47definition
48  ByAssum :: nat
49where "ByAssum = 0"
50
51lemma Eq_TrueI_ByAssum:
52  "P \<Longrightarrow> simp_strategy ByAssum P \<equiv> True"
53  by (simp add: simp_strategy_def)
54
55simproc_setup simp_strategy_ByAssum ("simp_strategy ByAssum b") =
56  \<open>K (fn ss => fn ct => let
57      val b = Thm.dest_arg ct
58      val t = Thm.instantiate ([],[((("P",0),@{typ bool}), b)])
59        @{thm Eq_TrueI_ByAssum}
60      val prems = Raw_Simplifier.prems_of ss
61    in get_first (try (fn p => p RS t)) prems end)\<close>
62
63lemma ByAssum:
64  "simp_strategy ByAssum P \<Longrightarrow> P"
65  by (simp add: simp_strategy_def)
66
67lemma simp_ByAssum_test:
68  "P \<Longrightarrow> simp_strategy ByAssum P"
69  by simp
70
71text \<open>
72Generic framework for instantiating a simproc which simplifies within a
73simp_strategy with a given simpset.
74
75The boolean determines whether simp_strategy Name True should be rewritten
76to True.
77\<close>
78
79lemma simp_strategy_Eq_True:
80  "simp_strategy name True \<equiv> True"
81  by (simp add: simp_strategy_def)
82
83ML \<open>
84fun simp_strategy_True_conv ct = case Thm.term_of ct of
85    (Const (@{const_name simp_strategy}, _) $ _ $ @{term True})
86      => Thm.instantiate ([], [((("name",0), @{typ nat}), Thm.dest_arg1 ct)])
87          @{thm simp_strategy_Eq_True}
88  | _ => Conv.all_conv ct
89
90fun new_simp_strategy thy (name : term) ss rewr_True =
91let
92  val ctxt = Proof_Context.init_global thy;
93  val ss = Simplifier.make_simproc ctxt ("simp_strategy_" ^ fst (dest_Const name))
94    {lhss = [@{term simp_strategy} $ name $ @{term x}],
95     proc = (fn _ => fn ctxt' => fn ct =>
96        ct
97        |> (Conv.arg_conv (Simplifier.rewrite (put_simpset ss ctxt'))
98          then_conv (if rewr_True then simp_strategy_True_conv
99                      else Conv.all_conv))
100        |> (fn c => if Thm.is_reflexive c then NONE else SOME c))
101     }
102in
103  ss
104end
105\<close>
106
107end
108