--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Tacs.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -0,0 +1,129 @@
+theory Tacs
+imports Main
+begin
+
+(* General not-nominal/quotient functionality useful for proving *)
+
+(* A version of case_rule_tac that takes more exhaust rules *)
+ML {*
+fun case_rules_tac ctxt0 s rules i st =
+let
+  val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
+  val ty = fastype_of (ProofContext.read_term_schematic ctxt s)
+  fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));
+  val ty_rules = filter (fn x => exhaust_ty x = ty) rules;
+in
+  InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st
+end
+*}
+
+ML {*
+fun mk_conjl props =
+  fold (fn a => fn b =>
+    if a = @{term True} then b else
+    if b = @{term True} then a else
+    HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+(* Given function for buildng a goal for an input, prepares a
+   one common goals for all the inputs and proves it by induction
+   together *)
+ML {*
+fun prove_by_induct tys build_goal ind utac inputs ctxt =
+let
+  val names = Datatype_Prop.make_tnames tys;
+  val (names', ctxt') = Variable.variant_fixes names ctxt;
+  val frees = map Free (names' ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map frees;
+  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
+  fun tac {context,...} = (
+    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
+    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+
+(* An induction for a single relation is "R x y \<Longrightarrow> P x y"
+   but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)
+ML {*
+fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+
+ML {*
+fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
+let
+  val tys = map (domain_type o fastype_of) alphas;
+  val names = Datatype_Prop.make_tnames tys;
+  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
+  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
+  val freesl = map Free (namesl ~~ tys);
+  val freesr = map Free (namesr ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map freesl;
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val pgls = map
+    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
+    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
+  fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+    TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+(* Code for transforming an inductive relation to a function *)
+ML {*
+fun rel_inj_tac dist_inj intrs elims =
+  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
+  (rtac @{thm iffI} THEN' RANGE [
+     (eresolve_tac elims THEN_ALL_NEW
+       asm_full_simp_tac (HOL_ss addsimps dist_inj)
+     ),
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
+*}
+
+ML {*
+fun build_rel_inj_gl thm =
+  let
+    val prop = prop_of thm;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+    fun list_conj l = foldr1 HOLogic.mk_conj l;
+  in
+    if hyps = [] then concl
+    else HOLogic.mk_eq (concl, list_conj hyps)
+  end;
+*}
+
+ML {*
+fun build_rel_inj intrs dist_inj elims ctxt =
+let
+  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
+  val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;
+  fun tac _ = rel_inj_tac dist_inj intrs elims 1;
+  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
+in
+  Variable.export ctxt' ctxt thms
+end
+*}
+
+end
+