1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Title: Tactics for abstract separation algebras 8 Authors: Gerwin Klein and Rafal Kolanski, 2012 9 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 10 Rafal Kolanski <rafal.kolanski at nicta.com.au> 11*) 12 13(* Separating Conjunction (and Top, AKA sep_true) {{{ 14 15 This defines the constants and theorems necessary for the conjunct 16 selection and cancelling tactic, as well as utility functions. 17*) 18 19structure SepConj = 20struct 21 22val sep_conj_term = @{term sep_conj} 23val sep_conj_str = "**" 24val sep_conj_ac = @{thms sep_conj_ac} 25val sep_conj_impl = @{thm sep_conj_impl} 26 27fun is_sep_conj_const (Const (@{const_name sep_conj}, _)) = true 28 | is_sep_conj_const _ = false 29 30fun is_sep_conj_term (Const t $ _ $ _ $ _) = is_sep_conj_const (Const t) 31 | is_sep_conj_term _ = false 32 33fun is_sep_conj_prop (Const _ $ t) = is_sep_conj_term t 34 | is_sep_conj_prop _ = false 35 36fun strip_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2 $ _) = 37 [t1] @ (strip_sep_conj t2) 38 | strip_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2) = 39 [t1] @ (strip_sep_conj t2) 40 (* dig through eta exanded terms: *) 41 | strip_sep_conj (Abs (_, _, t $ Bound 0)) = strip_sep_conj t 42 | strip_sep_conj t = [t] 43 44fun is_sep_true_term (Abs (_, _, Const (@{const_name True}, _))) = true 45 | is_sep_true_term _ = false 46 47fun mk_sep_conj (t1, t2) = sep_conj_term $ t1 $ t2 48 49(* Types of conjuncts and name of state type, for term construction *) 50val sep_conj_cjt_typ = type_of sep_conj_term |> domain_type 51val sep_conj_state_typn = domain_type sep_conj_cjt_typ |> dest_TFree |> #1 52 53end 54 55(* }}} *) 56 57(* Function application terms {{{ *) 58(* Dealing with function applications of the type 59 Const/Free(name,type) $ arg1 $ arg2 $ ... $ last_arg *) 60structure FunApp = 61struct 62 63(* apply a function term to a Free with given name *) 64fun fun_app_free t free_name = t $ Free (free_name, type_of t |> domain_type) 65 66end (* }}} *) 67 68(* Selecting Conjuncts in Premise or Conclusion {{{ *) 69 70(* Constructs a rearrangement lemma of the kind: 71 (A ** B ** C) s ==> (C ** A ** B) s 72 When cjt_select = 2 (0-based index of C) and 73 cjt_select = 3 (number of conjuncts to use), conclusion = true 74 "conclusion" specifies whether the rearrangement occurs in conclusion 75 (for dtac) or the premise (for rtac) of the rule. 76*) 77 78fun mk_sep_select_rule ctxt conclusion (cjt_count, cjt_selects) = 79let 80 fun variants nctxt names = fold_map Name.variant names nctxt 81 val (state, nctxt0) = Name.variant "s" (Variable.names_of ctxt) 82 fun mk_cjt n = Free (n, type_of SepConj.sep_conj_term |> domain_type) 83 fun sep_conj_prop cjts = 84 FunApp.fun_app_free (foldr1 SepConj.mk_sep_conj (map mk_cjt cjts)) state |> HOLogic.mk_Trueprop 85 (* concatenate string and string of an int *) 86 fun conc_str_int str int = str ^ Int.toString int 87 (* make the conjunct names *) 88 val (cjts, _) = 1 upto cjt_count |> map (conc_str_int "a") |> variants nctxt0 89 (* make normal-order separation conjunction terms *) 90 val orig = sep_conj_prop cjts 91 92 (* make reordered separation conjunction terms *) 93 94 (* We gather the needed conjuncts, and then append it the original list with those conjuncts removed *) 95 fun dropit n (x::xs) is = if exists (fn y => y = n) is then dropit (n+1) xs is else x :: dropit (n+1) xs is 96 | dropit _ [] _ = [] 97 98 fun nths_to_front idxs xs = map (nth xs) idxs @ dropit 0 xs idxs 99 val reordered = sep_conj_prop (nths_to_front cjt_selects cjts) 100 val goal = Logic.mk_implies (if conclusion then (orig, reordered) else (reordered, orig)) 101 102 (* simp add: sep_conj_ac *) 103 val sep_conj_ac_tac = Simplifier.asm_full_simp_tac 104 (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac) 105 106in 107 Goal.prove ctxt [] [] goal (fn _ => sep_conj_ac_tac 1) 108 |> Drule.generalize ([SepConj.sep_conj_state_typn], state :: cjts) 109end 110 111fun conj_length ctxt ct = 112let 113 val ((_, ct'), _) = Variable.focus_cterm NONE ct ctxt 114 val concl = ct' |> Drule.strip_imp_concl |> Thm.term_of 115in 116 concl |> HOLogic.dest_Trueprop |> SepConj.strip_sep_conj |> length 117end 118 119local 120 fun all_uniq xs = forall (fn x => length (filter (fn y => x = y) xs) = 1 ) xs 121in 122 fun sep_selects_tac ctxt ns = 123 let 124 fun sep_select_tac' ctxt ns (ct, i) = 125 let 126 fun th ns = mk_sep_select_rule ctxt false ((conj_length ctxt ct),ns) 127 in 128 if not (all_uniq ns) 129 then error ("Duplicate numbers in arguments") 130 else resolve0_tac [th ns] i handle Subscript => no_tac 131 end 132 in 133 CSUBGOAL (sep_select_tac' ctxt (map (fn m => m - 1) ns)) 134 end 135end 136 137fun UNSOLVED' tac i st = 138 tac i st |> Seq.filter (fn st' => Thm.nprems_of st' = Thm.nprems_of st) 139 140fun sep_flatten ctxt = 141let 142 fun simptac i = 143 CHANGED_PROP (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm sep_conj_assoc}]) i) 144in 145 UNSOLVED' simptac 146end 147 148fun sep_select_tactic lens_tac ns ctxt = 149let 150 val sep_select = sep_selects_tac ctxt 151 val iffI = @{thm iffI} 152 val sep_conj_ac_tac = 153 Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac) 154in 155 lens_tac THEN' 156 resolve0_tac [iffI] THEN' 157 sep_select ns THEN' 158 assume_tac ctxt THEN' 159 sep_conj_ac_tac 160end 161