equal
deleted
inserted
replaced
57 val s_disjs: term list -> term |
57 val s_disjs: term list -> term |
58 val s_dnf: term list list -> term list |
58 val s_dnf: term list list -> term list |
59 |
59 |
60 val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
60 val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
61 typ list -> term -> term -> term -> term |
61 typ list -> term -> term -> term -> term |
|
62 val unfold_let: term -> term |
62 val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> |
63 val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> |
63 typ list -> term -> term |
64 typ list -> term -> term |
64 val massage_indirect_corec_call: Proof.context -> (term -> bool) -> |
65 val massage_indirect_corec_call: Proof.context -> (term -> bool) -> |
65 (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term |
66 (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term |
66 val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term |
67 val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term |
280 end |
281 end |
281 | _ => apsnd (f conds t)) |
282 | _ => apsnd (f conds t)) |
282 in |
283 in |
283 fld [] t o pair [] |
284 fld [] t o pair [] |
284 end; |
285 end; |
|
286 |
|
287 fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1)) |
|
288 | unfold_let t = t; |
285 |
289 |
286 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex); |
290 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex); |
287 |
291 |
288 fun massage_let_if_case ctxt has_call massage_leaf = |
292 fun massage_let_if_case ctxt has_call massage_leaf = |
289 let |
293 let |