equal
deleted
inserted
replaced
1 (* Title: HOL/BNF/BNF_FP_Rec_Sugar.thy |
|
2 Author: Lorenz Panny, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Author: Dmitriy Traytel, TU Muenchen |
|
5 Copyright 2013 |
|
6 |
|
7 Recursor and corecursor sugar. |
|
8 *) |
|
9 |
|
10 header {* Recursor and Corecursor Sugar *} |
|
11 |
|
12 theory BNF_FP_Rec_Sugar |
|
13 imports BNF_FP_N2M |
|
14 keywords |
|
15 "primrec_new" :: thy_decl and |
|
16 "primcorec" :: thy_goal and |
|
17 "sequential" |
|
18 begin |
|
19 |
|
20 lemma if_if_True: |
|
21 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = |
|
22 (if b then x else if b' then x' else f y')" |
|
23 by simp |
|
24 |
|
25 lemma if_if_False: |
|
26 "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) = |
|
27 (if b then f y else if b' then x' else f y')" |
|
28 by simp |
|
29 |
|
30 ML_file "Tools/bnf_fp_rec_sugar_util.ML" |
|
31 ML_file "Tools/bnf_fp_rec_sugar_tactics.ML" |
|
32 ML_file "Tools/bnf_fp_rec_sugar.ML" |
|
33 |
|
34 end |
|