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