--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/sep_tactics.ML Thu Mar 06 13:28:38 2014 +0000
@@ -0,0 +1,375 @@
+(* Title: Tactics for abstract separation algebras
+ Authors: Gerwin Klein and Rafal Kolanski, 2012
+ Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+ Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+(* Separating Conjunction (and Top, AKA sep_true) {{{
+
+ This defines all the constants and theorems necessary for the conjunct
+ selection and cancelling tactic, as well as utility functions.
+*)
+
+structure SepConj =
+struct
+
+val sep_conj_term = @{term sep_conj};
+val sep_conj_str = "**";
+val sep_conj_ac = @{thms sep_conj_ac};
+val sep_conj_impl = @{thm sep_conj_impl}
+
+fun is_sep_conj_const (Const (@{const_name sep_conj}, _)) = true
+ | is_sep_conj_const _ = false;
+
+fun is_sep_conj_term
+ (Const t $ _ $ _ $ _) = is_sep_conj_const (Const t)
+ | is_sep_conj_term _ = false;
+
+fun is_sep_conj_prop
+ (Const Trueprop $ t) = is_sep_conj_term t
+ | is_sep_conj_prop _ = false;
+
+fun break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2 $ _) =
+ [t1] @ (break_sep_conj t2)
+ | break_sep_conj (Const (@{const_name sep_conj},_) $ t1 $ t2) =
+ [t1] @ (break_sep_conj t2)
+ (* dig through eta exanded terms: *)
+ | break_sep_conj (Abs (_, _, t $ Bound 0)) = break_sep_conj t
+ | break_sep_conj t = [t];
+
+fun is_sep_true_term (Abs (_, _, Const (@{const_name True}, _))) = true
+ | is_sep_true_term _ = false;
+
+end;
+
+(* }}} *)
+
+(* Convenience functions for lists {{{ *)
+structure ListExtra =
+struct
+
+fun init l = List.take (l, List.length l - 1);
+
+fun range _ 0 = []
+ | range from howmany = from :: (range (from+1) (howmany-1));
+
+(* move nth element in list to the front *)
+fun nth_to_front i xs =
+ (nth xs i) :: (List.take (xs, i)) @ (List.drop (xs,i+1));
+
+(* assign all members of list an index in the list *)
+fun index_list xs = ListPair.zip (range 0 (length xs), xs);
+
+end; (* }}} *)
+
+(* Function application terms {{{ *)
+(* Dealing with function applications of the type
+ Const/Free(name,type) $ arg1 $ arg2 $ ... $ last_arg *)
+structure FunApp =
+struct
+
+(* apply a transformation to the args in a function application term *)
+fun app_args_op f t = strip_comb t |> apsnd f |> list_comb;
+
+(* remove last argument *)
+fun app_del_last_arg t = app_args_op ListExtra.init t;
+
+(* apply a function term to a Free with given name *)
+fun fun_app_free t free_name = t $ Free (free_name, type_of t |> domain_type);
+
+(* fold two-argument function over a list of arg names using fun_app_free *)
+fun fun_app_foldr f [a,b] = fun_app_free (fun_app_free f a) b
+ | fun_app_foldr f (x::xs) = (fun_app_free f x) $ (fun_app_foldr f xs)
+ | fun_app_foldr _ _ = raise Fail "fun_app_foldr";
+
+end; (* }}} *)
+
+(* Selecting Conjuncts in Premise or Conclusion {{{ *)
+
+(* Constructs a rearrangement lemma of the kind:
+ (A ** B ** C) s ==> (C ** A ** B) s
+ When cjt_select = 2 (0-based index of C) and
+ cjt_select = 3 (number of conjuncts to use), conclusion = true
+ "conclusion" specifies whether the rearrangement occurs in conclusion
+ (for dtac) or the premise (for rtac) of the rule.
+*)
+fun mk_sep_select_rule ctxt conclusion (cjt_count, cjt_select) =
+let
+ fun variants nctxt names = fold_map Name.variant names nctxt;
+
+ val (state, nctxt0) = Name.variant "s" (Variable.names_of ctxt);
+ fun sep_conj_prop cjts =
+ FunApp.fun_app_free
+ (FunApp.fun_app_foldr SepConj.sep_conj_term cjts) state
+ |> HOLogic.mk_Trueprop;
+
+ (* concatenate string and string of an int *)
+ fun conc_str_int str int = str ^ Int.toString int;
+
+ (* make the conjunct names *)
+ val (cjts, _) = ListExtra.range 1 cjt_count
+ |> map (conc_str_int "a") |> variants nctxt0;
+
+ (* make normal-order separation conjunction terms *)
+ val orig = sep_conj_prop cjts;
+
+ (* make reordered separation conjunction terms *)
+ val reordered = sep_conj_prop (ListExtra.nth_to_front cjt_select cjts);
+
+ val goal = Logic.mk_implies
+ (if conclusion then (orig, reordered) else (reordered, orig));
+
+ (* simp add: sep_conj_ac *)
+ val sep_conj_ac_tac = Simplifier.asm_full_simp_tac
+ (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac);
+
+in
+ (* XXX: normally you'd want to keep track of what variables we want to make
+ schematic and which ones are bound, but we don't use fixed names for
+ the rules we make, so we use Drule.export_without_context to schematise
+ all. *)
+ Goal.prove ctxt [] [] goal (fn _ => sep_conj_ac_tac 1)
+ |> Drule.export_without_context
+end;
+
+(* }}} *)
+
+local
+ (* Common tactic functionality {{{ *)
+
+ (* given two terms of some 'a to bool, can you prove
+ \<And>s. t1 s \<Longrightarrow> t2 s
+ using the supplied proof method?
+ NOTE: t1 and t2 MUST have a function type with one argument,
+ or TYPE dest_Type is raised
+ NOTE: if asm or concl is sep_true, returns false
+ *)
+ fun can_prove ctxt tac asm concl =
+ let
+ fun variant name = Name.variant name (Variable.names_of ctxt) |> fst;
+ val arg_name = variant "s";
+ val left = FunApp.fun_app_free asm arg_name |> HOLogic.mk_Trueprop;
+ val right = FunApp.fun_app_free concl arg_name |> HOLogic.mk_Trueprop;
+ val goal = Logic.mk_implies (left, right);
+ in
+ if (SepConj.is_sep_true_term asm) orelse (SepConj.is_sep_true_term concl)
+ then false
+ else (Goal.prove ctxt [] [] goal (fn _ => tac 1); true)
+ handle ERROR _ => false
+ end;
+
+ (* apply function in list until it returns SOME *)
+ fun find_some (x::xs) f =
+ (case f x of SOME v => SOME v
+ | NONE => find_some xs f)
+ | find_some [] _ = NONE;
+
+ (* Given indices into the separating conjunctions in the assumption and
+ conclusion, rewrite them so that the targeted conjuncts are at the
+ front, then remove them. *)
+ fun eliminate_target_tac ctxt tac
+ ((prem_total,prem_idx), (concl_total,concl_idx)) =
+ let
+ val asm_select = mk_sep_select_rule ctxt true (prem_total,prem_idx);
+ val concl_select = mk_sep_select_rule ctxt false
+ (concl_total,concl_idx);
+ in
+ dtac asm_select THEN' rtac concl_select
+ THEN' etac SepConj.sep_conj_impl THEN' tac
+ end;
+
+ fun find_target ctxt tac cprem cconcl =
+ let
+ val prem_cjts = cprem |> term_of |> SepConj.break_sep_conj;
+ val concl_cjts = cconcl |> term_of |> SepConj.break_sep_conj;
+
+ val iprems = ListExtra.index_list prem_cjts;
+ val iconcls = ListExtra.index_list concl_cjts;
+
+ fun can_prove' (pi,p) (ci,c) =
+ if can_prove ctxt tac p c then SOME (pi, ci) else NONE;
+
+ val target = find_some iconcls
+ (fn c => find_some iprems (fn p => can_prove' p c));
+ in
+ case target
+ of SOME (pi,ci) => SOME ((List.length prem_cjts, pi),
+ (List.length concl_cjts, ci))
+ | NONE => NONE
+ end;
+
+ fun strip_cprop ct =
+ let val thy = theory_of_cterm ct
+ in ct |> term_of |> HOLogic.dest_Trueprop |> cterm_of thy
+ end;
+
+ (* }}} *)
+in
+
+ (* Tactic: Select nth conjunct in assumption {{{ *)
+ local
+ fun sep_select_asm_tac' ctxt n (ct, i) =
+ let
+ (* digging out prems *)
+ val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
+ val prems = Drule.strip_imp_prems ct';
+
+ fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct)
+
+ fun mk_tac prem =
+ let
+ val prem = HOLogic.dest_Trueprop (term_of prem)
+ val p = length (SepConj.break_sep_conj prem)
+ val th = mk_sep_select_rule ctxt true (p,n)
+ handle Subscript => error "Conjunct index out of range"
+ in
+ dtac th i
+ end;
+ in
+ if length prems = 0
+ then error ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^
+ " _) _")
+ else
+ (* backtrack until first premise that does something *)
+ map mk_tac (filter prem_ok prems) |> FIRST
+ end;
+ in
+ fun sep_select_asm_tac ctxt n = CSUBGOAL (sep_select_asm_tac' ctxt (n-1))
+ end; (* }}} *)
+
+ (* Tactic: Select nth conjunct in conclusion {{{ *)
+ local
+ fun sep_select_tac' ctxt n (ct, i) =
+ let
+ (* digging out conclusions *)
+ val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
+ val concl = ct' |> Drule.strip_imp_concl |> term_of;
+ val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj
+ |> length;
+ val th = mk_sep_select_rule ctxt false (p,n)
+ handle Subscript => error "Conjunct index out of range"
+ in
+ if not (SepConj.is_sep_conj_prop concl)
+ then error ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^ " _) _")
+ else rtac th i
+ end;
+ in
+ fun sep_select_tac ctxt n = CSUBGOAL (sep_select_tac' ctxt (n-1))
+ end; (* }}} *)
+
+ (* Tactic: for all reorderings of the premises try apply tac {{{ *)
+ local
+ fun sep_assm_tac' ctxt tac (ct,i) =
+ let
+ (* digging out prems *)
+ val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
+ val prems = Drule.strip_imp_prems ct';
+
+ fun prem_ok ct = SepConj.is_sep_conj_prop (term_of ct)
+
+ fun mk_tac prem =
+ let
+ val prem = HOLogic.dest_Trueprop (term_of prem)
+ val p = length (SepConj.break_sep_conj prem)
+ fun ord n = mk_sep_select_rule ctxt true (p,n)
+ val ord_thms = map ord (0 upto p-1)
+ in
+ (dresolve_tac ord_thms THEN' tac) i
+ end;
+ in
+ (* backtrack until first premise that does something *)
+ map mk_tac (filter prem_ok prems) |> FIRST
+ end;
+ in
+ fun sep_assm_tac ctxt tac = CSUBGOAL (sep_assm_tac' ctxt tac)
+ end; (* }}} *)
+
+ (* Tactic: for all reorderings of the conclusion, try apply tac {{{ *)
+ local
+ fun sep_concl_tac' ctxt tac (ct, i) =
+ let
+ (* digging out conclusion *)
+ val ((_, ct'), _) = Variable.focus_cterm ct ctxt;
+ val concl = ct' |> Drule.strip_imp_concl |> term_of;
+ val p = concl |> HOLogic.dest_Trueprop |> SepConj.break_sep_conj
+ |> length;
+ fun ord n = mk_sep_select_rule ctxt false (p,n);
+ val ord_thms = map ord (0 upto p-1);
+ in
+ if not (SepConj.is_sep_conj_prop concl)
+ then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^
+ " _) _");
+ no_tac)
+ else (resolve_tac ord_thms THEN' tac) i
+ end;
+ in
+ fun sep_concl_tac ctxt tac = CSUBGOAL (sep_concl_tac' ctxt tac)
+ end; (* }}} *)
+
+ (* Tactic: Cancel conjuncts of assumption and conclusion via tac {{{ *)
+ local
+ fun sep_cancel_tac' ctxt tac (ct, i) =
+ let
+ (* digging out prems and conclusions *)
+ val ((vars, ct'), ctxt') = Variable.focus_cterm ct ctxt;
+ val concl = Drule.strip_imp_concl ct';
+ val prems = Drule.strip_imp_prems ct';
+
+ fun prem_ok ct =
+ let
+ (* name of state in sep conj (should be Free after focus) *)
+ fun state_get (_ $ _ $ _ $ s) = s
+ | state_get t = raise Fail "prem_ok: state_get";
+ val state_get_ct = state_get o HOLogic.dest_Trueprop o term_of;
+
+ val concl_state = concl |> state_get_ct;
+ (* states considered equal if they alpha-convert *)
+ fun state_ok ct = (state_get_ct ct) aconv concl_state;
+ in
+ SepConj.is_sep_conj_prop (term_of ct) andalso state_ok ct
+ end;
+
+ fun mk_tac prem =
+ case find_target ctxt tac (prem |> strip_cprop)
+ (strip_cprop concl)
+ of SOME target => eliminate_target_tac ctxt tac target i
+ | NONE => no_tac;
+ in
+ if (not (concl |> term_of |> SepConj.is_sep_conj_prop))
+ then (tracing ("Goal not of form: (_ " ^ SepConj.sep_conj_str ^
+ " _) _");
+ no_tac)
+ else if (length prems = 0)
+ then (tracing ("No assumption of form: (_ " ^ SepConj.sep_conj_str ^
+ " _) _");
+ no_tac)
+ else
+ (* backtrack until first premise that does something *)
+ map mk_tac (filter prem_ok prems) |> FIRST
+ end;
+ in
+ fun sep_cancel_tac ctxt tac = CSUBGOAL (sep_cancel_tac' ctxt tac)
+ end;
+ (* }}} *)
+
+ (* Derived Tactics *)
+
+ fun sep_atac ctxt = sep_assm_tac ctxt atac;
+
+ (* Substitution *)
+ fun sep_subst_tac ctxt occs thms =
+ EqSubst.eqsubst_tac ctxt occs thms THEN' sep_atac ctxt;
+ fun sep_subst_asm_tac ctxt occs thms =
+ EqSubst.eqsubst_asm_tac ctxt occs thms THEN' sep_atac ctxt;
+
+ (* Forward reasoning *)
+ fun sep_dtac ctxt thms = sep_assm_tac ctxt (dresolve_tac thms)
+ fun sep_ftac ctxt thms = sep_assm_tac ctxt (forward_tac thms)
+
+ (* Backward reasoning *)
+ fun sep_rtac ctxt thms = sep_concl_tac ctxt (resolve_tac thms)
+
+end;
+
+(* vim: set foldmethod=marker sw=2 sts=2 et: *)
+