1821 in do_term 0 [] end |
1821 in do_term 0 [] end |
1822 |
1822 |
1823 (** Axiom extraction/generation **) |
1823 (** Axiom extraction/generation **) |
1824 |
1824 |
1825 fun extensional_equal j T t1 t2 = |
1825 fun extensional_equal j T t1 t2 = |
1826 if is_fun_or_set_type T then |
1826 if is_fun_type T then |
1827 let |
1827 let |
1828 val dom_T = pseudo_domain_type T |
1828 val dom_T = pseudo_domain_type T |
1829 val ran_T = pseudo_range_type T |
1829 val ran_T = pseudo_range_type T |
1830 val var_t = Var (("x", j), dom_T) |
1830 val var_t = Var (("x", j), dom_T) |
1831 fun apply fun_t arg_t = |
1831 in |
1832 if is_fun_type T then |
1832 extensional_equal (j + 1) ran_T (betapply (t1, var_t)) |
1833 betapply (fun_t, arg_t) |
1833 (betapply (t2, var_t)) |
1834 else |
1834 end |
1835 Const (@{const_name Set.member}, dom_T --> T --> ran_T) |
|
1836 $ arg_t $ fun_t |
|
1837 in extensional_equal (j + 1) ran_T (apply t1 var_t) (apply t2 var_t) end |
|
1838 else |
1835 else |
1839 Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2 |
1836 Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2 |
1840 |
1837 |
1841 (* FIXME: needed? *) |
1838 (* FIXME: needed? *) |
1842 fun equationalize_term ctxt tag t = |
1839 fun equationalize_term ctxt tag t = |