Quelle  veriT_Preprocessing.thy

(*  Title:      HOL/ex/veriT_Preprocessing.thy
    Author:     Jasmin Christian Blanchette, Inria, LORIA, MPII
*)

section ‹Proof Reconstruction for veriT's Preprocessing›

theory veriT_Preprocessing
imports Main
begin

declare [[eta_contract = false]]

lemma
  some_All_iffI: "p (SOME x. ¬ p x) = q ==> (∀x. p x) = q" and
  some_Ex_iffI: "p (SOME x. p x) = q ==> (∃x. p x) = q"
  by (metis (full_types) someI_ex)+

ML ‹
  mk_prod1 bound_Ts (t, u) =
 HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;

  mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));

  mk_arg_congN 0 = refl
 | mk_arg_congN 1 = arg_cong
 | mk_arg_congN 2 = @{thm arg_cong2}
 | mk_arg_congN n = arg_cong RS funpow (n - 2) (fn th => @{thm cong} RS th) @{thm cong};

  mk_let_iffNI ctxt n =
 let
 val ((As, [B]), _) = ctxt
 |> Ctr_Sugar_Util.mk_TFrees n
 ||>> Ctr_Sugar_Util.mk_TFrees 1;

 val ((((ts, us), [p]), [q]), _) = ctxt
 |> Ctr_Sugar_Util.mk_Frees "t" As
 ||>> Ctr_Sugar_Util.mk_Frees "u" As
 ||>> Ctr_Sugar_Util.mk_Frees "p" [As ---> B]
 ||>> Ctr_Sugar_Util.mk_Frees "q" [B];

 val tuple_t = HOLogic.mk_tuple ts;
 val tuple_T = fastype_of tuple_t;

 val lambda_t = HOLogic.tupled_lambda tuple_t (list_comb (p, ts));

 val left_prems = map2 (curry Ctr_Sugar_Util.mk_Trueprop_eq) ts us;
 val right_prem = Ctr_Sugar_Util.mk_Trueprop_eq (list_comb (p, us), q);
 val concl = Ctr_Sugar_Util.mk_Trueprop_eq (🍋‹Let tuple_T B for tuple_t lambda_t›, q);

 val goal = Logic.list_implies (left_prems @ [right_prem], concl);
 val vars = Variable.add_free_names ctxt goal [];
 in
 Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
 HEADGOAL (hyp_subst_tac ctxt) THEN
 Local_Defs.unfold0_tac ctxt @{thms Let_def prod.case} THEN
 HEADGOAL (resolve_tac ctxt [refl]))
 end;

  rule_name =
 Refl
  Taut of thm
  Trans of term
  Cong
  Bind
  Sko_Ex
  Sko_All
  Let of term list;

  str_of_rule_name Refl = "Refl"
 | str_of_rule_name (Taut th) = "Taut[" ^ 🍋 th ^ "]"
 | str_of_rule_name (Trans t) = "Trans[" ^ Syntax.string_of_term 🍋 t ^ "]"
 | str_of_rule_name Cong = "Cong"
 | str_of_rule_name Bind = "Bind"
 | str_of_rule_name Sko_Ex = "Sko_Ex"
 | str_of_rule_name Sko_All = "Sko_All"
 | str_of_rule_name (Let ts) =
 "Let[" ^ commas (map (Syntax.string_of_term 🍋) ts) ^ "]";

  node = N of rule_name * node list;

  lambda_count (Abs (_, _, t)) = lambda_count t + 1
 | lambda_count ((t as Abs _) $ _) = lambda_count t - 1
 | lambda_count ((t as 🍋‹case_prod _ _ _› $ _) $ _) = lambda_count t - 1
 | lambda_count 🍋‹case_prod _ _ _ for t› = lambda_count t - 1
 | lambda_count _ = 0;

  zoom apply =
 let
 fun zo 0 bound_Ts (Abs (r, T, t), Abs (s, U, u)) =
 let val (t', u') = zo 0 (T :: bound_Ts) (t, u) in
 (lambda (Free (r, T)) t', lambda (Free (s, U)) u')
 end
 | zo 0 bound_Ts ((t as Abs (_, T, _)) $ arg, u) =
 let val (t', u') = zo 1 (T :: bound_Ts) (t, u) in
 (t' $ arg, u')
 end
 | zo 0 bound_Ts ((t as 🍋‹case_prod _ _ _› $ _) $ arg, u) =
 let val (t', u') = zo 1 bound_Ts (t, u) in
 (t' $ arg, u')
 end
 | zo 0 bound_Ts tu = apply bound_Ts tu
 | zo n bound_Ts (🍋‹case_prod A B _ for t›, u) =
 let
 val (t', u') = zo (n + 1) bound_Ts (t, u);
 val C = range_type (range_type (fastype_of t'));
 in (🍋‹case_prod A B C for t'›, u') end
 | zo n bound_Ts (Abs (s, T, t), u) =
 let val (t', u') = zo (n - 1) (T :: bound_Ts) (t, u) in
 (Abs (s, T, t'), u')
 end
 | zo _ _ (t, u) = raise TERM ("zoom", [t, u]);
 in
 zo 0 []
 end;

  apply_Trans_left t (lhs, _) = (lhs, t);
  apply_Trans_right t (_, rhs) = (t, rhs);

  apply_Cong ary j (lhs, rhs) =
 (case apply2 strip_comb (lhs, rhs) of
 ((c, ts), (d, us)) =>
 if c aconv d andalso length ts = ary andalso length us = ary then (nth ts j, nth us j)
 else raise TERM ("apply_Cong", [lhs, rhs]));

  apply_Bind (lhs, rhs) =
 (case (lhs, rhs) of
 (🍋‹All _ for ‹Abs (_, T, t)››, 🍋‹All _ for ‹Abs (s, U, u)››) =>
 (Abs (s, T, t), Abs (s, U, u))
 | (🍋‹Ex _ for t›, 🍋‹Ex _ for u›) => (t, u)
 | _ => raise TERM ("apply_Bind", [lhs, rhs]));

  apply_Sko_Ex (lhs, rhs) =
 (case lhs of
 🍋‹Ex _ for ‹t as Abs (_, T, _)›› =>
 (t $ (HOLogic.choice_const T $ t), rhs)
 | _ => raise TERM ("apply_Sko_Ex", [lhs]));

  apply_Sko_All (lhs, rhs) =
 (case lhs of
 🍋‹All _ for ‹t as Abs (s, T, body)›› =>
 (t $ (HOLogic.choice_const T $ Abs (s, T, HOLogic.mk_not body)), rhs)
 | _ => raise TERM ("apply_Sko_All", [lhs]));

  apply_Let_left ts j (lhs, _) =
 (case lhs of
 🍋‹Let _ _ for t _› =>
 let val ts0 = HOLogic.strip_tuple t in
 (nth ts0 j, nth ts j)
 end
 | _ => raise TERM ("apply_Let_left", [lhs]));

  apply_Let_right ts bound_Ts (lhs, rhs) =
 let val t' = mk_tuple1 bound_Ts ts in
 (case lhs of
 🍋‹Let _ _ for _ u› => (u $ t', rhs)
 | _ => raise TERM ("apply_Let_right", [lhs, rhs]))
 end;

  reconstruct_proof ctxt (lrhs as (_, rhs), N (rule_name, prems)) =
 let
 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq lrhs);
 val ary = length prems;

 val _ = warning (Syntax.string_of_term 🍋 goal);
 val _ = warning (str_of_rule_name rule_name);

 val parents =
 (case (rule_name, prems) of
 (Refl, []) => []
 | (Taut _, []) => []
 | (Trans t, [left_prem, right_prem]) =>
 [reconstruct_proof ctxt (zoom (K (apply_Trans_left t)) lrhs, left_prem),
 reconstruct_proof ctxt (zoom (K (apply_Trans_right t)) (rhs, rhs), right_prem)]
 | (Cong, _) =>
 map_index (fn (j, prem) => reconstruct_proof ctxt (zoom (K (apply_Cong ary j)) lrhs, prem))
 prems
 | (Bind, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Bind) lrhs, prem)]
 | (Sko_Ex, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_Ex) lrhs, prem)]
 | (Sko_All, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_All) lrhs, prem)]
 | (Let ts, prems) =>
 let val (left_prems, right_prem) = split_last prems in
 map2 (fn j => fn prem =>
 reconstruct_proof ctxt (zoom (K (apply_Let_left ts j)) lrhs, prem))
 (0 upto length left_prems - 1) left_prems @
 [reconstruct_proof ctxt (zoom (apply_Let_right ts) lrhs, right_prem)]
 end
 | _ => raise Fail ("Invalid rule: " ^ str_of_rule_name rule_name ^ "/" ^
 string_of_int (length prems)));

 val rule_thms =
 (case rule_name of
 Refl => [refl]
 | Taut th => [th]
 | Trans _ => [trans]
 | Cong => [mk_arg_congN ary]
 | Bind => @{thms arg_cong[of _ _ All] arg_cong[of _ _ Ex]}
 | Sko_Ex => [@{thm some_Ex_iffI}]
 | Sko_All => [@{thm some_All_iffI}]
 | Let ts => [mk_let_iffNI ctxt (length ts)]);

 val num_lams = lambda_count rhs;
 val conged_parents = map (funpow num_lams (fn th => th RS fun_cong)
 #> Local_Defs.unfold0 ctxt @{thms prod.case}) parents;
 in
 Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} =>
 Local_Defs.unfold0_tac ctxt @{thms prod.case} THEN
 HEADGOAL (REPEAT_DETERM_N num_lams o resolve_tac ctxt [ext] THEN'
 resolve_tac ctxt rule_thms THEN'
 K (Local_Defs.unfold0_tac ctxt @{thms prod.case}) THEN'
 EVERY' (map (resolve_tac ctxt o single) conged_parents)))
 end;
 ›

ML ‹
  proof0 =
 ((term‹∃x :: nat. p x›,
 term‹p (SOME x :: nat. p x)›),
 N (Sko_Ex, [N (Refl, [])]));

  🍋 proof0;
 ›

ML ‹
  proof1 =
 ((term‹¬ (∀x :: nat. ∃y :: nat. p x y)›,
 term‹¬ (∃y :: nat. p (SOME x :: nat. ¬ (∃y :: nat. p x y)) y)›),
 N (Cong, [N (Sko_All, [N (Bind, [N (Refl, [])])])]));

  🍋 proof1;
 ›

ML ‹
  proof2 =
 ((term‹∀x :: nat. ∃y :: nat. ∃z :: nat. p x y z›,
 term‹∀x :: nat. p x (SOME y :: nat. ∃z :: nat. p x y z)
 (SOME z :: nat. p x (SOME y :: nat. ∃z :: nat. p x y z) z)›),
 N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])]));

  🍋 proof2
 ›

