diff -r 000000000000 -r 1378b654acde Separation_Algebra/sep_tactics.ML --- /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 + Rafal Kolanski +*) + +(* 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 + \s. t1 s \ 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: *) +