107 fun fp_part intr = (*quantify over rule's free vars except parameters*) |
107 fun fp_part intr = (*quantify over rule's free vars except parameters*) |
108 let val prems = map dest_tprop (Logic.strip_imp_prems intr) |
108 let val prems = map dest_tprop (Logic.strip_imp_prems intr) |
109 val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds |
109 val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds |
110 val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr) |
110 val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr) |
111 val zeq = FOLogic.mk_eq (Free(z', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr)) |
111 val zeq = FOLogic.mk_eq (Free(z', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr)) |
112 in List.foldr FOLogic.mk_exists |
112 in |
113 (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees |
113 fold_rev (FOLogic.mk_exists o Term.dest_Free) exfrees |
|
114 (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) |
114 end; |
115 end; |
115 |
116 |
116 (*The Part(A,h) terms -- compose injections to make h*) |
117 (*The Part(A,h) terms -- compose injections to make h*) |
117 fun mk_Part (Bound 0) = Free(X', \<^Type>\<open>i\<close>) (*no mutual rec, no Part needed*) |
118 fun mk_Part (Bound 0) = Free(X', \<^Type>\<open>i\<close>) (*no mutual rec, no Part needed*) |
118 | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', \<^Type>\<open>i\<close>) $ Abs (w', \<^Type>\<open>i\<close>, h); |
119 | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', \<^Type>\<open>i\<close>) $ Abs (w', \<^Type>\<open>i\<close>, h); |
387 fun mk_predpair rec_tm = |
388 fun mk_predpair rec_tm = |
388 let val rec_name = (#1 o dest_Const o head_of) rec_tm |
389 let val rec_name = (#1 o dest_Const o head_of) rec_tm |
389 val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name, |
390 val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name, |
390 elem_factors ---> \<^Type>\<open>o\<close>) |
391 elem_factors ---> \<^Type>\<open>o\<close>) |
391 val qconcl = |
392 val qconcl = |
392 List.foldr FOLogic.mk_all |
393 fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees |
393 (\<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for elem_tuple rec_tm\<close> |
394 \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close> |
394 $ (list_comb (pfree, elem_frees))) elem_frees |
|
395 in (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree, |
395 in (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree, |
396 qconcl) |
396 qconcl) |
397 end; |
397 end; |
398 |
398 |
399 val (preds,qconcls) = split_list (map mk_predpair rec_tms); |
399 val (preds,qconcls) = split_list (map mk_predpair rec_tms); |
400 |
400 |
401 (*Used to form simultaneous induction lemma*) |
401 (*Used to form simultaneous induction lemma*) |
402 fun mk_rec_imp (rec_tm,pred) = |
402 fun mk_rec_imp (rec_tm,pred) = |
403 \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0); |
403 \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>; |
404 |
404 |
405 (*To instantiate the main induction rule*) |
405 (*To instantiate the main induction rule*) |
406 val induct_concl = |
406 val induct_concl = |
407 FOLogic.mk_Trueprop |
407 FOLogic.mk_Trueprop |
408 (Ind_Syntax.mk_all_imp |
408 (Ind_Syntax.mk_all_imp |