ML ‹
  proof3 =
 ((term‹∀x :: nat. ∃x :: nat. ∃x :: nat. p x x x›,
 term‹∀x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)›),
 N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])]));

  🍋 proof3
 ›

ML ‹
  proof4 =
 ((term‹∀x :: nat. ∃x :: nat. ∃x :: nat. p x x x›,
 term‹∀x :: nat. ∃x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)›),
 N (Bind, [N (Bind, [N (Sko_Ex, [N (Refl, [])])])]));

  🍋 proof4
 ›

ML ‹
  proof5 =
 ((term‹∀x :: nat. q ∧ (∃x :: nat. ∃x :: nat. p x x x)›,
 term‹∀x :: nat. q ∧
 (∃x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x))›),
 N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_Ex, [N (Refl, [])])])])]));

  🍋 proof5
 ›

ML ‹
  proof6 =
 ((term‹¬ (∀x :: nat. p ∧ (∃x :: nat. ∀x :: nat. q x x))›,
 term‹¬ (∀x :: nat. p ∧
 (∃x :: nat. q (SOME x :: nat. ¬ q x x) (SOME x. ¬ q x x)))›),
 N (Cong, [N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_All, [N (Refl, [])])])])])]));

  🍋 proof6
 ›

ML ‹
  proof7 =
 ((term‹¬ ¬ (∃x. p x)›,
 term‹¬ ¬ p (SOME x. p x)›),
 N (Cong, [N (Cong, [N (Sko_Ex, [N (Refl, [])])])]));

  🍋 proof7
 ›

