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 

    33 ML {*

    34 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =

    35 let

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

    37   val names = Datatype_Prop.make_tnames tys;

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

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

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

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

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

    43   val gls = flat gls_lists;

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

    45   val trm_gl_lists = map trm_gls_map freesl;

    46   val trm_gls = map mk_conjl trm_gl_lists;

    47   val pgls = map

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

    49     ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))

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

    51   fun tac {context,...} = (rtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW

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

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

    54   val ths_loc = HOLogic.conj_elims th_loc

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

    56 in

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

    58 end

    59 *}

    60 

    61 ML {*

    62 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm

    63 *}

    64 

    65 (* Introduces an implication and immediately eliminates it by cases *)

    66 ML {*

    67 fun imp_elim_tac case_rules =

    68   Subgoal.FOCUS (fn {concl, context, ...} =>

    69     case term_of concl of

    70       _ $ (_ $ asm $ _) =>

    71         let

    72           fun filter_fn case_rule = (

    73             case Logic.strip_assums_hyp (prop_of case_rule) of

    74               ((_ $ asmc) :: _) =>

    75                 let

    76                   val thy = ProofContext.theory_of context

    77                 in

    78                   Pattern.matches thy (asmc, asm)

    79                 end

    80             | _ => false)

    81           val matching_rules = filter filter_fn case_rules

    82         in

    83          (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1

    84         end

    85     | _ => no_tac)

    86 *}

    87 

    88 ML {*

    89 fun is_ex (Const ("Ex", _) $ Abs _) = true

    90   | is_ex _ = false;

    91 *}

    92 

    93 ML {*

    94 fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free"

    95   | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"

    96   | dtyp_no_of_typ dts (Type (tname, _)) =

    97       case try (find_index (curry op = tname o fst)) dts of

    98         NONE => error "dtyp_no_of_typ: Illegal recursion"

    99       | SOME i => i

   100 *}

   101 

   102 end

   103