70 in case pred of |
70 in case pred of |
71 Const (c, T) => c |
71 Const (c, T) => c |
72 | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) |
72 | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) |
73 end |
73 end |
74 *) |
74 *) |
75 val defining_term_of_introrule = defining_term_of_introrule_term o prop_of |
75 val defining_term_of_introrule = defining_term_of_introrule_term o Thm.prop_of |
76 |
76 |
77 fun defining_const_of_introrule th = |
77 fun defining_const_of_introrule th = |
78 (case defining_term_of_introrule th of |
78 (case defining_term_of_introrule th of |
79 Const (c, _) => c |
79 Const (c, _) => c |
80 | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])) |
80 | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [Thm.prop_of th])) |
81 |
81 |
82 (*TODO*) |
82 (*TODO*) |
83 fun is_introlike_term _ = true |
83 fun is_introlike_term _ = true |
84 |
84 |
85 val is_introlike = is_introlike_term o prop_of |
85 val is_introlike = is_introlike_term o Thm.prop_of |
86 |
86 |
87 fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) = |
87 fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) = |
88 (case strip_comb u of |
88 (case strip_comb u of |
89 (Const (_, T), args) => |
89 (Const (_, T), args) => |
90 if (length (binder_types T) = length args) then |
90 if (length (binder_types T) = length args) then |
93 raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) |
93 raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) |
94 | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) |
94 | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) |
95 | check_equation_format_term t = |
95 | check_equation_format_term t = |
96 raise TERM ("check_equation_format_term failed: Not an equation", [t]) |
96 raise TERM ("check_equation_format_term failed: Not an equation", [t]) |
97 |
97 |
98 val check_equation_format = check_equation_format_term o prop_of |
98 val check_equation_format = check_equation_format_term o Thm.prop_of |
99 |
99 |
100 |
100 |
101 fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u) |
101 fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u) |
102 | defining_term_of_equation_term t = |
102 | defining_term_of_equation_term t = |
103 raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) |
103 raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) |
104 |
104 |
105 val defining_term_of_equation = defining_term_of_equation_term o prop_of |
105 val defining_term_of_equation = defining_term_of_equation_term o Thm.prop_of |
106 |
106 |
107 fun defining_const_of_equation th = |
107 fun defining_const_of_equation th = |
108 (case defining_term_of_equation th of |
108 (case defining_term_of_equation th of |
109 Const (c, _) => c |
109 Const (c, _) => c |
110 | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])) |
110 | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [Thm.prop_of th])) |
111 |
111 |
112 |
112 |
113 |
113 |
114 |
114 |
115 (* Normalizing equations *) |
115 (* Normalizing equations *) |
116 |
116 |
117 fun mk_meta_equation th = |
117 fun mk_meta_equation th = |
118 (case prop_of th of |
118 (case Thm.prop_of th of |
119 Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => |
119 Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => |
120 th RS @{thm eq_reflection} |
120 th RS @{thm eq_reflection} |
121 | _ => th) |
121 | _ => th) |
122 |
122 |
123 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
123 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
124 |
124 |
125 fun full_fun_cong_expand th = |
125 fun full_fun_cong_expand th = |
126 let |
126 let |
127 val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) |
127 val (f, args) = strip_comb (fst (Logic.dest_equals (Thm.prop_of th))) |
128 val i = length (binder_types (fastype_of f)) - length args |
128 val i = length (binder_types (fastype_of f)) - length args |
129 in funpow i (fn th => th RS meta_fun_cong) th end; |
129 in funpow i (fn th => th RS meta_fun_cong) th end; |
130 |
130 |
131 fun declare_names s xs ctxt = |
131 fun declare_names s xs ctxt = |
132 let |
132 let |
135 |
135 |
136 fun split_all_pairs thy th = |
136 fun split_all_pairs thy th = |
137 let |
137 let |
138 val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
138 val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
139 val ((_, [th']), _) = Variable.import true [th] ctxt |
139 val ((_, [th']), _) = Variable.import true [th] ctxt |
140 val t = prop_of th' |
140 val t = Thm.prop_of th' |
141 val frees = Term.add_frees t [] |
141 val frees = Term.add_frees t [] |
142 val freenames = Term.add_free_names t [] |
142 val freenames = Term.add_free_names t [] |
143 val nctxt = Name.make_context freenames |
143 val nctxt = Name.make_context freenames |
144 fun mk_tuple_rewrites (x, T) nctxt = |
144 fun mk_tuple_rewrites (x, T) nctxt = |
145 let |
145 let |
267 fun is_datatype_constructor (x as (_, T)) = |
267 fun is_datatype_constructor (x as (_, T)) = |
268 (case body_type T of |
268 (case body_type T of |
269 Type (Tcon, _) => can (Ctr_Sugar.dest_ctr ctxt Tcon) (Const x) |
269 Type (Tcon, _) => can (Ctr_Sugar.dest_ctr ctxt Tcon) (Const x) |
270 | _ => false) |
270 | _ => false) |
271 fun defiants_of specs = |
271 fun defiants_of specs = |
272 fold (Term.add_consts o prop_of) specs [] |
272 fold (Term.add_consts o Thm.prop_of) specs [] |
273 |> filter_out is_datatype_constructor |
273 |> filter_out is_datatype_constructor |
274 |> filter_out is_nondefining_const |
274 |> filter_out is_nondefining_const |
275 |> filter_out has_code_pred_intros |
275 |> filter_out has_code_pred_intros |
276 |> filter_out case_consts |
276 |> filter_out case_consts |
277 |> filter_out special_cases |
277 |> filter_out special_cases |