ML ‹
  proof8 =
 ((term‹¬ ¬ (let x = Suc x in x = 0)›,
 term‹¬ ¬ Suc x = 0›),
 N (Cong, [N (Cong, [N (Let [term‹Suc x›], [N (Refl, []), N (Refl, [])])])]));

  🍋 proof8
 ›

ML ‹
  proof9 =
 ((term‹¬ (let x = Suc x in x = 0)›,
 term‹¬ Suc x = 0›),
 N (Cong, [N (Let [term‹Suc x›], [N (Refl, []), N (Refl, [])])]));

  🍋 proof9
 ›

ML ‹
  proof10 =
 ((term‹∃x :: nat. p (x + 0)›,
 term‹∃x :: nat. p x›),
 N (Bind, [N (Cong, [N (Taut @{thm add_0_right}, [])])]));

  🍋 proof10;
 ›

ML ‹
  proof11 =
 ((term‹¬ (let (x, y) = (Suc y, Suc x) in y = 0)›,
 term‹¬ Suc x = 0›),
 N (Cong, [N (Let [term‹Suc y›, term‹Suc x›], [N (Refl, []), N (Refl, []),
 N (Refl, [])])]));

  🍋 proof11
 ›

ML ‹
  proof12 =
 ((term‹¬ (let (x, y) = (Suc y, Suc x); (u, v, w) = (y, x, y) in w = 0)›,
 term‹¬ Suc x = 0›),
 N (Cong, [N (Let [term‹Suc y›, term‹Suc x›], [N (Refl, []), N (Refl, []),
 N (Let [term‹Suc x›, term‹Suc y›, term‹Suc x›],
 [N (Refl, []), N (Refl, []), N (Refl, []), N (Refl, [])])])]));

  🍋 proof12
 ›

