src/Tools/induct.ML
changeset 56231 b98813774a63
parent 55954 a29aefc88c8d
child 56245 84fc7dfa3cd4
     1.1 --- a/src/Tools/induct.ML	Thu Mar 20 19:58:33 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Thu Mar 20 21:07:57 2014 +0100
     1.3 @@ -741,71 +741,71 @@
     1.4  type case_data = (((string * string list) * string list) list * int);
     1.5  
     1.6  fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
     1.7 -  let
     1.8 -    val thy = Proof_Context.theory_of ctxt;
     1.9 -
    1.10 -    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    1.11 -    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
    1.12 -
    1.13 -    fun inst_rule (concls, r) =
    1.14 -      (if null insts then `Rule_Cases.get r
    1.15 -       else (align_left "Rule has fewer conclusions than arguments given"
    1.16 -          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    1.17 -        |> maps (prep_inst ctxt align_right (atomize_term thy))
    1.18 -        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    1.19 -      |> mod_cases thy
    1.20 -      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.21 -
    1.22 -    val ruleq =
    1.23 -      (case opt_rule of
    1.24 -        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    1.25 -      | NONE =>
    1.26 -          (get_inductP ctxt facts @
    1.27 -            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
    1.28 -          |> map_filter (Rule_Cases.mutual_rule ctxt)
    1.29 -          |> tap (trace_rules ctxt inductN o map #2)
    1.30 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.31 -
    1.32 -    fun rule_cases ctxt rule cases =
    1.33 -      let
    1.34 -        val rule' = Rule_Cases.internalize_params rule;
    1.35 -        val rule'' = rule' |> simp ? simplified_rule ctxt;
    1.36 -        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
    1.37 -        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
    1.38 -      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
    1.39 -  in
    1.40 -    (fn i => fn st =>
    1.41 -      ruleq
    1.42 -      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
    1.43 -      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.44 -        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.45 -          (CONJUNCTS (ALLGOALS
    1.46 -            let
    1.47 -              val adefs = nth_list atomized_defs (j - 1);
    1.48 -              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
    1.49 -              val xs = nth_list arbitrary (j - 1);
    1.50 -              val k = nth concls (j - 1) + more_consumes
    1.51 -            in
    1.52 -              Method.insert_tac (more_facts @ adefs) THEN'
    1.53 -                (if simp then
    1.54 -                   rotate_tac k (length adefs) THEN'
    1.55 -                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    1.56 -                 else
    1.57 -                   arbitrary_tac defs_ctxt k xs)
    1.58 -             end)
    1.59 -          THEN' inner_atomize_tac defs_ctxt) j))
    1.60 -        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
    1.61 -            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
    1.62 -            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    1.63 -            |> Seq.maps (fn rule' =>
    1.64 -              CASES (rule_cases ctxt rule' cases)
    1.65 -                (rtac rule' i THEN
    1.66 -                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    1.67 -    THEN_ALL_NEW_CASES
    1.68 -      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
    1.69 -        else K all_tac)
    1.70 -       THEN_ALL_NEW rulify_tac ctxt)
    1.71 -  end;
    1.72 +  SUBGOAL_CASES (fn (_, i, st) =>
    1.73 +    let
    1.74 +      val thy = Proof_Context.theory_of ctxt;
    1.75 +  
    1.76 +      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    1.77 +      val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
    1.78 +  
    1.79 +      fun inst_rule (concls, r) =
    1.80 +        (if null insts then `Rule_Cases.get r
    1.81 +         else (align_left "Rule has fewer conclusions than arguments given"
    1.82 +            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    1.83 +          |> maps (prep_inst ctxt align_right (atomize_term thy))
    1.84 +          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    1.85 +        |> mod_cases thy
    1.86 +        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.87 +  
    1.88 +      val ruleq =
    1.89 +        (case opt_rule of
    1.90 +          SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    1.91 +        | NONE =>
    1.92 +            (get_inductP ctxt facts @
    1.93 +              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
    1.94 +            |> map_filter (Rule_Cases.mutual_rule ctxt)
    1.95 +            |> tap (trace_rules ctxt inductN o map #2)
    1.96 +            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.97 +  
    1.98 +      fun rule_cases ctxt rule cases =
    1.99 +        let
   1.100 +          val rule' = Rule_Cases.internalize_params rule;
   1.101 +          val rule'' = rule' |> simp ? simplified_rule ctxt;
   1.102 +          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
   1.103 +          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
   1.104 +        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
   1.105 +    in
   1.106 +      fn st =>
   1.107 +        ruleq
   1.108 +        |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
   1.109 +        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   1.110 +          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   1.111 +            (CONJUNCTS (ALLGOALS
   1.112 +              let
   1.113 +                val adefs = nth_list atomized_defs (j - 1);
   1.114 +                val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
   1.115 +                val xs = nth_list arbitrary (j - 1);
   1.116 +                val k = nth concls (j - 1) + more_consumes
   1.117 +              in
   1.118 +                Method.insert_tac (more_facts @ adefs) THEN'
   1.119 +                  (if simp then
   1.120 +                     rotate_tac k (length adefs) THEN'
   1.121 +                     arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
   1.122 +                   else
   1.123 +                     arbitrary_tac defs_ctxt k xs)
   1.124 +               end)
   1.125 +            THEN' inner_atomize_tac defs_ctxt) j))
   1.126 +          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
   1.127 +              guess_instance ctxt (internalize ctxt more_consumes rule) i st'
   1.128 +              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   1.129 +              |> Seq.maps (fn rule' =>
   1.130 +                CASES (rule_cases ctxt rule' cases)
   1.131 +                  (rtac rule' i THEN
   1.132 +                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
   1.133 +      end)
   1.134 +      THEN_ALL_NEW_CASES
   1.135 +        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
   1.136 +         THEN_ALL_NEW rulify_tac ctxt);
   1.137  
   1.138  val induct_tac = gen_induct_tac (K I);
   1.139  
   1.140 @@ -832,7 +832,7 @@
   1.141  
   1.142  in
   1.143  
   1.144 -fun coinduct_tac ctxt inst taking opt_rule facts =
   1.145 +fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
   1.146    let
   1.147      val thy = Proof_Context.theory_of ctxt;
   1.148  
   1.149 @@ -849,7 +849,7 @@
   1.150            |> tap (trace_rules ctxt coinductN)
   1.151            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   1.152    in
   1.153 -    SUBGOAL_CASES (fn (goal, i) => fn st =>
   1.154 +    fn st =>
   1.155        ruleq goal
   1.156        |> Seq.maps (Rule_Cases.consume ctxt [] facts)
   1.157        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   1.158 @@ -858,8 +858,8 @@
   1.159          |> Seq.maps (fn rule' =>
   1.160            CASES (Rule_Cases.make_common (thy,
   1.161                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   1.162 -            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
   1.163 -  end;
   1.164 +            (Method.insert_tac more_facts i THEN rtac rule' i) st))
   1.165 +  end);
   1.166  
   1.167  end;
   1.168