117 (*Makes a disjunct from an introduction rule*) |
117 (*Makes a disjunct from an introduction rule*) |
118 fun lfp_part intr = (*quantify over rule's free vars except parameters*) |
118 fun lfp_part intr = (*quantify over rule's free vars except parameters*) |
119 let val prems = map dest_tprop (strip_imp_prems intr) |
119 let val prems = map dest_tprop (strip_imp_prems intr) |
120 val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds |
120 val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds |
121 val exfrees = term_frees intr \\ rec_params |
121 val exfrees = term_frees intr \\ rec_params |
122 val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr)) |
122 val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr)) |
123 in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; |
123 in foldr FOLogic.mk_exists |
|
124 (exfrees, fold_bal (app FOLogic.conj) (zeq::prems)) |
|
125 end; |
124 |
126 |
125 (*The Part(A,h) terms -- compose injections to make h*) |
127 (*The Part(A,h) terms -- compose injections to make h*) |
126 fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) |
128 fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) |
127 | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); |
129 | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); |
128 |
130 |
133 |
135 |
134 (*replace each set by the corresponding Part(A,h)*) |
136 (*replace each set by the corresponding Part(A,h)*) |
135 val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; |
137 val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; |
136 |
138 |
137 val lfp_abs = absfree(X', iT, |
139 val lfp_abs = absfree(X', iT, |
138 mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs)); |
140 mk_Collect(z', dom_sum, |
|
141 fold_bal (app FOLogic.disj) part_intrs)); |
139 |
142 |
140 val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs |
143 val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs |
141 |
144 |
142 val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) |
145 val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) |
143 "Illegal occurrence of recursion operator") |
146 "Illegal occurrence of recursion operator") |