ML ‹
  proof13 =
 ((term‹¬ ¬ (let x = Suc x in x = 0)›,
 term‹¬ ¬ Suc x = 0›),
 N (Cong, [N (Cong, [N (Let [term‹Suc x›], [N (Refl, []), N (Refl, [])])])]));

  🍋 proof13
 ›

ML ‹
  proof14 =
 ((term‹let (x, y) = (f (a :: nat), b :: nat) in x > a›,
 term‹f (a :: nat) > a›),
 N (Let [term‹f (a :: nat) :: nat›, term‹b :: nat›],
 [N (Cong, [N (Refl, [])]), N (Refl, []), N (Refl, [])]));

  🍋 proof14
 ›

ML ‹
  proof15 =
 ((term‹let x = (let y = g (z :: nat) in f (y :: nat)) in x = Suc 0›,
 term‹f (g (z :: nat) :: nat) = Suc 0›),
 N (Let [term‹f (g (z :: nat) :: nat) :: nat›],
 [N (Let [term‹g (z :: nat) :: nat›], [N (Refl, []), N (Refl, [])]), N (Refl, [])]));

  🍋 proof15
 ›

ML ‹
  proof16 =
 ((term‹a > Suc b›,
 term‹a > Suc b›),
 N (Trans term‹a > Suc b›, [N (Refl, []), N (Refl, [])]));

  🍋 proof16
 ›

