src/HOL/Tools/TFL/casesplit.ML
changeset 29265 5b4247055bd7
parent 23150 073a65f0bc40
child 29270 0eade173f77e
equal deleted inserted replaced
29264:4ea3358fac3f 29265:5b4247055bd7
     1 (*  Title:      HOL/Tools/TFL/casesplit.ML
     1 (*  Title:      HOL/Tools/TFL/casesplit.ML
     2     ID:         $Id$
       
     3     Author:     Lucas Dixon, University of Edinburgh
     2     Author:     Lucas Dixon, University of Edinburgh
     4 
     3 
     5 A structure that defines a tactic to program case splits.
     4 A structure that defines a tactic to program case splits.
     6 
     5 
     7     casesplit_free :
     6     casesplit_free :
   102     in
   101     in
   103       cases_thm_of_induct_thm (#induction dt)
   102       cases_thm_of_induct_thm (#induction dt)
   104     end;
   103     end;
   105 
   104 
   106 (*
   105 (*
   107  val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
   106  val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
   108 *)
   107 *)
   109 
   108 
   110 
   109 
   111 (* for use when there are no prems to the subgoal *)
   110 (* for use when there are no prems to the subgoal *)
   112 (* does a case split on the given variable *)
   111 (* does a case split on the given variable *)
   120       val case_thm = case_thm_of_ty sgn ty;
   119       val case_thm = case_thm_of_ty sgn ty;
   121 
   120 
   122       val abs_ct = ctermify abst;
   121       val abs_ct = ctermify abst;
   123       val free_ct = ctermify x;
   122       val free_ct = ctermify x;
   124 
   123 
   125       val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
   124       val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
   126 
   125 
   127       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   126       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   128       val (Pv, Dv, type_insts) =
   127       val (Pv, Dv, type_insts) =
   129           case (Thm.concl_of case_thm) of
   128           case (Thm.concl_of case_thm) of
   130             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   129             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   168     let
   167     let
   169       val (subgoalth, exp) = IsaND.fix_alls i th;
   168       val (subgoalth, exp) = IsaND.fix_alls i th;
   170       val subgoalth' = atomize_goals subgoalth;
   169       val subgoalth' = atomize_goals subgoalth;
   171       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   170       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   172 
   171 
   173       val freets = Term.term_frees gt;
   172       val freets = OldTerm.term_frees gt;
   174       fun getter x =
   173       fun getter x =
   175           let val (n,ty) = Term.dest_Free x in
   174           let val (n,ty) = Term.dest_Free x in
   176             (if vstr = n orelse vstr = Name.dest_skolem n
   175             (if vstr = n orelse vstr = Name.dest_skolem n
   177              then SOME (n,ty) else NONE )
   176              then SOME (n,ty) else NONE )
   178             handle Fail _ => NONE (* dest_skolem *)
   177             handle Fail _ => NONE (* dest_skolem *)