55 quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions |
55 quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions |
56 for destructing quotient theorems (Quotient R Abs Rep T). |
56 for destructing quotient theorems (Quotient R Abs Rep T). |
57 *) |
57 *) |
58 |
58 |
59 fun quot_thm_rel quot_thm = |
59 fun quot_thm_rel quot_thm = |
60 case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of |
60 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
61 (rel, _, _, _) => rel |
61 (rel, _, _, _) => rel |
62 |
62 |
63 fun quot_thm_abs quot_thm = |
63 fun quot_thm_abs quot_thm = |
64 case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of |
64 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
65 (_, abs, _, _) => abs |
65 (_, abs, _, _) => abs |
66 |
66 |
67 fun quot_thm_rep quot_thm = |
67 fun quot_thm_rep quot_thm = |
68 case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of |
68 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
69 (_, _, rep, _) => rep |
69 (_, _, rep, _) => rep |
70 |
70 |
71 fun quot_thm_crel quot_thm = |
71 fun quot_thm_crel quot_thm = |
72 case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of |
72 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
73 (_, _, _, crel) => crel |
73 (_, _, _, crel) => crel |
74 |
74 |
75 fun quot_thm_rty_qty quot_thm = |
75 fun quot_thm_rty_qty quot_thm = |
76 let |
76 let |
77 val abs = quot_thm_abs quot_thm |
77 val abs = quot_thm_abs quot_thm |
85 val assm = Thm.cprem_of thm 1 |
85 val assm = Thm.cprem_of thm 1 |
86 in |
86 in |
87 Thm.implies_elim thm (Thm.assume assm) |
87 Thm.implies_elim thm (Thm.assume assm) |
88 end |
88 end |
89 |
89 |
90 fun undisch_all thm = funpow (nprems_of thm) undisch thm |
90 fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm |
91 |
91 |
92 fun is_fun_type (Type (@{type_name fun}, _)) = true |
92 fun is_fun_type (Type (@{type_name fun}, _)) = true |
93 | is_fun_type _ = false |
93 | is_fun_type _ = false |
94 |
94 |
95 fun get_args n = rev o fst o funpow_yield n (swap o dest_comb) |
95 fun get_args n = rev o fst o funpow_yield n (swap o dest_comb) |