thm Suc_1
thm numeral_2_eq_2
thm One_nat_def

ML ‹
  proof17 =
 ((term‹2 :: nat›,
 term‹Suc (Suc 0) :: nat›),
 N (Trans term‹Suc 1›, [N (Taut @{thm Suc_1[symmetric]}, []), N (Cong,
 [N (Taut @{thm One_nat_def}, [])])]));

  🍋 proof17
 ›

ML ‹
  proof18 =
 ((term‹let x = a in let y = b in Suc x + y›,
 term‹Suc a + b›),
 N (Trans term‹let y = b in Suc a + y›,
 [N (Let [term‹a :: nat›], [N (Refl, []), N (Refl, [])]),
 N (Let [term‹b :: nat›], [N (Refl, []), N (Refl, [])])]));

  🍋 proof18
 ›

ML ‹
  proof19 =
 ((term‹∀x. let x = f (x :: nat) :: nat in g x›,
 term‹∀x. g (f (x :: nat) :: nat)›),
 N (Bind, [N (Let [term‹f :: nat ==> nat› $ Bound 0],
 [N (Refl, []), N (Refl, [])])]));

  🍋 proof19
 ›

ML ‹
  proof20 =
 ((term‹∀x. let y = Suc 0 in let x = f (x :: nat) :: nat in g x›,
 term‹∀x. g (f (x :: nat) :: nat)›),
 N (Bind, [N (Let [term‹Suc 0›], [N (Refl, []), N (Let [term‹f (x :: nat) :: nat›],
 [N (Refl, []), N (Refl, [])])])]));

  🍋 proof20
 ›

ML ‹
  proof21 =
 ((term‹∀x :: nat. let x = f x :: nat in let y = x in p y›,
 term‹∀z :: nat. p (f z :: nat)›),
 N (Bind, [N (Let [term‹f (z :: nat) :: nat›],
 [N (Refl, []), N (Let [term‹f (z :: nat) :: nat›],
 [N (Refl, []), N (Refl, [])])])]));

  🍋 proof21
 ›

ML ‹
  proof22 =
 ((term‹∀x :: nat. let x = f x :: nat in let y = x in p y›,
 term‹∀x :: nat. p (f x :: nat)›),
 N (Bind, [N (Let [term‹f (x :: nat) :: nat›],
 [N (Refl, []), N (Let [term‹f (x :: nat) :: nat›],
 [N (Refl, []), N (Refl, [])])])]));

  🍋 proof22
 ›

ML ‹
  proof23 =
 ((term‹∀x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y›,
 term‹∀z :: nat. p (f z :: nat)›),
 N (Bind, [N (Let [term‹f (z :: nat) :: nat›, term‹0 :: nat›],
 [N (Refl, []), N (Refl, []), N (Let [term‹f (z :: nat) :: nat›],
 [N (Refl, []), N (Refl, [])])])]));

  🍋 proof23
 ›

ML ‹
  proof24 =
 ((term‹∀x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y›,
 term‹∀x :: nat. p (f x :: nat)›),
 N (Bind, [N (Let [term‹f (x :: nat) :: nat›, term‹0 :: nat›],
 [N (Refl, []), N (Refl, []), N (Let [term‹f (x :: nat) :: nat›],
 [N (Refl, []), N (Refl, [])])])]));

  🍋 proof24
 ›

ML ‹
  proof25 =
 ((term‹let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat›,
 term‹vr1 + vr2 + vr2 :: nat›),
 N (Trans term‹let vr1a = vr2 in vr1 + vr1a + vr2 :: nat›,
 [N (Let [term‹vr1 :: nat›], [N (Refl, []), N (Refl, [])]),
 N (Let [term‹vr2 :: nat›], [N (Refl, []), N (Refl, [])])]));

  🍋 proof25
 ›

end