theory Reification_Test
  imports "Isabelle_DOF.DOF_Deep"
  
begin

ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"}
\<close>

term*\<open>@{typ \<open>int\<close>}\<close>
value*\<open>@{typ \<open>int\<close>}\<close>
value*\<open>@{typ \<open>int \<Rightarrow> bool\<close>}\<close>
term*\<open>@{typ \<open>prop\<close>}\<close>
value*\<open>@{typ \<open>prop\<close>}\<close>
term*\<open>@{typ \<open>'a list\<close>}\<close>
value*\<open>@{typ \<open>'a list\<close>}\<close>

ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
\<close>
term*\<open>@{term \<open>1::int\<close>}\<close>
value*\<open>@{term \<open>1::int\<close>}\<close>
term*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
value*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
term*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
value*\<open>@{term \<open>[2, 3::int]\<close>}\<close>

prf refl
full_prf refl

term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
value*\<open>proof @{thm \<open>HOL.refl\<close>}\<close>
value*\<open>depth (proof @{thm \<open>HOL.refl\<close>})\<close>
value*\<open>size (proof @{thm \<open>HOL.refl\<close>})\<close>
value*\<open>fv_Proof (proof @{thm \<open>HOL.refl\<close>})\<close>
term*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>

ML\<open>
val t_schematic = TVar(("'a",0), [])
val t = @{term "Tv (Var (STR '''a'', 0)) {}"}
val rt_schematic = ISA_core.reify_typ t_schematic
val true = rt_schematic = t
\<close>

lemma test : "AAA \<and> BBB \<longrightarrow> BBB \<and> AAA"
  by auto

lemma test2 : "AAA \<and> BBB \<Longrightarrow> BBB \<and> AAA"
  by auto

lemma test3: "AAAAA \<and> BBBBB \<longrightarrow> BBBBB \<and> AAAAA"
proof
  assume "AAAAA \<and> BBBBB"
  then obtain BBBBB and AAAAA ..
  then show "BBBBB \<and> AAAAA" ..
qed

lemma test4:
  assumes "(AAA \<and> BBB)"
  shows "BBB \<and> AAA"
  apply (insert assms)
  by auto

declare[[show_sorts]]
declare[[ML_print_depth = 20]]

ML\<open>
val full = true
val thm = @{thm "test2"}
val hyps = Thm.hyps_of thm
val prems = Thm.prems_of thm
val reconstruct_proof = Thm.reconstruct_proof_of thm
val standard_proof = Proof_Syntax.standard_proof_of
          {full = full, expand_name = Thm.expand_name thm} thm
val term_of_proof = Proof_Syntax.term_of_proof standard_proof
\<close>

ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
ML\<open>
  val thm = @{thm test};

  (*proof body with digest*)
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {name, ...} => insert (op =) name) [body] [];
\<close>

prf test
full_prf test
term*\<open>@{thm \<open>Reification_Test.test\<close>}\<close>
value*\<open>@{thm \<open>Reification_Test.test\<close>}\<close>
term*\<open>@{thms-of \<open>Reification_Test.test\<close>}\<close>
value*\<open>@{thms-of \<open>Reification_Test.test\<close>}\<close>

ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
ML\<open>
  val thm = @{thm test4};

  (*proof body with digest*)
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {name, ...} => insert (op =) name) [body] [];
\<close>

ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
ML\<open>
  val thm = @{thm test2};

  (*proof body with digest*)
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {name, ...} => insert (op =) name) [body] [];
\<close>

prf test2
full_prf test2
term*\<open>@{thm \<open>Reification_Test.test2\<close>}\<close>
value*\<open>proof @{thm \<open>Reification_Test.test2\<close>}\<close>

ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
ML\<open>
  val thm = @{thm test3};

  (*proof body with digest*)
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {name, ...} => insert (op =) name) [body] [];
\<close>

prf test2
full_prf test2
term*\<open>@{thm \<open>Reification_Test.test3\<close>}\<close>
value*\<open>@{thm \<open>Reification_Test.test3\<close>}\<close>

ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
ML\<open>
  val thm = @{thm Pure.symmetric};

  (*proof body with digest*)
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {name, ...} => insert (op =) name) [body] [];
\<close>

prf symmetric
full_prf symmetric
term*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
value*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>

ML\<open>
val full = true
val thm = @{thm "Groups.minus_class.super"}
val standard_proof = Proof_Syntax.standard_proof_of
          {full = full, expand_name = Thm.expand_name thm} thm
val term_of_proof = Proof_Syntax.term_of_proof standard_proof
\<close>

ML\<open>
val thm = Proof_Context.get_thm \<^context> "Groups.minus_class.super"
val prop = Thm.prop_of thm
val proof = Thm.proof_of thm
\<close>

prf Groups.minus_class.super
full_prf Groups.minus_class.super
term*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
value*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>

(*ML\<open>
val full = true
val thm = @{thm "Homotopy.starlike_imp_contractible"}
val standard_proof = Proof_Syntax.standard_proof_of
          {full = full, expand_name = Thm.expand_name thm} thm
val term_of_proof = Proof_Syntax.term_of_proof standard_proof
\<close>

ML\<open>
val thm = Proof_Context.get_thm \<^context> "Homotopy.starlike_imp_contractible"
val prop = Thm.prop_of thm
val proof = Thm.proof_of thm
\<close>

prf Homotopy.starlike_imp_contractible
full_prf Homotopy.starlike_imp_contractible
term*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>
value*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>*)


end