TFL/post.ML
changeset 14240 d3843feb9de7
parent 13501 79242cccaddc
child 15150 c7af682b9ee5
equal deleted inserted replaced
14239:af2a9e68bea9 14240:d3843feb9de7
   136                U.itlist (fn th => fn (So,Si,St) =>
   136                U.itlist (fn th => fn (So,Si,St) =>
   137                      if (id_thm th) then (So, Si, th::St) else
   137                      if (id_thm th) then (So, Si, th::St) else
   138                      if (solved th) then (th::So, Si, St)
   138                      if (solved th) then (th::So, Si, St)
   139                      else (So, th::Si, St)) nested_tcs ([],[],[])
   139                      else (So, th::Si, St)) nested_tcs ([],[],[])
   140               val simplified' = map join_assums simplified
   140               val simplified' = map join_assums simplified
       
   141               val dummy = (Prim.trace_thms "solved =" solved;
       
   142                            Prim.trace_thms "simplified' =" simplified')
   141               val rewr = full_simplify (ss addsimps (solved @ simplified'));
   143               val rewr = full_simplify (ss addsimps (solved @ simplified'));
       
   144               val dummy = Prim.trace_thms "Simplifying the induction rule..."
       
   145                                           [induction]
   142               val induction' = rewr induction
   146               val induction' = rewr induction
   143               and rules'     = rewr rules
   147               val dummy = Prim.trace_thms "Simplifying the recursion rules..."
       
   148                                           [rules]
       
   149               val rules'     = rewr rules
       
   150               val _ = message "... Postprocessing finished";
   144           in
   151           in
   145           {induction = induction',
   152           {induction = induction',
   146                rules = rules',
   153                rules = rules',
   147                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   154                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   148                            (simplified@stubborn)}
   155                            (simplified@stubborn)}
   160   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   167   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   161 
   168 
   162 (*Strip off the outer !P*)
   169 (*Strip off the outer !P*)
   163 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   170 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   164 
   171 
       
   172 fun tracing true _ = ()
       
   173   | tracing false msg = writeln msg;
       
   174 
   165 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
   175 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
   166    let val def = freezeT def0 RS meta_eq_to_obj_eq
   176    let val def = freezeT def0 RS meta_eq_to_obj_eq
   167        val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
   177        val {theory,rules,rows,TCs,full_pats_TCs} =
       
   178            Prim.post_definition congs (thy, (def,pats))
   168        val {lhs=f,rhs} = S.dest_eq (concl def)
   179        val {lhs=f,rhs} = S.dest_eq (concl def)
   169        val (_,[R,_]) = S.strip_comb rhs
   180        val (_,[R,_]) = S.strip_comb rhs
       
   181        val dummy = Prim.trace_thms "congs =" congs
       
   182        (*the next step has caused simplifier looping in some cases*)
   170        val {induction, rules, tcs} =
   183        val {induction, rules, tcs} =
   171              proof_stage strict cs ss wfs theory
   184              proof_stage strict cs ss wfs theory
   172                {f = f, R = R, rules = rules,
   185                {f = f, R = R, rules = rules,
   173                 full_pats_TCs = full_pats_TCs,
   186                 full_pats_TCs = full_pats_TCs,
   174                 TCs = TCs}
   187                 TCs = TCs}
   175        val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
   188        val rules' = map (standard o ObjectLogic.rulify_no_asm)
   176    in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   189                         (R.CONJUNCTS rules)
       
   190          in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   177         rules = ListPair.zip(rules', rows),
   191         rules = ListPair.zip(rules', rows),
   178         tcs = (termination_goals rules') @ tcs}
   192         tcs = (termination_goals rules') @ tcs}
   179    end
   193    end
   180   handle U.ERR {mesg,func,module} =>
   194   handle U.ERR {mesg,func,module} =>
   181                error (mesg ^
   195                error (mesg ^