TFL/post.sml
changeset 3271 b873969b05d3
parent 3245 241838c01caf
child 3302 404fe31fd8d2
equal deleted inserted replaced
3270:4a3ab8d43451 3271:b873969b05d3
   138 fun mk_meta_eq r = case concl_of r of
   138 fun mk_meta_eq r = case concl_of r of
   139      Const("==",_)$_$_ => r
   139      Const("==",_)$_$_ => r
   140   |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   140   |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   141   |   _ => r RS P_imp_P_eq_True
   141   |   _ => r RS P_imp_P_eq_True
   142 fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
   142 fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
   143 fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss))
   143 fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset)))
   144 
   144 
   145 fun join_assums th = 
   145 fun join_assums th = 
   146   let val {sign,...} = rep_thm th
   146   let val {sign,...} = rep_thm th
   147       val tych = cterm_of sign
   147       val tych = cterm_of sign
   148       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   148       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   156   end
   156   end
   157   val gen_all = S.gen_all
   157   val gen_all = S.gen_all
   158 in
   158 in
   159 (*---------------------------------------------------------------------------
   159 (*---------------------------------------------------------------------------
   160  * The "reducer" argument is 
   160  * The "reducer" argument is 
   161  *  (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); 
   161  *  (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset)))); 
   162  *---------------------------------------------------------------------------*)
   162  *---------------------------------------------------------------------------*)
   163 fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
   163 fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
   164   let val dummy = output(std_out, "Proving induction theorem..  ")
   164   let val dummy = prs "Proving induction theorem..  "
   165       val ind = Prim.mk_induction theory f R full_pats_TCs
   165       val ind = Prim.mk_induction theory f R full_pats_TCs
   166       val dummy = output(std_out, "Proved induction theorem.\n")
   166       val dummy = writeln "Proved induction theorem."
   167       val pp = std_postprocessor theory
   167       val pp = std_postprocessor theory
   168       val dummy = output(std_out, "Postprocessing..  ")
   168       val dummy = prs "Postprocessing..  "
   169       val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
   169       val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
   170   in
   170   in
   171   case nested_tcs
   171   case nested_tcs
   172   of [] => (output(std_out, "Postprocessing done.\n");
   172   of [] => (writeln "Postprocessing done.";
   173             {induction=induction, rules=rules,tcs=[]})
   173             {induction=induction, rules=rules,tcs=[]})
   174   | L  => let val dummy = output(std_out, "Simplifying nested TCs..  ")
   174   | L  => let val dummy = prs "Simplifying nested TCs..  "
   175               val (solved,simplified,stubborn) =
   175               val (solved,simplified,stubborn) =
   176                U.itlist (fn th => fn (So,Si,St) =>
   176                U.itlist (fn th => fn (So,Si,St) =>
   177                      if (id_thm th) then (So, Si, th::St) else
   177                      if (id_thm th) then (So, Si, th::St) else
   178                      if (solved th) then (th::So, Si, St) 
   178                      if (solved th) then (th::So, Si, St) 
   179                      else (So, th::Si, St)) nested_tcs ([],[],[])
   179                      else (So, th::Si, St)) nested_tcs ([],[],[])
   180               val simplified' = map join_assums simplified
   180               val simplified' = map join_assums simplified
   181               val induction' = reducer (solved@simplified') induction
   181               val induction' = reducer (solved@simplified') induction
   182               val rules' = reducer (solved@simplified') rules
   182               val rules' = reducer (solved@simplified') rules
   183               val dummy = output(std_out, "Postprocessing done.\n")
   183               val dummy = writeln "Postprocessing done."
   184           in
   184           in
   185           {induction = induction',
   185           {induction = induction',
   186                rules = rules',
   186                rules = rules',
   187                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   187                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   188                            (simplified@stubborn)}
   188                            (simplified@stubborn)}
   189           end
   189           end
   190   end handle (e as Utils.ERR _) => Utils.Raise e
   190   end handle (e as Utils.ERR _) => Utils.Raise e
   191           |   e                 => print_exn e;
   191           |   e                 => print_exn e;
   192 
   192 
   193 
   193 
       
   194 (*lcp: uncurry the predicate of the induction rule*)
       
   195 fun uncurry_rule rl = Prod_Syntax.split_rule_var
       
   196                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
       
   197 			 rl);
       
   198 
   194 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   199 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   195 val meta_outer = 
   200 val meta_outer = 
   196     standard o rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]));
   201     uncurry_rule o standard o 
   197 
   202     rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
       
   203 				  ORELSE' etac conjE));
   198 
   204 
   199 (*Strip off the outer !P*)
   205 (*Strip off the outer !P*)
   200 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   206 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   201 
   207 
   202 
   208