69 fold_rev (absfree o dest_Free) args |
69 fold_rev (absfree o dest_Free) args |
70 (HOLogic.choice_const T $ beta_eta_in_abs_body body) |
70 (HOLogic.choice_const T $ beta_eta_in_abs_body body) |
71 |> mk_old_skolem_term_wrapper |
71 |> mk_old_skolem_term_wrapper |
72 val comb = list_comb (rhs, args) |
72 val comb = list_comb (rhs, args) |
73 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
73 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
74 | dec_sko \<^Const_>\<open>All _ for \<open>Abs (a, T, p)\<close>\<close> rhss = |
74 | dec_sko \<^Const_>\<open>All _ for \<open>Abs abs\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs abs)) rhss |
75 (*Universal quant: insert a free variable into body and continue*) |
|
76 let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a |
|
77 in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
|
78 | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q |
75 | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q |
79 | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q |
76 | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q |
80 | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss |
77 | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss |
81 | dec_sko _ rhss = rhss |
78 | dec_sko _ rhss = rhss |
82 in dec_sko (Thm.prop_of th) [] end; |
79 in dec_sko (Thm.prop_of th) [] end; |