src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41002 11a442b472c7
parent 41001 11715564e2ad
child 41003 7e2a7bd55a00
equal deleted inserted replaced
41001:11715564e2ad 41002:11a442b472c7
  1159           val (m2, accum) = do_formula t2 accum
  1159           val (m2, accum) = do_formula t2 accum
  1160         in
  1160         in
  1161           (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
  1161           (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
  1162         end
  1162         end
  1163       and do_formula t accum =
  1163       and do_formula t accum =
  1164           case t of
  1164         case t of
  1165             (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  1165           (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  1166             do_all t0 s1 T1 t1 accum
  1166           do_all t0 s1 T1 t1 accum
  1167           | @{const Trueprop} $ t1 =>
  1167         | @{const Trueprop} $ t1 =>
  1168             let val (m1, accum) = do_formula t1 accum in
  1168           let val (m1, accum) = do_formula t1 accum in
  1169               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
  1169             (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
  1170                      m1), accum)
  1170              accum)
  1171             end
  1171           end
  1172           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
  1172         | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
  1173             consider_general_equals mdata true x t1 t2 accum
  1173           consider_general_equals mdata true x t1 t2 accum
  1174           | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  1174         | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  1175           | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
  1175         | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
  1176             do_conjunction t0 t1 t2 accum
  1176           do_conjunction t0 t1 t2 accum
  1177           | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
  1177         | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
  1178             do_all t0 s0 T1 t1 accum
  1178           do_all t0 s0 T1 t1 accum
  1179           | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
  1179         | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
  1180             consider_general_equals mdata true x t1 t2 accum
  1180           consider_general_equals mdata true x t1 t2 accum
  1181           | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
  1181         | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
  1182           | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  1182         | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  1183           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
  1183         | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
  1184                              \do_formula", [t])
  1184                            \do_formula", [t])
  1185     in do_formula t end
  1185     in do_formula t end
  1186 
  1186 
  1187 fun string_for_mtype_of_term ctxt asgs t M =
  1187 fun string_for_mtype_of_term ctxt asgs t M =
  1188   Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype asgs M)
  1188   Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype asgs M)
  1189 
  1189