Added exhaustion thm and exhaust_tac for each datatype.
authornipkow
Thu May 22 09:20:28 1997 +0200 (1997-05-22)
changeset 3282c31e6239d4c9
parent 3281 d4ddd43f418a
child 3283 0db086394024
Added exhaustion thm and exhaust_tac for each datatype.
src/HOL/NatDef.ML
src/HOL/datatype.ML
src/HOL/simpdata.ML
src/HOL/thy_data.ML
     1.1 --- a/src/HOL/NatDef.ML	Wed May 21 17:31:12 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Thu May 22 09:20:28 1997 +0200
     1.3 @@ -46,13 +46,6 @@
     1.4            COND (Datatype.occs_in_prems a (i+1)) all_tac
     1.5                 (rename_last_tac a [""] (i+1))];
     1.6  
     1.7 -(*Install 'automatic' induction tactic, pretending nat is a datatype *)
     1.8 -(*except for induct_tac, everything is dummy*)
     1.9 -datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.10 -  constructors = [], induct_tac = nat_ind_tac,
    1.11 -  nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.12 -
    1.13 -
    1.14  (*A special form of induction for reasoning about m<n and m-n*)
    1.15  val prems = goal thy
    1.16      "[| !!x. P x 0;  \
    1.17 @@ -76,6 +69,14 @@
    1.18  by (Blast_tac 1);
    1.19  qed "natE";
    1.20  
    1.21 +(*Install 'automatic' induction tactic, pretending nat is a datatype *)
    1.22 +(*except for induct_tac, everything is dummy*)
    1.23 +datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.24 +  constructors = [], induct_tac = nat_ind_tac,
    1.25 +  exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
    1.26 +  nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.27 +
    1.28 +
    1.29  (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    1.30  
    1.31  (*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),
     2.1 --- a/src/HOL/datatype.ML	Wed May 21 17:31:12 1997 +0200
     2.2 +++ b/src/HOL/datatype.ML	Thu May 22 09:20:28 1997 +0200
     2.3 @@ -798,6 +798,21 @@
     2.4   end
     2.5   handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
     2.6  
     2.7 +(*---------------------------------------------------------------------------
     2.8 + * Turn nchotomy into exhaustion:
     2.9 + *    [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |]
    2.10 + *    ==> P
    2.11 + *---------------------------------------------------------------------------*)
    2.12 +fun mk_exhaust nchotomy =
    2.13 +  let val tac = rtac impI 1 THEN
    2.14 +                REPEAT(SOMEGOAL(eresolve_tac [disjE,exE]))
    2.15 +  in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end;
    2.16 +
    2.17 +(* find name of v in exhaustion: *)
    2.18 +fun exhaust_var thm =
    2.19 +  let val _ $ ( _ $ Var((x,_),_) $ _ ) =
    2.20 +        hd(Logic.strip_assums_hyp(hd(prems_of thm)))
    2.21 +  in x end;
    2.22  
    2.23  (*---------------------------------------------------------------------------
    2.24   * Brings the preceeding functions together.
    2.25 @@ -841,6 +856,9 @@
    2.26       fun const s = Const(s, the(Sign.const_type sign s))
    2.27       val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
    2.28       val {nchotomy,case_cong} = case_thms sign case_rewrites itac
    2.29 +     val exhaustion = mk_exhaust nchotomy
    2.30 +     val exh_var = exhaust_var exhaustion;
    2.31 +     fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion;
    2.32       fun induct_tac a i =
    2.33             STATE(fn st =>
    2.34               (if Datatype.occs_in_prems a i st
    2.35 @@ -853,6 +871,8 @@
    2.36          case_rewrites = map mk_rw case_rewrites,
    2.37          induct_tac = induct_tac,
    2.38          nchotomy = nchotomy,
    2.39 +        exhaustion = exhaustion,
    2.40 +        exhaust_tac = exhaust_tac,
    2.41          case_cong = case_cong})
    2.42   end
    2.43  end;
     3.1 --- a/src/HOL/simpdata.ML	Wed May 21 17:31:12 1997 +0200
     3.2 +++ b/src/HOL/simpdata.ML	Thu May 22 09:20:28 1997 +0200
     3.3 @@ -351,7 +351,9 @@
     3.4                     case_rewrites:thm list,
     3.5                     constructors:term list,
     3.6                     induct_tac: string -> int -> tactic,
     3.7 -                   nchotomy:thm,
     3.8 +                   nchotomy: thm,
     3.9 +                   exhaustion: thm,
    3.10 +                   exhaust_tac: string -> int -> tactic,
    3.11                     case_cong:thm};
    3.12  
    3.13  exception DT_DATA of (string * dtype_info) list;
     4.1 --- a/src/HOL/thy_data.ML	Wed May 21 17:31:12 1997 +0200
     4.2 +++ b/src/HOL/thy_data.ML	Thu May 22 09:20:28 1997 +0200
     4.3 @@ -49,27 +49,48 @@
     4.4                in (map #case_cong info, flat (map #case_rewrites info)) end;
     4.5    in {case_congs = congs, case_rewrites = rewrites} end;
     4.6  
     4.7 +local
     4.8 +
     4.9 +fun find_tname var Bi =
    4.10 +  let val frees = map dest_Free (term_frees Bi)
    4.11 +      val params = Logic.strip_params Bi;
    4.12 +  in case assoc (frees@params, var) of
    4.13 +       None => error("No such variable in subgoal: " ^ quote var)
    4.14 +     | Some(Type(tn,_)) => tn
    4.15 +     | _ => error("Cannot induct on type of " ^ quote var)
    4.16 +  end;
    4.17 +
    4.18 +fun get_dt_info sign tn =
    4.19 +      case get_thydata (thyname_of_sign sign) "datatypes" of
    4.20 +        None => error ("No such datatype: " ^ quote tn)
    4.21 +      | Some (DT_DATA ds) =>
    4.22 +          case assoc (ds, tn) of
    4.23 +            Some info => info
    4.24 +          | None => error ("Not a datatype: " ^ quote tn)
    4.25 +
    4.26 +in
    4.27 +
    4.28  (* generic induction tactic for datatypes *)
    4.29  fun induct_tac var i =
    4.30 -  let fun find_tname Bi =
    4.31 -        let val frees = map dest_Free (term_frees Bi)
    4.32 -            val params = Logic.strip_params Bi;
    4.33 -        in case assoc (frees@params, var) of
    4.34 -             None => error("No such variable in subgoal: " ^ quote var)
    4.35 -           | Some(Type(tn,_)) => tn
    4.36 -           | _ => error("Cannot induct on type of " ^ quote var)
    4.37 -        end;
    4.38 -      fun get_ind_tac sign tn =
    4.39 -        (case get_thydata (thyname_of_sign sign) "datatypes" of
    4.40 -           None => error ("No such datatype: " ^ quote tn)
    4.41 -         | Some (DT_DATA ds) =>
    4.42 -             (case assoc (ds, tn) of
    4.43 -                Some {induct_tac, ...} => induct_tac
    4.44 -              | None => error ("Not a datatype: " ^ quote tn)));
    4.45 -      fun induct state =
    4.46 +  let fun induct state =
    4.47 +        let val (_, _, Bi, _) = dest_state (state, i)
    4.48 +            val sign = #sign(rep_thm state)
    4.49 +            val tn = find_tname var Bi
    4.50 +            val ind_tac = #induct_tac(get_dt_info sign tn)
    4.51 +        in ind_tac var i end
    4.52 +  in STATE induct end;
    4.53 +
    4.54 +(* generic exhaustion tactic for datatypes *)
    4.55 +fun exhaust_tac var i =
    4.56 +  let fun exhaust state =
    4.57          let val (_, _, Bi, _) = dest_state (state, i) 
    4.58 -        in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end
    4.59 -  in STATE induct end;
    4.60 +            val sign = #sign(rep_thm state)
    4.61 +            val tn = find_tname var Bi
    4.62 +            val exh_tac = #exhaust_tac(get_dt_info sign tn)
    4.63 +        in exh_tac var i end
    4.64 +  in STATE exhaust end;
    4.65 +
    4.66 +end;
    4.67  
    4.68  (*Must be redefined in order to refer to the new instance of bind_thm
    4.69    created by init_thy_reader.*)