equal
deleted
inserted
replaced
41 if Logic.occs (Free x, t) then raise Match else true |
41 if Logic.occs (Free x, t) then raise Match else true |
42 | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => |
42 | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => |
43 if Logic.occs (Free x, t) then raise Match else false |
43 if Logic.occs (Free x, t) then raise Match else false |
44 | _ => raise Match); |
44 | _ => raise Match); |
45 fun mk_eq thm = |
45 fun mk_eq thm = |
46 (if inspect (prop_of thm) then [thm RS eq_reflection] |
46 (if inspect (Thm.prop_of thm) then [thm RS eq_reflection] |
47 else [Thm.symmetric (thm RS eq_reflection)]) |
47 else [Thm.symmetric (thm RS eq_reflection)]) |
48 handle Match => []; |
48 handle Match => []; |
49 val simpset = |
49 val simpset = |
50 empty_simpset ctxt |
50 empty_simpset ctxt |
51 |> Simplifier.set_mksimps (K mk_eq); |
51 |> Simplifier.set_mksimps (K mk_eq); |
78 in |
78 in |
79 |
79 |
80 fun mk_partial_elim_rules ctxt result = |
80 fun mk_partial_elim_rules ctxt result = |
81 let |
81 let |
82 val thy = Proof_Context.theory_of ctxt; |
82 val thy = Proof_Context.theory_of ctxt; |
83 val cert = cterm_of thy; |
83 val cert = Thm.cterm_of thy; |
84 |
84 |
85 val FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
85 val FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
86 val n_fs = length fs; |
86 val n_fs = length fs; |
87 |
87 |
88 fun mk_partial_elim_rule (idx, f) = |
88 fun mk_partial_elim_rule (idx, f) = |
96 in mk_funeq (n - 1) T ctxt (xn :: acc_vars, acc_lhs $ xn) end |
96 in mk_funeq (n - 1) T ctxt (xn :: acc_vars, acc_lhs $ xn) end |
97 | mk_funeq _ _ _ _ = raise TERM ("Not a function.", [f]); |
97 | mk_funeq _ _ _ _ = raise TERM ("Not a function.", [f]); |
98 |
98 |
99 val f_simps = |
99 val f_simps = |
100 filter (fn r => |
100 filter (fn r => |
101 (prop_of r |> Logic.strip_assums_concl |
101 (Thm.prop_of r |> Logic.strip_assums_concl |
102 |> HOLogic.dest_Trueprop |
102 |> HOLogic.dest_Trueprop |
103 |> dest_funprop |> fst |> fst) = f) |
103 |> dest_funprop |> fst |> fst) = f) |
104 psimps; |
104 psimps; |
105 |
105 |
106 val arity = |
106 val arity = |
107 hd f_simps |
107 hd f_simps |
108 |> prop_of |
108 |> Thm.prop_of |
109 |> Logic.strip_assums_concl |
109 |> Logic.strip_assums_concl |
110 |> HOLogic.dest_Trueprop |
110 |> HOLogic.dest_Trueprop |
111 |> snd o fst o dest_funprop |
111 |> snd o fst o dest_funprop |
112 |> length; |
112 |> length; |
113 val name_ctxt = Variable.names_of ctxt |
113 val name_ctxt = Variable.names_of ctxt |