86 (* make a casethm from an induction thm *) |
86 (* make a casethm from an induction thm *) |
87 val cases_thm_of_induct_thm = |
87 val cases_thm_of_induct_thm = |
88 Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); |
88 Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); |
89 |
89 |
90 (* get the case_thm (my version) from a type *) |
90 (* get the case_thm (my version) from a type *) |
91 fun case_thm_of_ty sgn ty = |
91 fun case_thm_of_ty thy ty = |
92 let |
92 let |
93 val dtypestab = Datatype.get_datatypes sgn; |
|
94 val ty_str = case ty of |
93 val ty_str = case ty of |
95 Type(ty_str, _) => ty_str |
94 Type(ty_str, _) => ty_str |
96 | TFree(s,_) => error ("Free type: " ^ s) |
95 | TFree(s,_) => error ("Free type: " ^ s) |
97 | TVar((s,i),_) => error ("Free variable: " ^ s) |
96 | TVar((s,i),_) => error ("Free variable: " ^ s) |
98 val dt = case Symtab.lookup dtypestab ty_str |
97 val dt = Datatype.the_info thy ty_str |
99 of SOME dt => dt |
|
100 | NONE => error ("Not a Datatype: " ^ ty_str) |
|
101 in |
98 in |
102 cases_thm_of_induct_thm (#induction dt) |
99 cases_thm_of_induct_thm (#induction dt) |
103 end; |
100 end; |
104 |
101 |
105 (* |
102 (* |