94 let |
94 let |
95 val thy = Proof_Context.theory_of ctxt |
95 val thy = Proof_Context.theory_of ctxt |
96 val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state |
96 val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state |
97 val tn = find_tname ctxt' var (map Thm.term_of asms) |
97 val tn = find_tname ctxt' var (map Thm.term_of asms) |
98 val rule = |
98 val rule = |
99 if exh then #exhaustion (datatype_info thy tn) |
99 datatype_info thy tn |
100 else #induct (datatype_info thy tn) |
100 |> (if exh then #exhaustion else #induct) |
|
101 |> Thm.transfer thy; |
101 val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) = |
102 val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) = |
102 (case Thm.prems_of rule of |
103 (case Thm.prems_of rule of |
103 [] => error "induction is not available for this datatype" |
104 [] => error "induction is not available for this datatype" |
104 | major::_ => FOLogic.dest_Trueprop major) |
105 | major::_ => FOLogic.dest_Trueprop major) |
105 in |
106 in |
134 val simps = case_eqns @ recursor_eqns; |
135 val simps = case_eqns @ recursor_eqns; |
135 |
136 |
136 val dt_info = |
137 val dt_info = |
137 {inductive = true, |
138 {inductive = true, |
138 constructors = constructors, |
139 constructors = constructors, |
139 rec_rewrites = recursor_eqns, |
140 rec_rewrites = map Thm.trim_context recursor_eqns, |
140 case_rewrites = case_eqns, |
141 case_rewrites = map Thm.trim_context case_eqns, |
141 induct = induct, |
142 induct = Thm.trim_context induct, |
142 mutual_induct = @{thm TrueI}, (*No need for mutual induction*) |
143 mutual_induct = Thm.trim_context @{thm TrueI}, (*No need for mutual induction*) |
143 exhaustion = elim}; |
144 exhaustion = Thm.trim_context elim}; |
144 |
145 |
145 val con_info = |
146 val con_info = |
146 {big_rec_name = big_rec_name, |
147 {big_rec_name = big_rec_name, |
147 constructors = constructors, |
148 constructors = constructors, |
148 (*let primrec handle definition by cases*) |
149 (*let primrec handle definition by cases*) |
149 free_iffs = [], (*thus we expect the necessary freeness rewrites |
150 free_iffs = [], (*thus we expect the necessary freeness rewrites |
150 to be in the simpset already, as is the case for |
151 to be in the simpset already, as is the case for |
151 Nat and disjoint sum*) |
152 Nat and disjoint sum*) |
152 rec_rewrites = (case recursor_eqns of |
153 rec_rewrites = |
153 [] => case_eqns | _ => recursor_eqns)}; |
154 (case recursor_eqns of [] => case_eqns | _ => recursor_eqns) |
|
155 |> map Thm.trim_context}; |
154 |
156 |
155 (*associate with each constructor the datatype name and rewrites*) |
157 (*associate with each constructor the datatype name and rewrites*) |
156 val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors |
158 val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors |
157 |
159 |
158 in |
160 in |