TFL/post.ML
 changeset 14240 d3843feb9de7 parent 13501 79242cccaddc child 15150 c7af682b9ee5
equal 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 ^`