equal
deleted
inserted
replaced
1992 conversion as @{text "(K conv)"}, which is a function that ignores its |
1992 conversion as @{text "(K conv)"}, which is a function that ignores its |
1993 argument (the argument being a sufficiently freshened version of the |
1993 argument (the argument being a sufficiently freshened version of the |
1994 variable that is abstracted and a context). The conversion that goes under |
1994 variable that is abstracted and a context). The conversion that goes under |
1995 an application is @{ML [index] combination_conv in Conv}. It expects two |
1995 an application is @{ML [index] combination_conv in Conv}. It expects two |
1996 conversions as arguments, each of which is applied to the corresponding |
1996 conversions as arguments, each of which is applied to the corresponding |
1997 ``branch'' of the application. |
1997 ``branch'' of the application. An abbreviation for this conversion is the |
|
1998 function @{ML [index] comb_conv in Conv}, which applies the same conversion |
|
1999 to both branches. |
1998 |
2000 |
1999 We can now apply all these functions in a conversion that recursively |
2001 We can now apply all these functions in a conversion that recursively |
2000 descends a term and applies a ``@{thm [source] true_conj1}''-conversion |
2002 descends a term and applies a ``@{thm [source] true_conj1}''-conversion |
2001 in all possible positions. |
2003 in all possible positions. |
2002 *} |
2004 *} |
2004 ML %linenosgray{*fun all_true1_conv ctxt ctrm = |
2006 ML %linenosgray{*fun all_true1_conv ctxt ctrm = |
2005 case (Thm.term_of ctrm) of |
2007 case (Thm.term_of ctrm) of |
2006 @{term "op \<and>"} $ @{term True} $ _ => |
2008 @{term "op \<and>"} $ @{term True} $ _ => |
2007 (Conv.arg_conv (all_true1_conv ctxt) then_conv |
2009 (Conv.arg_conv (all_true1_conv ctxt) then_conv |
2008 Conv.rewr_conv @{thm true_conj1}) ctrm |
2010 Conv.rewr_conv @{thm true_conj1}) ctrm |
2009 | _ $ _ => Conv.combination_conv |
2011 | _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm |
2010 (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm |
|
2011 | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm |
2012 | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm |
2012 | _ => Conv.all_conv ctrm*} |
2013 | _ => Conv.all_conv ctrm*} |
2013 |
2014 |
2014 text {* |
2015 text {* |
2015 This function ``fires'' if the terms is of the form @{text "(True \<and> \<dots>)"}. |
2016 This function ``fires'' if the terms is of the form @{text "(True \<and> \<dots>)"}. |
2036 |
2037 |
2037 ML{*fun if_true1_conv ctxt ctrm = |
2038 ML{*fun if_true1_conv ctxt ctrm = |
2038 case Thm.term_of ctrm of |
2039 case Thm.term_of ctrm of |
2039 Const (@{const_name If}, _) $ _ => |
2040 Const (@{const_name If}, _) $ _ => |
2040 Conv.arg_conv (all_true1_conv ctxt) ctrm |
2041 Conv.arg_conv (all_true1_conv ctxt) ctrm |
2041 | _ $ _ => Conv.combination_conv |
2042 | _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm |
2042 (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm |
|
2043 | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm |
2043 | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm |
2044 | _ => Conv.all_conv ctrm *} |
2044 | _ => Conv.all_conv ctrm *} |
2045 |
2045 |
2046 text {* |
2046 text {* |
2047 Here is an example for this conversion: |
2047 Here is an example for this conversion: |