equal
deleted
inserted
replaced
102 EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
102 EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m |
103 | [exclude] => different_case_tac ctxt m exclude) |
103 | [exclude] => different_case_tac ctxt m exclude) |
104 (take k (nth excludesss (k - 1)))) |
104 (take k (nth excludesss (k - 1)))) |
105 end; |
105 end; |
106 |
106 |
107 fun prelude_tac ctxt defs thm = |
107 fun prelude_tac ctxt fun_defs thm = |
108 unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets; |
108 unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets; |
109 |
109 |
110 fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss = |
110 fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss = |
111 prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss; |
111 prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss; |
112 |
112 |
113 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss |
113 fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss |
114 distinct_discs = |
114 distinct_discs = |
115 HEADGOAL (rtac ctxt iffI THEN' |
115 HEADGOAL (rtac ctxt iffI THEN' |
116 rtac ctxt fun_exhaust THEN' |
116 rtac ctxt fun_exhaust THEN' |
127 fun_discss) THEN' |
127 fun_discss) THEN' |
128 (etac ctxt FalseE ORELSE' |
128 (etac ctxt FalseE ORELSE' |
129 resolve_tac ctxt |
129 resolve_tac ctxt |
130 (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt)); |
130 (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt)); |
131 |
131 |
132 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k |
132 fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps |
133 m excludesss = |
133 fun_sel k m excludesss = |
134 prelude_tac ctxt defs (fun_sel RS trans) THEN |
134 prelude_tac ctxt fun_defs (fun_sel RS trans) THEN |
135 cases_tac ctxt k m excludesss THEN |
135 cases_tac ctxt k m excludesss THEN |
136 HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
136 HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE' |
137 eresolve_tac ctxt falseEs ORELSE' |
137 eresolve_tac ctxt falseEs ORELSE' |
138 resolve_tac ctxt split_connectI ORELSE' |
138 resolve_tac ctxt split_connectI ORELSE' |
139 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |
139 Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE' |