Separation_Algebra/sep_tactics.ML
changeset 0 1378b654acde
child 25 a5f5b9336007
equal deleted inserted replaced
-1:000000000000 0:1378b654acde
       
     1 (* Title: Tactics for abstract separation algebras
       
     2    Authors: Gerwin Klein and Rafal Kolanski, 2012
       
     3    Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
       
     4                 Rafal Kolanski <rafal.kolanski at nicta.com.au>
       
     5 *)
       
     6 
       
     7 (* Separating Conjunction (and Top, AKA sep_true) {{{
       
     8 
       
     9   This defines all the constants and theorems necessary for the conjunct
       
    10   selection and cancelling tactic, as well as utility functions.
       
    11 *)
       
    12 
       
    13 structure SepConj =
       
    14 struct
       
    15 
       
    16 val sep_conj_term = @{term sep_conj};
       
    17 val sep_conj_str = "**";
       
    18 val sep_conj_ac = @{thms sep_conj_ac};
       
    19 val sep_conj_impl = @{thm sep_conj_impl}
       
    20 
       
    21 fun is_sep_conj_const (Const (@{const_name sep_conj}, _)) = true
       
    22   | is_sep_conj_const _ = false;
       
    23 
       
    24 fun is_sep_conj_term
       
    25       (Const t $ _ $ _ $ _) = is_sep_conj_const (Const t)
       
    26   | is_sep_conj_term _ = false;
       
    27 
       
    28 fun is_sep_conj_prop
       
    29       (Const Trueprop $ t) = is_sep_conj_term t
       
    30   | is_sep_conj_prop _ = false;
       
    31 
       
    32 fun break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2 $ _) =
       
    33   [t1] @ (break_sep_conj t2)
       
    34   | break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2) =
       
    35   [t1] @ (break_sep_conj t2)
       
    36   (* dig through eta exanded terms: *)
       
    37   | break_sep_conj (Abs (_, _, t $ Bound 0)) = break_sep_conj t
       
    38   | break_sep_conj t = [t];
       
    39 
       
    40 fun is_sep_true_term (Abs (_, _, Const (@{const_name True}, _))) = true
       
    41   | is_sep_true_term _ = false;
       
    42 
       
    43 end;
       
    44 
       
    45 (* }}} *)
       
    46 
       
    47 (* Convenience functions for lists {{{ *)
       
    48 structure ListExtra =
       
    49 struct
       
    50 
       
    51 fun init l = List.take (l, List.length l - 1);
       
    52 
       
    53 fun range _ 0 = []
       
    54   | range from howmany = from :: (range (from+1) (howmany-1));
       
    55 
       
    56 (* move nth element in list to the front *)
       
    57 fun nth_to_front i xs =
       
    58       (nth xs i) :: (List.take (xs, i)) @ (List.drop (xs,i+1));
       
    59 
       
    60 (* assign all members of list an index in the list *)
       
    61 fun index_list xs = ListPair.zip (range 0 (length xs), xs);
       
    62 
       
    63 end; (* }}} *)
       
    64 
       
    65 (* Function application terms {{{ *)
       
    66 (* Dealing with function applications of the type
       
    67      Const/Free(name,type) $ arg1 $ arg2 $ ... $ last_arg *)
       
    68 structure FunApp =
       
    69 struct
       
    70 
       
    71 (* apply a transformation to the args in a function application term *)
       
    72 fun app_args_op f t = strip_comb t |> apsnd f |> list_comb;
       
    73 
       
    74 (* remove last argument *)
       
    75 fun app_del_last_arg t = app_args_op ListExtra.init t;
       
    76 
       
    77 (* apply a function term to a Free with given name *)
       
    78 fun fun_app_free t free_name = t $ Free (free_name, type_of t |> domain_type);
       
    79 
       
    80 (* fold two-argument function over a list of arg names using fun_app_free *)
       
    81 fun fun_app_foldr f [a,b] = fun_app_free (fun_app_free f a) b
       
    82   | fun_app_foldr f (x::xs) = (fun_app_free f x) $ (fun_app_foldr f xs)
       
    83   | fun_app_foldr _ _ = raise Fail "fun_app_foldr";
       
    84 
       
    85 end; (* }}} *)
       
    86 
       
    87 (* Selecting Conjuncts in Premise or Conclusion {{{ *)
       
    88 
       
    89 (* Constructs a rearrangement lemma of the kind:
       
    90    (A ** B ** C) s ==> (C ** A ** B) s
       
    91    When cjt_select = 2 (0-based index of C) and
       
    92    cjt_select = 3 (number of conjuncts to use), conclusion = true
       
    93    "conclusion" specifies whether the rearrangement occurs in conclusion
       
    94    (for dtac) or the premise (for rtac) of the rule.
       
    95 *)
       
    96 fun mk_sep_select_rule ctxt conclusion (cjt_count, cjt_select) =
       
    97 let
       
    98   fun variants nctxt names = fold_map Name.variant names nctxt;
       
    99 
       
   100   val (state, nctxt0) = Name.variant "s" (Variable.names_of ctxt);
       
   101   fun sep_conj_prop cjts =
       
   102         FunApp.fun_app_free
       
   103           (FunApp.fun_app_foldr SepConj.sep_conj_term cjts) state
       
   104         |> HOLogic.mk_Trueprop;
       
   105 
       
   106   (* concatenate string and string of an int *)
       
   107   fun conc_str_int str int = str ^ Int.toString int;
       
   108 
       
   109   (* make the conjunct names *)
       
   110   val (cjts, _) = ListExtra.range 1 cjt_count
       
   111                   |> map (conc_str_int "a") |> variants nctxt0;
       
   112 
       
   113   (* make normal-order separation conjunction terms *)
       
   114   val orig = sep_conj_prop cjts;
       
   115 
       
   116   (* make reordered separation conjunction terms *)
       
   117   val reordered = sep_conj_prop (ListExtra.nth_to_front cjt_select cjts);
       
   118 
       
   119   val goal = Logic.mk_implies
       
   120                (if conclusion then (orig, reordered) else (reordered, orig));
       
   121 
       
   122   (* simp add: sep_conj_ac *)
       
   123   val sep_conj_ac_tac = Simplifier.asm_full_simp_tac
       
   124                           (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac);
       
   125 
       
   126 in
       
   127   (* XXX: normally you'd want to keep track of what variables we want to make
       
   128      schematic and which ones are bound, but we don't use fixed names for
       
   129      the rules we make, so we use Drule.export_without_context to schematise
       
   130      all. *)
       
   131   Goal.prove ctxt [] [] goal (fn _ => sep_conj_ac_tac 1)
       
   132   |> Drule.export_without_context
       
   133 end;
       
   134 
       
   135 (* }}} *)
       
   136 
       
   137 local
       
   138   (* Common tactic functionality {{{ *)
       
   139 
       
   140   (* given two terms of some 'a to bool, can you prove
       
   141      \<And>s. t1 s \<Longrightarrow> t2 s
       
   142      using the supplied proof method?
       
   143      NOTE: t1 and t2 MUST have a function type with one argument,
       
   144      or TYPE dest_Type is raised
       
   145      NOTE: if asm or concl is sep_true, returns false
       
   146   *)
       
   147   fun can_prove ctxt tac asm concl =
       
   148     let
       
   149       fun variant name = Name.variant name (Variable.names_of ctxt) |> fst;
       
   150       val arg_name = variant "s";
       
   151       val left = FunApp.fun_app_free asm arg_name |> HOLogic.mk_Trueprop;
       
   152       val right = FunApp.fun_app_free concl arg_name |> HOLogic.mk_Trueprop;
       
   153       val goal = Logic.mk_implies (left, right);
       
   154     in
       
   155       if (SepConj.is_sep_true_term asm) orelse (SepConj.is_sep_true_term concl)
       
   156       then false
       
   157       else (Goal.prove ctxt [] [] goal (fn _ => tac 1); true)
       
   158             handle ERROR _ => false
       
   159     end;
       
   160 
       
   161   (* apply function in list until it returns SOME *)
       
   162   fun find_some (x::xs) f =
       
   163     (case f x of SOME v => SOME v
       
   164                | NONE => find_some xs f)
       
   165     | find_some [] _ = NONE;
       
   166 
       
   167   (* Given indices into the separating conjunctions in the assumption and
       
   168      conclusion, rewrite them so that the targeted conjuncts are at the
       
   169      front, then remove them. *)
       
   170   fun eliminate_target_tac ctxt tac
       
   171                            ((prem_total,prem_idx), (concl_total,concl_idx)) =
       
   172     let
       
   173       val asm_select = mk_sep_select_rule ctxt true (prem_total,prem_idx);
       
   174       val concl_select = mk_sep_select_rule ctxt false
       
   175                            (concl_total,concl_idx);
       
   176     in
       
   177       dtac asm_select THEN' rtac concl_select
       
   178       THEN' etac SepConj.sep_conj_impl THEN' tac
       
   179     end;
       
   180 
       
   181   fun find_target ctxt tac cprem cconcl =
       
   182     let
       
   183       val prem_cjts = cprem |> term_of |> SepConj.break_sep_conj;
       
   184       val concl_cjts = cconcl |> term_of |> SepConj.break_sep_conj;
       
   185 
       
   186       val iprems = ListExtra.index_list prem_cjts;
       
   187       val iconcls = ListExtra.index_list concl_cjts;
       
   188 
       
   189       fun can_prove' (pi,p) (ci,c) =
       
   190             if can_prove ctxt tac p c then SOME (pi, ci) else NONE;
       
   191 
       
   192       val target = find_some iconcls
       
   193                      (fn c => find_some iprems (fn p => can_prove' p c));
       
   194     in
       
   195       case target
       
   196         of SOME (pi,ci) => SOME ((List.length prem_cjts, pi),
       
   197                                  (List.length concl_cjts, ci))
       
   198          | NONE => NONE
       
   199     end;
       
   200 
       
   201   fun strip_cprop ct =
       
   202     let val thy = theory_of_cterm ct
       
   203     in ct |> term_of |> HOLogic.dest_Trueprop |> cterm_of thy
       
   204     end;
       
   205 
       
   206   (* }}} *)
       
   207 in
       
   208 
       
   209   (* Tactic: Select nth conjunct in assumption {{{ *)
       
   210   local
       
   211     fun sep_select_asm_tac' ctxt n (ct, i) =
       
   212       let
       
   213         (* digging out prems *)
       
   214         val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
       
   215         val prems = Drule.strip_imp_prems ct';
       
   216 
       
   217         fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct)
       
   218 
       
   219         fun mk_tac prem =
       
   220             let
       
   221               val prem = HOLogic.dest_Trueprop (term_of prem)
       
   222               val p = length (SepConj.break_sep_conj prem)
       
   223               val th = mk_sep_select_rule ctxt true (p,n)
       
   224                   handle Subscript => error "Conjunct index out of range"
       
   225              in
       
   226                dtac th i
       
   227              end;
       
   228       in
       
   229         if length prems = 0
       
   230         then error ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^
       
   231                     " _) _")
       
   232         else
       
   233           (* backtrack until first premise that does something *)
       
   234           map mk_tac (filter prem_ok prems) |> FIRST
       
   235       end;
       
   236     in
       
   237       fun sep_select_asm_tac ctxt n = CSUBGOAL (sep_select_asm_tac' ctxt (n-1))
       
   238     end; (* }}} *)
       
   239 
       
   240   (* Tactic: Select nth conjunct in conclusion {{{ *)
       
   241   local
       
   242     fun sep_select_tac' ctxt n (ct, i) =
       
   243       let
       
   244         (* digging out conclusions *)
       
   245         val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
       
   246         val concl = ct' |> Drule.strip_imp_concl |> term_of;
       
   247         val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj
       
   248                 |> length;
       
   249         val th = mk_sep_select_rule ctxt false (p,n)
       
   250                  handle Subscript => error "Conjunct index out of range"
       
   251       in
       
   252         if not (SepConj.is_sep_conj_prop concl)
       
   253         then error ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^ " _) _")
       
   254         else rtac th i
       
   255       end;
       
   256   in
       
   257     fun sep_select_tac ctxt n = CSUBGOAL (sep_select_tac' ctxt (n-1))
       
   258   end; (* }}} *)
       
   259 
       
   260   (* Tactic: for all reorderings of the premises try apply tac {{{ *)
       
   261     local
       
   262       fun sep_assm_tac' ctxt tac (ct,i) =
       
   263         let
       
   264           (* digging out prems *)
       
   265           val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
       
   266           val prems = Drule.strip_imp_prems ct';
       
   267 
       
   268           fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct)
       
   269 
       
   270           fun mk_tac prem =
       
   271             let
       
   272               val prem = HOLogic.dest_Trueprop (term_of prem)
       
   273               val p = length (SepConj.break_sep_conj prem)
       
   274               fun ord n = mk_sep_select_rule ctxt true (p,n)
       
   275               val ord_thms = map ord (0 upto p-1)
       
   276             in
       
   277                 (dresolve_tac ord_thms THEN' tac) i
       
   278             end;
       
   279         in
       
   280           (* backtrack until first premise that does something *)
       
   281           map mk_tac (filter prem_ok prems) |> FIRST
       
   282         end;
       
   283     in
       
   284       fun sep_assm_tac ctxt tac = CSUBGOAL (sep_assm_tac' ctxt tac)
       
   285     end; (* }}} *)
       
   286 
       
   287   (* Tactic: for all reorderings of the conclusion, try apply tac {{{ *)
       
   288   local
       
   289     fun sep_concl_tac' ctxt tac (ct, i) =
       
   290       let
       
   291         (* digging out conclusion *)
       
   292         val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
       
   293         val concl = ct' |> Drule.strip_imp_concl |> term_of;
       
   294         val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj
       
   295                 |> length;
       
   296         fun ord n = mk_sep_select_rule ctxt false (p,n);
       
   297         val ord_thms = map ord (0 upto p-1);
       
   298       in
       
   299         if not (SepConj.is_sep_conj_prop concl)
       
   300         then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^
       
   301                       " _) _");
       
   302               no_tac)
       
   303         else (resolve_tac ord_thms THEN' tac) i
       
   304       end;
       
   305   in
       
   306     fun sep_concl_tac ctxt tac = CSUBGOAL (sep_concl_tac' ctxt tac)
       
   307   end; (* }}} *)
       
   308 
       
   309   (* Tactic: Cancel conjuncts of assumption and conclusion via tac {{{ *)
       
   310   local
       
   311     fun sep_cancel_tac' ctxt tac (ct, i) =
       
   312       let
       
   313         (* digging out prems and conclusions *)
       
   314         val ((vars, ct'), ctxt') = Variable.focus_cterm ct ctxt;
       
   315         val concl = Drule.strip_imp_concl ct';
       
   316         val prems = Drule.strip_imp_prems ct';
       
   317 
       
   318         fun prem_ok ct =
       
   319           let
       
   320             (* name of state in sep conj (should be Free after focus) *)
       
   321             fun state_get (_ $ _ $ _ $ s) = s
       
   322               | state_get t = raise Fail "prem_ok: state_get";
       
   323             val state_get_ct = state_get o HOLogic.dest_Trueprop o term_of;
       
   324 
       
   325             val concl_state = concl |> state_get_ct;
       
   326             (* states considered equal if they alpha-convert *)
       
   327             fun state_ok ct = (state_get_ct ct) aconv concl_state;
       
   328           in
       
   329             SepConj.is_sep_conj_prop (term_of ct) andalso state_ok ct
       
   330           end;
       
   331 
       
   332         fun mk_tac prem =
       
   333               case find_target ctxt tac (prem |> strip_cprop)
       
   334                                         (strip_cprop concl)
       
   335                 of SOME target => eliminate_target_tac ctxt tac target i
       
   336                  | NONE => no_tac;
       
   337       in
       
   338         if (not (concl |> term_of |> SepConj.is_sep_conj_prop))
       
   339         then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^
       
   340                        " _) _");
       
   341               no_tac)
       
   342         else if (length prems = 0)
       
   343         then (tracing ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^
       
   344                        " _) _");
       
   345               no_tac)
       
   346         else
       
   347           (* backtrack until first premise that does something *)
       
   348           map mk_tac (filter prem_ok prems) |> FIRST
       
   349       end;
       
   350   in
       
   351     fun sep_cancel_tac ctxt tac = CSUBGOAL (sep_cancel_tac' ctxt tac)
       
   352   end;
       
   353   (* }}} *)
       
   354 
       
   355   (* Derived Tactics *)
       
   356 
       
   357   fun sep_atac ctxt = sep_assm_tac ctxt atac;
       
   358 
       
   359   (* Substitution *)
       
   360   fun sep_subst_tac ctxt occs thms =
       
   361         EqSubst.eqsubst_tac ctxt occs thms THEN' sep_atac ctxt;
       
   362   fun sep_subst_asm_tac ctxt occs thms =
       
   363         EqSubst.eqsubst_asm_tac ctxt occs thms THEN' sep_atac ctxt;
       
   364 
       
   365   (* Forward reasoning *)
       
   366   fun sep_dtac ctxt thms = sep_assm_tac ctxt (dresolve_tac thms)
       
   367   fun sep_ftac ctxt thms = sep_assm_tac ctxt (forward_tac thms)
       
   368 
       
   369   (* Backward reasoning *)
       
   370   fun sep_rtac ctxt thms = sep_concl_tac ctxt (resolve_tac thms)
       
   371 
       
   372 end;
       
   373 
       
   374 (* vim: set foldmethod=marker sw=2 sts=2 et: *)
       
   375