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