src/ZF/Tools/inductive_package.ML
changeset 32765 3032c0308019
parent 32091 30e2ffbba718
child 32957 675c0c7e6a37
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
   111     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
   111     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
   112         val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
   112         val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
   113         val exfrees = OldTerm.term_frees intr \\ rec_params
   113         val exfrees = OldTerm.term_frees intr \\ rec_params
   114         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   114         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   115     in List.foldr FOLogic.mk_exists
   115     in List.foldr FOLogic.mk_exists
   116              (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
   116              (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
   117     end;
   117     end;
   118 
   118 
   119   (*The Part(A,h) terms -- compose injections to make h*)
   119   (*The Part(A,h) terms -- compose injections to make h*)
   120   fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
   120   fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
   121     | mk_Part h         = @{const Part} $ Free(X',iT) $ Abs(w',iT,h);
   121     | mk_Part h         = @{const Part} $ Free(X',iT) $ Abs(w',iT,h);
   122 
   122 
   123   (*Access to balanced disjoint sums via injections*)
   123   (*Access to balanced disjoint sums via injections*)
   124   val parts = map mk_Part
   124   val parts = map mk_Part
   125     (BalancedTree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
   125     (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
   126       (length rec_tms));
   126       (length rec_tms));
   127 
   127 
   128   (*replace each set by the corresponding Part(A,h)*)
   128   (*replace each set by the corresponding Part(A,h)*)
   129   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
   129   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
   130 
   130 
   131   val fp_abs = absfree(X', iT,
   131   val fp_abs = absfree(X', iT,
   132                    mk_Collect(z', dom_sum,
   132                    mk_Collect(z', dom_sum,
   133                               BalancedTree.make FOLogic.mk_disj part_intrs));
   133                               Balanced_Tree.make FOLogic.mk_disj part_intrs));
   134 
   134 
   135   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
   135   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
   136 
   136 
   137   val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso
   137   val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso
   138                              error "Illegal occurrence of recursion operator"; ()))
   138                              error "Illegal occurrence of recursion operator"; ()))
   236      if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
   236      if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
   237      else all_tac,
   237      else all_tac,
   238      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   238      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   239 
   239 
   240   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   240   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   241   val mk_disj_rls = BalancedTree.accesses
   241   val mk_disj_rls = Balanced_Tree.accesses
   242     {left = fn rl => rl RS @{thm disjI1},
   242     {left = fn rl => rl RS @{thm disjI1},
   243      right = fn rl => rl RS @{thm disjI2},
   243      right = fn rl => rl RS @{thm disjI2},
   244      init = @{thm asm_rl}};
   244      init = @{thm asm_rl}};
   245 
   245 
   246   val intrs =
   246   val intrs =
   396      val induct_concl =
   396      val induct_concl =
   397          FOLogic.mk_Trueprop
   397          FOLogic.mk_Trueprop
   398            (Ind_Syntax.mk_all_imp
   398            (Ind_Syntax.mk_all_imp
   399             (big_rec_tm,
   399             (big_rec_tm,
   400              Abs("z", Ind_Syntax.iT,
   400              Abs("z", Ind_Syntax.iT,
   401                  BalancedTree.make FOLogic.mk_conj
   401                  Balanced_Tree.make FOLogic.mk_conj
   402                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
   402                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
   403      and mutual_induct_concl =
   403      and mutual_induct_concl =
   404       FOLogic.mk_Trueprop(BalancedTree.make FOLogic.mk_conj qconcls);
   404       FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
   405 
   405 
   406      val dummy = if !Ind_Syntax.trace then
   406      val dummy = if !Ind_Syntax.trace then
   407                  (writeln ("induct_concl = " ^
   407                  (writeln ("induct_concl = " ^
   408                            Syntax.string_of_term ctxt1 induct_concl);
   408                            Syntax.string_of_term ctxt1 induct_concl);
   409                   writeln ("mutual_induct_concl = " ^
   409                   writeln ("mutual_induct_concl = " ^