equal
deleted
inserted
replaced
28 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
28 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
29 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
29 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
30 |
30 |
31 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; |
31 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; |
32 |
32 |
33 val fresh_prod = thm "fresh_prod"; |
33 val fresh_prod = @{thm fresh_prod}; |
34 |
34 |
35 val perm_bool = mk_meta_eq (thm "perm_bool"); |
35 val perm_bool = mk_meta_eq @{thm perm_bool}; |
36 val perm_boolI = thm "perm_boolI"; |
36 val perm_boolI = @{thm perm_boolI}; |
37 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb |
37 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb |
38 (Drule.strip_imp_concl (cprop_of perm_boolI)))); |
38 (Drule.strip_imp_concl (cprop_of perm_boolI)))); |
39 |
39 |
40 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate |
40 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate |
41 [(perm_boolI_pi, pi)] perm_boolI; |
41 [(perm_boolI_pi, pi)] perm_boolI; |