src/Tools/induct.ML
changeset 33368 b1cf34f1855c
parent 33303 1e1210f31207
child 33373 674df68d4df0
     1.1 --- a/src/Tools/induct.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -216,8 +216,8 @@
     1.4  fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
     1.5  fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
     1.6  
     1.7 -val consumes0 = RuleCases.consumes_default 0;
     1.8 -val consumes1 = RuleCases.consumes_default 1;
     1.9 +val consumes0 = Rule_Cases.consumes_default 0;
    1.10 +val consumes1 = Rule_Cases.consumes_default 1;
    1.11  
    1.12  in
    1.13  
    1.14 @@ -344,10 +344,10 @@
    1.15      val thy = ProofContext.theory_of ctxt;
    1.16  
    1.17      fun inst_rule r =
    1.18 -      if null insts then `RuleCases.get r
    1.19 +      if null insts then `Rule_Cases.get r
    1.20        else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.21          |> maps (prep_inst ctxt align_left I)
    1.22 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
    1.23 +        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
    1.24  
    1.25      val ruleq =
    1.26        (case opt_rule of
    1.27 @@ -359,9 +359,9 @@
    1.28    in
    1.29      fn i => fn st =>
    1.30        ruleq
    1.31 -      |> Seq.maps (RuleCases.consume [] facts)
    1.32 +      |> Seq.maps (Rule_Cases.consume [] facts)
    1.33        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.34 -        CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
    1.35 +        CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
    1.36            (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
    1.37    end;
    1.38  
    1.39 @@ -483,7 +483,7 @@
    1.40            in Logic.list_implies (map rename_asm As, C) end;
    1.41          val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
    1.42          val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
    1.43 -      in [RuleCases.save thm thm'] end
    1.44 +      in [Rule_Cases.save thm thm'] end
    1.45    | special_rename_params _ _ ths = ths;
    1.46  
    1.47  
    1.48 @@ -570,7 +570,7 @@
    1.49        ((fn [] => NONE | ts => List.last ts) #>
    1.50          (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
    1.51          find_inductT ctxt)) [[]]
    1.52 -  |> filter_out (forall RuleCases.is_inner_rule);
    1.53 +  |> filter_out (forall Rule_Cases.is_inner_rule);
    1.54  
    1.55  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
    1.56    | get_inductP _ _ = [];
    1.57 @@ -583,29 +583,29 @@
    1.58      val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    1.59  
    1.60      fun inst_rule (concls, r) =
    1.61 -      (if null insts then `RuleCases.get r
    1.62 +      (if null insts then `Rule_Cases.get r
    1.63         else (align_left "Rule has fewer conclusions than arguments given"
    1.64            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    1.65          |> maps (prep_inst ctxt align_right (atomize_term thy))
    1.66 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
    1.67 +        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    1.68        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.69  
    1.70      val ruleq =
    1.71        (case opt_rule of
    1.72 -        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
    1.73 +        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    1.74        | NONE =>
    1.75            (get_inductP ctxt facts @
    1.76              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
    1.77 -          |> map_filter (RuleCases.mutual_rule ctxt)
    1.78 +          |> map_filter (Rule_Cases.mutual_rule ctxt)
    1.79            |> tap (trace_rules ctxt inductN o map #2)
    1.80            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.81  
    1.82      fun rule_cases rule =
    1.83 -      RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
    1.84 +      Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
    1.85    in
    1.86      (fn i => fn st =>
    1.87        ruleq
    1.88 -      |> Seq.maps (RuleCases.consume (flat defs) facts)
    1.89 +      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
    1.90        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.91          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.92            (CONJUNCTS (ALLGOALS
    1.93 @@ -643,7 +643,7 @@
    1.94  fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
    1.95  
    1.96  fun main_prop_of th =
    1.97 -  if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
    1.98 +  if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
    1.99  
   1.100  in
   1.101  
   1.102 @@ -652,9 +652,9 @@
   1.103      val thy = ProofContext.theory_of ctxt;
   1.104  
   1.105      fun inst_rule r =
   1.106 -      if null inst then `RuleCases.get r
   1.107 +      if null inst then `Rule_Cases.get r
   1.108        else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
   1.109 -        |> pair (RuleCases.get r);
   1.110 +        |> pair (Rule_Cases.get r);
   1.111  
   1.112      fun ruleq goal =
   1.113        (case opt_rule of
   1.114 @@ -666,12 +666,12 @@
   1.115    in
   1.116      SUBGOAL_CASES (fn (goal, i) => fn st =>
   1.117        ruleq goal
   1.118 -      |> Seq.maps (RuleCases.consume [] facts)
   1.119 +      |> Seq.maps (Rule_Cases.consume [] facts)
   1.120        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   1.121          guess_instance ctxt rule i st
   1.122          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   1.123          |> Seq.maps (fn rule' =>
   1.124 -          CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
   1.125 +          CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
   1.126              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   1.127    end;
   1.128