104 NONE => NONE |
104 NONE => NONE |
105 | SOME (bop, (m, p, S, S')) => |
105 | SOME (bop, (m, p, S, S')) => |
106 SOME (close (Goal.prove ctxt [] []) |
106 SOME (close (Goal.prove ctxt [] []) |
107 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) |
107 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) |
108 (K (EVERY |
108 (K (EVERY |
109 [rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1, |
109 [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1, |
110 EVERY [etac conjE 1, rtac IntI 1, simp, simp, |
110 EVERY [etac conjE 1, rtac IntI 1, simp, simp, |
111 etac IntE 1, rtac conjI 1, simp, simp] ORELSE |
111 etac IntE 1, rtac conjI 1, simp, simp] ORELSE |
112 EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp, |
112 EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp, |
113 etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]]))) |
113 etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]]))) |
114 handle ERROR _ => NONE)) |
114 handle ERROR _ => NONE)) |
525 (HOLogic.mk_Trueprop (HOLogic.mk_eq |
525 (HOLogic.mk_Trueprop (HOLogic.mk_eq |
526 (list_comb (p, params3), |
526 (list_comb (p, params3), |
527 fold_rev (Term.abs o pair "x") Ts |
527 fold_rev (Term.abs o pair "x") Ts |
528 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)), |
528 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)), |
529 list_comb (c, params)))))) |
529 list_comb (c, params)))))) |
530 (K (REPEAT (rtac ext 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps |
530 (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps |
531 [def, mem_Collect_eq, @{thm split_conv}]) 1)) |
531 [def, mem_Collect_eq, @{thm split_conv}]) 1)) |
532 in |
532 in |
533 lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"), |
533 lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"), |
534 [Attrib.internal (K pred_set_conv_att)]), |
534 [Attrib.internal (K pred_set_conv_att)]), |
535 [conv_thm]) |> snd |
535 [conv_thm]) |> snd |