3076 |
3076 |
3077 (* pat matched with the current term gives an environment |
3077 (* pat matched with the current term gives an environment |
3078 (or not: hen the Rrls not applied); |
3078 (or not: hen the Rrls not applied); |
3079 if pre1 and pre2 evaluate to HOLogic.true_const in this environment, |
3079 if pre1 and pre2 evaluate to HOLogic.true_const in this environment, |
3080 then the Rrls is applied. *) |
3080 then the Rrls is applied. *) |
3081 val pat = parse_patt thy "?r/?s"; |
3081 val pat = parse_patt thy "?r/?s :: real"; |
3082 val pre1 = parse_patt thy "?r is_expanded"; |
3082 val pre1 = parse_patt thy "?r is_expanded"; |
3083 val pre2 = parse_patt thy "?s is_expanded"; |
3083 val pre2 = parse_patt thy "?s is_expanded"; |
3084 val prepat = [([pre1, pre2], pat)]; |
3084 val prepat = [([pre1, pre2], pat)]; |
3085 |
3085 |
3086 in |
3086 in |
3226 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3226 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3227 []:(rule * (term * term list)) list; |
3227 []:(rule * (term * term list)) list; |
3228 |
3228 |
3229 (* if each pat* matches with the current term, the Rrls is applied |
3229 (* if each pat* matches with the current term, the Rrls is applied |
3230 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3230 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3231 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3231 val pat0 = parse_patt thy "?r/?s+?u/?v :: real"; |
3232 val pat1 = parse_patt thy "?r/?s+?u "; |
3232 val pat1 = parse_patt thy "?r/?s+?u :: real"; |
3233 val pat2 = parse_patt thy "?r +?u/?v"; |
3233 val pat2 = parse_patt thy "?r +?u/?v :: real"; |
3234 val prepat = [([HOLogic.true_const], pat0), |
3234 val prepat = [([HOLogic.true_const], pat0), |
3235 ([HOLogic.true_const], pat1), |
3235 ([HOLogic.true_const], pat1), |
3236 ([HOLogic.true_const], pat2)]; |
3236 ([HOLogic.true_const], pat2)]; |
3237 in |
3237 in |
3238 |
3238 |
3371 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3371 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
3372 []:(rule * (term * term list)) list; |
3372 []:(rule * (term * term list)) list; |
3373 |
3373 |
3374 (* if each pat* matches with the current term, the Rrls is applied |
3374 (* if each pat* matches with the current term, the Rrls is applied |
3375 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3375 (there are no preconditions to be checked, they are HOLogic.true_const) *) |
3376 val pat0 = parse_patt thy "?r/?s+?u/?v"; |
3376 val pat0 = parse_patt thy "?r/?s+?u/?v :: real"; |
3377 val pat01 = parse_patt thy "?r/?s-?u/?v"; |
3377 val pat01 = parse_patt thy "?r/?s-?u/?v :: real"; |
3378 val pat1 = parse_patt thy "?r/?s+?u "; |
3378 val pat1 = parse_patt thy "?r/?s+?u :: real"; |
3379 val pat11 = parse_patt thy "?r/?s-?u "; |
3379 val pat11 = parse_patt thy "?r/?s-?u :: real"; |
3380 val pat2 = parse_patt thy "?r +?u/?v"; |
3380 val pat2 = parse_patt thy "?r +?u/?v :: real"; |
3381 val pat21 = parse_patt thy "?r -?u/?v"; |
3381 val pat21 = parse_patt thy "?r -?u/?v :: real"; |
3382 val prepat = [([HOLogic.true_const], pat0), |
3382 val prepat = [([HOLogic.true_const], pat0), |
3383 ([HOLogic.true_const], pat01), |
3383 ([HOLogic.true_const], pat01), |
3384 ([HOLogic.true_const], pat1), |
3384 ([HOLogic.true_const], pat1), |
3385 ([HOLogic.true_const], pat11), |
3385 ([HOLogic.true_const], pat11), |
3386 ([HOLogic.true_const], pat2), |
3386 ([HOLogic.true_const], pat2), |