Now mutual_induct is simply "True" unless it is going to be
authorpaulson
Thu Dec 28 11:59:15 1995 +0100 (1995-12-28)
changeset 1424ccb3c5ff6707
parent 1423 5726a8243d3f
child 1425 7b61bcfeaa95
Now mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.
src/HOL/indrule.ML
     1.1 --- a/src/HOL/indrule.ML	Thu Dec 28 11:54:15 1995 +0100
     1.2 +++ b/src/HOL/indrule.ML	Thu Dec 28 11:59:15 1995 +0100
     1.3 @@ -17,16 +17,15 @@
     1.4  
     1.5  functor Indrule_Fun
     1.6      (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end and
     1.7 -	 Intr_elim: INTR_ELIM) : INDRULE  =
     1.8 -struct
     1.9 -open Logic Ind_Syntax Inductive Intr_elim;
    1.10 +	 Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
    1.11 +let
    1.12 +
    1.13 +val sign = sign_of Inductive.thy;
    1.14  
    1.15 -val sign = sign_of thy;
    1.16 +val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms);
    1.17  
    1.18 -val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    1.19 -
    1.20 -val elem_type = dest_setT (body_type recT);
    1.21 -val big_rec_name = space_implode "_" rec_names;
    1.22 +val elem_type = Ind_Syntax.dest_setT (body_type recT);
    1.23 +val big_rec_name = space_implode "_" Intr_elim.rec_names;
    1.24  val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
    1.25  
    1.26  val _ = writeln "  Proving the induction rule...";
    1.27 @@ -43,12 +42,13 @@
    1.28  fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 
    1.29  		 (Const("op :",_)$t$X), iprems) =
    1.30       (case gen_assoc (op aconv) (ind_alist, X) of
    1.31 -	  Some pred => prem :: mk_Trueprop (pred $ t) :: iprems
    1.32 +	  Some pred => prem :: Ind_Syntax.mk_Trueprop (pred $ t) :: iprems
    1.33  	| None => (*possibly membership in M(rec_tm), for M monotone*)
    1.34  	    let fun mk_sb (rec_tm,pred) = 
    1.35  		 (case binder_types (fastype_of pred) of
    1.36  		      [T] => (rec_tm, 
    1.37 -			      Int_const T $ rec_tm $ (Collect_const T $ pred))
    1.38 +			      Ind_Syntax.Int_const T $ rec_tm $ 
    1.39 +			        (Ind_Syntax.Collect_const T $ pred))
    1.40  		    | _ => error 
    1.41  		      "Bug: add_induct_prem called with non-unary predicate")
    1.42  	    in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
    1.43 @@ -58,11 +58,11 @@
    1.44  fun induct_prem ind_alist intr =
    1.45    let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
    1.46        val iprems = foldr (add_induct_prem ind_alist)
    1.47 -			 (strip_imp_prems intr,[])
    1.48 -      val (t,X) = rule_concl intr
    1.49 +			 (Logic.strip_imp_prems intr,[])
    1.50 +      val (t,X) = Ind_Syntax.rule_concl intr
    1.51        val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
    1.52 -      val concl = mk_Trueprop (pred $ t)
    1.53 -  in list_all_free (quantfrees, list_implies (iprems,concl)) end
    1.54 +      val concl = Ind_Syntax.mk_Trueprop (pred $ t)
    1.55 +  in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
    1.56    handle Bind => error"Recursion term not found in conclusion";
    1.57  
    1.58  (*Avoids backtracking by delivering the correct premise to each goal*)
    1.59 @@ -71,9 +71,10 @@
    1.60  	DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN
    1.61  	ind_tac prems (i-1);
    1.62  
    1.63 -val pred = Free(pred_name, elem_type --> boolT);
    1.64 +val pred = Free(pred_name, elem_type --> Ind_Syntax.boolT);
    1.65  
    1.66 -val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
    1.67 +val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
    1.68 +                    Inductive.intr_tms;
    1.69  
    1.70  (*Debugging code...
    1.71  val _ = writeln "ind_prems = ";
    1.72 @@ -82,11 +83,13 @@
    1.73  
    1.74  val quant_induct = 
    1.75      prove_goalw_cterm part_rec_defs 
    1.76 -      (cterm_of sign (list_implies (ind_prems, 
    1.77 -				mk_Trueprop (mk_all_imp (big_rec_tm,pred)))))
    1.78 +      (cterm_of sign 
    1.79 +       (Logic.list_implies (ind_prems, 
    1.80 +			    Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp 
    1.81 +						    (big_rec_tm,pred)))))
    1.82        (fn prems =>
    1.83         [rtac (impI RS allI) 1,
    1.84 -	DETERM (etac raw_induct 1),
    1.85 +	DETERM (etac Intr_elim.raw_induct 1),
    1.86  	asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1,
    1.87  	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
    1.88  			   ORELSE' hyp_subst_tac)),
    1.89 @@ -102,34 +105,40 @@
    1.90    and a conclusion for the simultaneous induction rule*)
    1.91  fun mk_predpair rec_tm = 
    1.92    let val rec_name = (#1 o dest_Const o head_of) rec_tm
    1.93 -      val T = factors elem_type ---> boolT
    1.94 +      val T = Ind_Syntax.factors elem_type ---> Ind_Syntax.boolT
    1.95        val pfree = Free(pred_name ^ "_" ^ rec_name, T)
    1.96        val frees = mk_frees "za" (binder_types T)
    1.97        val qconcl = 
    1.98 -	foldr mk_all (frees, 
    1.99 -		      imp $ (mk_mem (foldr1 mk_Pair frees, rec_tm))
   1.100 -			  $ (list_comb (pfree,frees)))
   1.101 -  in  (ap_split boolT pfree (binder_types T), 
   1.102 +	foldr Ind_Syntax.mk_all 
   1.103 +	  (frees, 
   1.104 +	   Ind_Syntax.imp $ (Ind_Syntax.mk_mem 
   1.105 +			     (foldr1 Ind_Syntax.mk_Pair frees, rec_tm))
   1.106 +	        $ (list_comb (pfree,frees)))
   1.107 +  in  (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T), 
   1.108        qconcl)  
   1.109    end;
   1.110  
   1.111 -val (preds,qconcls) = split_list (map mk_predpair rec_tms);
   1.112 +val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
   1.113  
   1.114  (*Used to form simultaneous induction lemma*)
   1.115  fun mk_rec_imp (rec_tm,pred) = 
   1.116 -    imp $ (mk_mem (Bound 0, rec_tm)) $  (pred $ Bound 0);
   1.117 +    Ind_Syntax.imp $ (Ind_Syntax.mk_mem (Bound 0, rec_tm)) $  (pred $ Bound 0);
   1.118  
   1.119  (*To instantiate the main induction rule*)
   1.120  val induct_concl = 
   1.121 - mk_Trueprop(mk_all_imp(big_rec_tm,
   1.122 -		     Abs("z", elem_type, 
   1.123 -			 fold_bal (app conj) 
   1.124 -			          (map mk_rec_imp (rec_tms~~preds)))))
   1.125 -and mutual_induct_concl = mk_Trueprop(fold_bal (app conj) qconcls);
   1.126 +    Ind_Syntax.mk_Trueprop
   1.127 +      (Ind_Syntax.mk_all_imp
   1.128 +       (big_rec_tm,
   1.129 +	Abs("z", elem_type, 
   1.130 +	    fold_bal (app Ind_Syntax.conj) 
   1.131 +	    (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   1.132 +and mutual_induct_concl = 
   1.133 +    Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
   1.134  
   1.135  val lemma = (*makes the link between the two induction rules*)
   1.136      prove_goalw_cterm part_rec_defs 
   1.137 -	  (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
   1.138 +	  (cterm_of sign (Logic.mk_implies (induct_concl,
   1.139 +					    mutual_induct_concl)))
   1.140  	  (fn prems =>
   1.141  	   [cut_facts_tac prems 1,
   1.142  	    REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
   1.143 @@ -144,10 +153,11 @@
   1.144  val mut_ss = simpset_of "Fun"
   1.145               addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
   1.146  
   1.147 -val all_defs = con_defs@part_rec_defs;
   1.148 +val all_defs = Inductive.con_defs @ part_rec_defs;
   1.149  
   1.150  (*Removes Collects caused by M-operators in the intro rules*)
   1.151 -val cmonos = [subset_refl RS Int_Collect_mono] RL monos RLN (2,[rev_subsetD]);
   1.152 +val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
   1.153 +             (2,[rev_subsetD]);
   1.154  
   1.155  (*Avoids backtracking by delivering the correct premise to each goal*)
   1.156  fun mutual_ind_tac [] 0 = all_tac
   1.157 @@ -177,7 +187,8 @@
   1.158  val mutual_induct_split = 
   1.159      prove_goalw_cterm []
   1.160  	  (cterm_of sign
   1.161 -	   (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
   1.162 +	   (Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) 
   1.163 +			      Inductive.intr_tms,
   1.164  			  mutual_induct_concl)))
   1.165  	  (fn prems =>
   1.166  	   [rtac (quant_induct RS lemma) 1,
   1.167 @@ -192,9 +203,15 @@
   1.168  			      bound_hyp_subst_tac]))
   1.169      THEN prune_params_tac;
   1.170  
   1.171 -(*strip quantifier*)
   1.172 -val induct = standard (quant_induct RS spec RSN (2,rev_mp));
   1.173 +in
   1.174 +  struct
   1.175 +  (*strip quantifier*)
   1.176 +  val induct = standard (quant_induct RS spec RSN (2,rev_mp));
   1.177  
   1.178 -val mutual_induct = rule_by_tactic split_tac mutual_induct_split;
   1.179 -
   1.180 +  val mutual_induct = 
   1.181 +      if length Intr_elim.rec_names > 1 orelse
   1.182 +	 length (Ind_Syntax.factors elem_type) > 1
   1.183 +      then rule_by_tactic split_tac mutual_induct_split
   1.184 +      else TrueI;
   1.185 +  end
   1.186  end;