1(*
2 * Copyright 2014, 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
11(*
12 * Tactic for solving monadic equalities, such as:
13 *
14 * (liftE (return 3) = returnOk 3
15 *
16 * Theorems of the form:
17 *
18 *   ((a, s') \<in> fst (A s)) = P a s s'
19 *
20 * and
21 *
22 *   snd (A s) = P s
23 *
24 * are added to the "monad_eq" set.
25 *)
26theory MonadEq
27imports "Monad_WP/NonDetMonadVCG"
28begin
29
30(* Setup "monad_eq" attributes. *)
31ML {*
32structure MonadEqThms = Named_Thms (
33    val name = Binding.name "monad_eq"
34    val description = "monad equality-prover theorems"
35    )
36*}
37attribute_setup monad_eq = {*
38  Attrib.add_del
39    (Thm.declaration_attribute MonadEqThms.add_thm)
40    (Thm.declaration_attribute MonadEqThms.del_thm) *}
41  "Monad equality-prover theorems"
42
43(* Setup tactic. *)
44
45ML {*
46fun monad_eq_tac ctxt =
47let
48  (* Set a simpset as being hidden, so warnings are not printed from it. *)
49  val ctxt' = Context_Position.set_visible false ctxt
50in
51  CHANGED (clarsimp_tac (ctxt' addsimps (MonadEqThms.get ctxt')) 1)
52end
53*}
54
55method_setup monad_eq = {*
56    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD o monad_eq_tac)) *}
57  "prove equality on monads"
58
59lemma monad_eq_simp_state [monad_eq]:
60  "((A :: ('s, 'a) nondet_monad) s = B s') =
61      ((\<forall>r t. (r, t) \<in> fst (A s) \<longrightarrow> (r, t) \<in> fst (B s'))
62         \<and> (\<forall>r t. (r, t) \<in> fst (B s') \<longrightarrow> (r, t) \<in> fst (A s))
63         \<and> (snd (A s) = snd (B s')))"
64  apply (auto intro!: set_eqI prod_eqI)
65  done
66
67lemma monad_eq_simp [monad_eq]:
68  "((A :: ('s, 'a) nondet_monad) = B) =
69      ((\<forall>r t s. (r, t) \<in> fst (A s) \<longrightarrow> (r, t) \<in> fst (B s))
70         \<and> (\<forall>r t s. (r, t) \<in> fst (B s) \<longrightarrow> (r, t) \<in> fst (A s))
71         \<and> (\<forall>x. snd (A x) = snd (B x)))"
72  apply (auto intro!: set_eqI prod_eqI)
73  done
74
75declare in_monad [monad_eq]
76declare in_bindE [monad_eq]
77
78(* Test *)
79lemma "returnOk 3 = liftE (return 3)"
80  apply monad_eq
81  oops
82
83end
84