1 theory Tacs

     2 imports Main

     3 begin

     4 

     5 (* General not-nominal/quotient functionality useful for proving *)

     6 

     7 (* A version of case_rule_tac that takes more exhaust rules *)

     8 ML {*

     9 fun case_rules_tac ctxt0 s rules i st =

    10 let

    11   val (_, ctxt) = Variable.focus_subgoal i st ctxt0;

    12   val ty = fastype_of (ProofContext.read_term_schematic ctxt s)

    13   fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));

    14   val ty_rules = filter (fn x => exhaust_ty x = ty) rules;

    15 in

    16   InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st

    17 end

    18 *}

    19 

    20 ML {*

    21 fun mk_conjl props =

    22   fold (fn a => fn b =>

    23     if a = @{term True} then b else

    24     if b = @{term True} then a else

    25     HOLogic.mk_conj (a, b)) (rev props) @{term True};

    26 *}

    27 

    28 ML {*

    29 val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)

    30 *}

    31 

    32 (* Given function for buildng a goal for an input, prepares a

    33    one common goals for all the inputs and proves it by induction

    34    together *)

    35 ML {*

    36 fun prove_by_induct tys build_goal ind utac inputs ctxt =

    37 let

    38   val names = Datatype_Prop.make_tnames tys;

    39   val (names', ctxt') = Variable.variant_fixes names ctxt;

    40   val frees = map Free (names' ~~ tys);

    41   val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';

    42   val gls = flat gls_lists;

    43   fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;

    44   val trm_gl_lists = map trm_gls_map frees;

    45   val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists

    46   val trm_gls = map mk_conjl trm_gl_lists;

    47   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);

    48   fun tac {context,...} = (

    49     InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]

    50     THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1

    51   val th_loc = Goal.prove ctxt'' [] [] gl tac

    52   val ths_loc = HOLogic.conj_elims th_loc

    53   val ths = Variable.export ctxt'' ctxt ths_loc

    54 in

    55   filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths

    56 end

    57 *}

    58 

    59 (* An induction for a single relation is "R x y \<Longrightarrow> P x y"

    60    but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)

    61 ML {*

    62 fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct

    63 *}

    64 

    65 ML {*

    66 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =

    67 let

    68   val tys = map (domain_type o fastype_of) alphas;

    69   val names = Datatype_Prop.make_tnames tys;

    70   val (namesl, ctxt') = Variable.variant_fixes names ctxt;

    71   val (namesr, ctxt'') = Variable.variant_fixes names ctxt';

    72   val freesl = map Free (namesl ~~ tys);

    73   val freesr = map Free (namesr ~~ tys);

    74   val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';

    75   val gls = flat gls_lists;

    76   fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;

    77   val trm_gl_lists = map trm_gls_map freesl;

    78   val trm_gls = map mk_conjl trm_gl_lists;

    79   val pgls = map

    80     (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 

    81     ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))

    82   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);

    83   fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW

    84     TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1

    85   val th_loc = Goal.prove ctxt'' [] [] gl tac

    86   val ths_loc = HOLogic.conj_elims th_loc

    87   val ths = Variable.export ctxt'' ctxt ths_loc

    88 in

    89   filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths

    90 end

    91 *}

    92 (* Code for transforming an inductive relation to a function *)

    93 ML {*

    94 fun rel_inj_tac dist_inj intrs elims =

    95   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'

    96   (rtac @{thm iffI} THEN' RANGE [

    97      (eresolve_tac elims THEN_ALL_NEW

    98        asm_full_simp_tac (HOL_ss addsimps dist_inj)

    99      ),

   100      asm_full_simp_tac (HOL_ss addsimps intrs)])

   101 *}

   102 

   103 ML {*

   104 fun build_rel_inj_gl thm =

   105   let

   106     val prop = prop_of thm;

   107     val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);

   108     val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);

   109     fun list_conj l = foldr1 HOLogic.mk_conj l;

   110   in

   111     if hyps = [] then concl

   112     else HOLogic.mk_eq (concl, list_conj hyps)

   113   end;

   114 *}

   115 

   116 ML {*

   117 fun build_rel_inj intrs dist_inj elims ctxt =

   118 let

   119   val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;

   120   val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;

   121   fun tac _ = rel_inj_tac dist_inj intrs elims 1;

   122   val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;

   123 in

   124   Variable.export ctxt' ctxt thms

   125 end

   126 *}

   127 

   128 end

   129