39 Free _ => t (*but not existing Vars, lest the names clash*) |
39 Free _ => t (*but not existing Vars, lest the names clash*) |
40 | Bound _ => t |
40 | Bound _ => t |
41 | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of |
41 | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of |
42 Some v => v |
42 Some v => v |
43 | None => insert t) |
43 | None => insert t) |
|
44 (*abstraction of a numeric literal*) |
|
45 fun lit (t as Const("0", _)) = t |
|
46 | lit (t as Const("1", _)) = t |
|
47 | lit (t as Const("Numeral.number_of", _) $ w) = t |
|
48 | lit t = replace t |
44 (*abstraction of a real/rational expression*) |
49 (*abstraction of a real/rational expression*) |
45 fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y) |
50 fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y) |
46 | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y) |
51 | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y) |
47 | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y) |
52 | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y) |
48 | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y) |
53 | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y) |
49 | rat ((c as Const("uminus", _)) $ x) = c $ (rat x) |
54 | rat ((c as Const("uminus", _)) $ x) = c $ (rat x) |
50 | rat ((c as Const("0", _))) = c |
55 | rat t = lit t |
51 | rat ((c as Const("1", _))) = c |
|
52 | rat (t as Const("Numeral.number_of", _) $ w) = t |
|
53 | rat t = replace t |
|
54 (*abstraction of an integer expression: no div, mod*) |
56 (*abstraction of an integer expression: no div, mod*) |
55 fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y) |
57 fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y) |
56 | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y) |
58 | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y) |
57 | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y) |
59 | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y) |
58 | int ((c as Const("uminus", _)) $ x) = c $ (int x) |
60 | int ((c as Const("uminus", _)) $ x) = c $ (int x) |
59 | int (t as Const("Numeral.number_of", _) $ w) = t |
61 | int t = lit t |
60 | int t = replace t |
|
61 (*abstraction of a natural number expression: no minus*) |
62 (*abstraction of a natural number expression: no minus*) |
62 fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y) |
63 fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y) |
63 | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y) |
64 | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y) |
64 | nat ((c as Const("Suc", _)) $ x) = c $ (nat x) |
65 | nat ((c as Const("Suc", _)) $ x) = c $ (nat x) |
65 | nat (t as Const("0", _)) = t |
66 | nat t = lit t |
66 | nat (t as Const("Numeral.number_of", _) $ w) = t |
|
67 | nat t = replace t |
|
68 (*abstraction of a relation: =, <, <=*) |
67 (*abstraction of a relation: =, <, <=*) |
69 fun rel (T, c $ x $ y) = |
68 fun rel (T, c $ x $ y) = |
70 if T = HOLogic.realT then c $ (rat x) $ (rat y) |
69 if T = HOLogic.realT then c $ (rat x) $ (rat y) |
71 else if T = HOLogic.intT then c $ (int x) $ (int y) |
70 else if T = HOLogic.intT then c $ (int x) $ (int y) |
72 else if T = HOLogic.natT then c $ (nat x) $ (nat y) |
71 else if T = HOLogic.natT then c $ (nat x) $ (nat y) |