rearranged inductive package for Isar;
authorwenzelm
Tue Nov 13 22:20:51 2001 +0100 (2001-11-13)
changeset 121755cf58a1799a7
parent 12174 a0aab0b9f2e9
child 12176 f9139e09a983
rearranged inductive package for Isar;
src/ZF/Datatype.ML
src/ZF/Datatype.thy
src/ZF/Finite.thy
src/ZF/Inductive.thy
src/ZF/IsaMakefile
src/ZF/ROOT.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/ZF/Datatype.ML	Tue Nov 13 22:20:15 2001 +0100
     1.2 +++ b/src/ZF/Datatype.ML	Tue Nov 13 22:20:51 2001 +0100
     1.3 @@ -59,6 +59,7 @@
     1.4          fold_bal FOLogic.mk_conj
     1.5                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
     1.6  
     1.7 + val datatype_ss = simpset_of (the_context ());
     1.8  
     1.9   fun proc sg _ old =
    1.10     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    1.11 @@ -82,7 +83,7 @@
    1.12                 else ();
    1.13         val goal = Logic.mk_equals (old, new)
    1.14         val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    1.15 -           simp_tac (simpset_of Datatype.thy addsimps #free_iffs lcon_info) 1)
    1.16 +           simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
    1.17           handle ERROR =>
    1.18           error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
    1.19     in Some thm end
     2.1 --- a/src/ZF/Datatype.thy	Tue Nov 13 22:20:15 2001 +0100
     2.2 +++ b/src/ZF/Datatype.thy	Tue Nov 13 22:20:51 2001 +0100
     2.3 @@ -1,11 +1,13 @@
     2.4 -(*  Title:      ZF/Datatype
     2.5 +(*  Title:      ZF/Datatype.thy
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1997  University of Cambridge
     2.9  
    2.10 -Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
    2.11 -
    2.12 -	"Datatype" must be capital to avoid conflicts with ML's "datatype"
    2.13 +(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
    2.14  *)
    2.15  
    2.16 -Datatype = Inductive + Univ + QUniv
    2.17 +theory Datatype = Inductive + Univ + QUniv
    2.18 +  files "Tools/datatype_package.ML":
    2.19 +
    2.20 +end
    2.21 +
     3.1 --- a/src/ZF/Finite.thy	Tue Nov 13 22:20:15 2001 +0100
     3.2 +++ b/src/ZF/Finite.thy	Tue Nov 13 22:20:51 2001 +0100
     3.3 @@ -8,8 +8,6 @@
     3.4  
     3.5  Finite = Inductive + Nat +
     3.6  
     3.7 -setup setup_datatypes
     3.8 -
     3.9  (*The natural numbers as a datatype*)
    3.10  rep_datatype 
    3.11    elim		natE
     4.1 --- a/src/ZF/Inductive.thy	Tue Nov 13 22:20:15 2001 +0100
     4.2 +++ b/src/ZF/Inductive.thy	Tue Nov 13 22:20:51 2001 +0100
     4.3 @@ -1,5 +1,20 @@
     4.4 -(*Dummy theory to document dependencies *)
     4.5 +(*  Title:      ZF/Inductive.thy
     4.6 +    ID:         $Id$
     4.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 +    Copyright   1993  University of Cambridge
     4.9 +
    4.10 +(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
    4.11 +*)
    4.12  
    4.13 -Inductive = Fixedpt + mono + 
    4.14 +theory Inductive = Fixedpt + mono
    4.15 +  files
    4.16 +    "Tools/cartprod.ML"
    4.17 +    "Tools/ind_cases.ML"
    4.18 +    "Tools/inductive_package.ML"
    4.19 +    "Tools/induct_tacs.ML"
    4.20 +    "Tools/primrec_package.ML":
    4.21 +
    4.22 +setup IndCases.setup
    4.23 +setup induct_tacs_setup
    4.24  
    4.25  end
     5.1 --- a/src/ZF/IsaMakefile	Tue Nov 13 22:20:15 2001 +0100
     5.2 +++ b/src/ZF/IsaMakefile	Tue Nov 13 22:20:51 2001 +0100
     5.3 @@ -43,8 +43,8 @@
     5.4    OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
     5.5    Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
     5.6    Rel.ML Rel.thy Sum.ML Sum.thy \
     5.7 -  Tools/numeral_syntax.ML Tools/cartprod.ML			\
     5.8 -  Tools/datatype_package.ML Tools/induct_tacs.ML			\
     5.9 +  Tools/numeral_syntax.ML Tools/cartprod.ML				\
    5.10 +  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
    5.11    Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
    5.12    Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
    5.13    WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy		\
    5.14 @@ -126,13 +126,14 @@
    5.15  
    5.16  $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
    5.17    Induct/Comb.ML Induct/Comb.thy  Induct/FoldSet.ML Induct/FoldSet.thy \
    5.18 -  Induct/ListN.ML Induct/ListN.thy\
    5.19 -  Induct/Multiset.ML Induct/Multiset.thy  Induct/Mutil.ML Induct/Mutil.thy\
    5.20 -  Induct/Primrec_defs.ML Induct/Primrec_defs.thy\
    5.21 -  Induct/Primrec.ML Induct/Primrec.thy\
    5.22 +  Induct/ListN.ML Induct/ListN.thy \
    5.23 +  Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
    5.24 +  Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
    5.25 +  Induct/Primrec.ML Induct/Primrec.thy \
    5.26    Induct/PropLog.ML Induct/PropLog.thy  Induct/Rmap.ML Induct/Rmap.thy
    5.27  	@$(ISATOOL) usedir $(OUT)/ZF Induct
    5.28  
    5.29 +
    5.30  ## ZF-ex
    5.31  
    5.32  ZF-ex: ZF $(LOG)/ZF-ex.gz
     6.1 --- a/src/ZF/ROOT.ML	Tue Nov 13 22:20:15 2001 +0100
     6.2 +++ b/src/ZF/ROOT.ML	Tue Nov 13 22:20:51 2001 +0100
     6.3 @@ -1,35 +1,29 @@
     6.4 -(*  Title:      ZF/ROOT
     6.5 +(*  Title:      ZF/ROOT.ML
     6.6      ID:         $Id$
     6.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1993  University of Cambridge
     6.9  
    6.10 -Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
    6.11 -
    6.12 -This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
    6.13 +Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
    6.14 +This theory is the work of Martin Coen, Philippe Noel and Lawrence
    6.15 +Paulson.
    6.16  *)
    6.17  
    6.18  val banner = "ZF Set Theory (in FOL)";
    6.19  writeln banner;
    6.20  
    6.21 -eta_contract:=false;
    6.22 +reset eta_contract;
    6.23  
    6.24  print_depth 1;
    6.25  
    6.26 -(*Add user sections for inductive/datatype definitions*)
    6.27 -use     "thy_syntax";
    6.28 +(*syntax for old-style theory sections*)
    6.29 +use "thy_syntax";
    6.30  
    6.31  use "~~/src/Provers/Arith/cancel_numerals.ML";
    6.32  use "~~/src/Provers/Arith/combine_numerals.ML";
    6.33  
    6.34  use_thy "mono";
    6.35 -use     "ind_syntax.ML";
    6.36 -use     "Tools/cartprod.ML";
    6.37 -use_thy "Fixedpt";
    6.38 -use     "Tools/inductive_package.ML";
    6.39 -use     "Tools/induct_tacs.ML";
    6.40 -use     "Tools/primrec_package.ML";
    6.41 -use_thy "QUniv";
    6.42 -use     "Tools/datatype_package.ML";
    6.43 +use "ind_syntax.ML";
    6.44 +use_thy "Datatype";
    6.45  
    6.46  use     "Tools/numeral_syntax.ML";
    6.47  (*the all-in-one theory*)
     7.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Nov 13 22:20:15 2001 +0100
     7.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Nov 13 22:20:51 2001 +0100
     7.3 @@ -23,7 +23,7 @@
     7.4  (** Datatype information, e.g. associated theorems **)
     7.5  
     7.6  type datatype_info =
     7.7 -  {inductive: bool,		(*true if inductive, not coinductive*)
     7.8 +  {inductive: bool,             (*true if inductive, not coinductive*)
     7.9     constructors : term list,    (*the constructors, as Consts*)
    7.10     rec_rewrites : thm list,     (*recursor equations*)
    7.11     case_rewrites : thm list,    (*case equations*)
    7.12 @@ -75,9 +75,6 @@
    7.13  
    7.14  structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
    7.15  
    7.16 -val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
    7.17 -
    7.18 -
    7.19  
    7.20  structure DatatypeTactics : DATATYPE_TACTICS =
    7.21  struct
    7.22 @@ -90,18 +87,18 @@
    7.23  
    7.24  (*Given a variable, find the inductive set associated it in the assumptions*)
    7.25  fun find_tname var Bi =
    7.26 -  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = 
    7.27 +  let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
    7.28               (v, #1 (dest_Const (head_of A)))
    7.29 -	| mk_pair _ = raise Match
    7.30 +        | mk_pair _ = raise Match
    7.31        val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
    7.32 -	  (#2 (strip_context Bi))
    7.33 +          (#2 (strip_context Bi))
    7.34    in case assoc (pairs, var) of
    7.35         None => error ("Cannot determine datatype of " ^ quote var)
    7.36       | Some t => t
    7.37    end;
    7.38  
    7.39 -(** generic exhaustion and induction tactic for datatypes 
    7.40 -    Differences from HOL: 
    7.41 +(** generic exhaustion and induction tactic for datatypes
    7.42 +    Differences from HOL:
    7.43        (1) no checking if the induction var occurs in premises, since it always
    7.44            appears in one of them, and it's hard to check for other occurrences
    7.45        (2) exhaustion works for VARIABLES in the premises, not general terms
    7.46 @@ -112,16 +109,16 @@
    7.47      val (_, _, Bi, _) = dest_state (state, i)
    7.48      val {sign, ...} = rep_thm state
    7.49      val tn = find_tname var Bi
    7.50 -    val rule = 
    7.51 -	if exh then #exhaustion (datatype_info_sg sign tn)
    7.52 -	       else #induct  (datatype_info_sg sign tn)
    7.53 -    val (Const("op :",_) $ Var(ixn,_) $ _) = 
    7.54 +    val rule =
    7.55 +        if exh then #exhaustion (datatype_info_sg sign tn)
    7.56 +               else #induct  (datatype_info_sg sign tn)
    7.57 +    val (Const("op :",_) $ Var(ixn,_) $ _) =
    7.58          (case prems_of rule of
    7.59 -	     [] => error "induction is not available for this datatype"
    7.60 -	   | major::_ => FOLogic.dest_Trueprop major)
    7.61 +             [] => error "induction is not available for this datatype"
    7.62 +           | major::_ => FOLogic.dest_Trueprop major)
    7.63      val ind_vname = Syntax.string_of_vname ixn
    7.64      val vname' = (*delete leading question mark*)
    7.65 -	String.substring (ind_vname, 1, size ind_vname-1)
    7.66 +        String.substring (ind_vname, 1, size ind_vname-1)
    7.67    in
    7.68      eres_inst_tac [(vname',var)] rule i state
    7.69    end;
    7.70 @@ -140,55 +137,63 @@
    7.71      (*analyze the LHS of a case equation to get a constructor*)
    7.72      fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
    7.73        | const_of eqn = error ("Ill-formed case equation: " ^
    7.74 -			      Sign.string_of_term sign eqn);
    7.75 +                              Sign.string_of_term sign eqn);
    7.76  
    7.77      val constructors =
    7.78 -	map (head_of o const_of o FOLogic.dest_Trueprop o
    7.79 -	     #prop o rep_thm) case_eqns;
    7.80 +        map (head_of o const_of o FOLogic.dest_Trueprop o
    7.81 +             #prop o rep_thm) case_eqns;
    7.82  
    7.83      val Const ("op :", _) $ _ $ data =
    7.84 -	FOLogic.dest_Trueprop (hd (prems_of elim));	
    7.85 -    
    7.86 +        FOLogic.dest_Trueprop (hd (prems_of elim));
    7.87 +
    7.88      val Const(big_rec_name, _) = head_of data;
    7.89  
    7.90      val simps = case_eqns @ recursor_eqns;
    7.91  
    7.92      val dt_info =
    7.93 -	  {inductive = true,
    7.94 -	   constructors = constructors,
    7.95 -	   rec_rewrites = recursor_eqns,
    7.96 -	   case_rewrites = case_eqns,
    7.97 -	   induct = induct,
    7.98 -	   mutual_induct = TrueI,  (*No need for mutual induction*)
    7.99 -	   exhaustion = elim};
   7.100 +          {inductive = true,
   7.101 +           constructors = constructors,
   7.102 +           rec_rewrites = recursor_eqns,
   7.103 +           case_rewrites = case_eqns,
   7.104 +           induct = induct,
   7.105 +           mutual_induct = TrueI,  (*No need for mutual induction*)
   7.106 +           exhaustion = elim};
   7.107  
   7.108      val con_info =
   7.109 -	  {big_rec_name = big_rec_name,
   7.110 -	   constructors = constructors,
   7.111 -	      (*let primrec handle definition by cases*)
   7.112 -	   free_iffs = [],  (*thus we expect the necessary freeness rewrites
   7.113 -			      to be in the simpset already, as is the case for
   7.114 -			      Nat and disjoint sum*)
   7.115 -	   rec_rewrites = (case recursor_eqns of
   7.116 -			       [] => case_eqns | _ => recursor_eqns)};
   7.117 +          {big_rec_name = big_rec_name,
   7.118 +           constructors = constructors,
   7.119 +              (*let primrec handle definition by cases*)
   7.120 +           free_iffs = [],  (*thus we expect the necessary freeness rewrites
   7.121 +                              to be in the simpset already, as is the case for
   7.122 +                              Nat and disjoint sum*)
   7.123 +           rec_rewrites = (case recursor_eqns of
   7.124 +                               [] => case_eqns | _ => recursor_eqns)};
   7.125  
   7.126      (*associate with each constructor the datatype name and rewrites*)
   7.127      val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
   7.128  
   7.129    in
   7.130        thy |> Theory.add_path (Sign.base_name big_rec_name)
   7.131 -	  |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   7.132 -	  |> DatatypesData.put 
   7.133 -	      (Symtab.update
   7.134 -	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
   7.135 -	  |> ConstructorsData.put
   7.136 -	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   7.137 -	  |> Theory.parent_path
   7.138 +          |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   7.139 +          |> DatatypesData.put
   7.140 +              (Symtab.update
   7.141 +               ((big_rec_name, dt_info), DatatypesData.get thy))
   7.142 +          |> ConstructorsData.put
   7.143 +               (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
   7.144 +          |> Theory.parent_path
   7.145    end
   7.146    handle exn => (writeln "Failure in rep_datatype"; raise exn);
   7.147  
   7.148  end;
   7.149  
   7.150 -
   7.151  val exhaust_tac = DatatypeTactics.exhaust_tac;
   7.152  val induct_tac  = DatatypeTactics.induct_tac;
   7.153 +
   7.154 +val induct_tacs_setup =
   7.155 + [DatatypesData.init,
   7.156 +  ConstructorsData.init,
   7.157 +  Method.add_methods
   7.158 +    [("induct_tac", Method.goal_args Args.name induct_tac,
   7.159 +      "induct_tac emulation (dynamic instantiation!)"),
   7.160 +     ("case_tac", Method.goal_args Args.name case_tac,
   7.161 +      "case_tac emulation (dynamic instantiation!)")]];
     8.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Nov 13 22:20:15 2001 +0100
     8.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Nov 13 22:20:51 2001 +0100
     8.3 @@ -56,9 +56,6 @@
     8.4  fun mk_frees a [] = []
     8.5    | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
     8.6  
     8.7 -(*read an assumption in the given theory*)
     8.8 -fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT));
     8.9 -
    8.10  
    8.11  (* add_inductive(_i) *)
    8.12  
    8.13 @@ -277,16 +274,14 @@
    8.14    (*Applies freeness of the given constructors, which *must* be unfolded by
    8.15        the given defs.  Cannot simply use the local con_defs because
    8.16        con_defs=[] for inference systems.
    8.17 -    String s should have the form t:Si where Si is an inductive set*)
    8.18 -  fun mk_cases s =
    8.19 -      rule_by_tactic (basic_elim_tac THEN
    8.20 -                      ALLGOALS Asm_full_simp_tac THEN
    8.21 -                      basic_elim_tac)
    8.22 -         (assume_read (theory_of_thm elim) s
    8.23 -                      (*Don't use thy1: it will be stale*)
    8.24 -          RS  elim)
    8.25 -      |> standard;
    8.26 -
    8.27 +    Proposition A should have the form t:Si where Si is an inductive set*)
    8.28 +  fun make_cases ss A =
    8.29 +    rule_by_tactic
    8.30 +      (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
    8.31 +      (Thm.assume A RS elim)
    8.32 +      |> Drule.standard';
    8.33 +  fun mk_cases a = make_cases (*delayed evaluation of body!*)
    8.34 +    (simpset ()) (read_cterm (Thm.sign_of_thm elim) (a, propT));
    8.35  
    8.36    fun induction_rules raw_induct thy =
    8.37     let
    8.38 @@ -527,8 +522,10 @@
    8.39                    |> standard
    8.40       and mutual_induct = CP.remove_split mutual_induct_fsplit
    8.41  
    8.42 +     val induct_att =
    8.43 +       (case rec_names of [name] => [InductAttrib.induct_set_global name] | _ => []);
    8.44       val (thy', [induct', mutual_induct']) =
    8.45 -        thy |> PureThy.add_thms [(("induct", induct), [InductAttrib.induct_set_global ""]),
    8.46 +        thy |> PureThy.add_thms [(("induct", induct), induct_att),
    8.47            (("mutual_induct", mutual_induct), [])];
    8.48      in (thy', induct', mutual_induct')
    8.49      end;  (*of induction_rules*)
    8.50 @@ -549,11 +546,11 @@
    8.51         (("cases", elim), [InductAttrib.cases_set_global ""])]
    8.52      |>>> (PureThy.add_thmss o map Thm.no_attributes)
    8.53          [("defs", defs),
    8.54 -         ("intros", intrs)]
    8.55 -    |>> Theory.parent_path;
    8.56 +         ("intros", intrs)];
    8.57    val (thy4, intrs'') =
    8.58      thy3 |> PureThy.add_thms
    8.59 -      (map2 (fn (((bname, _), atts), th) => ((bname, th), atts)) (intr_specs, intrs'));
    8.60 +      (map2 (fn (((bname, _), atts), th) => ((bname, th), atts)) (intr_specs, intrs'))
    8.61 +    |>> Theory.parent_path;
    8.62    in
    8.63      (thy4,
    8.64        {defs = defs',