theory Essential

imports FirstStep

begin

ML {*

fun pretty_helper aux env =

  env |> Vartab.dest

      |> map aux

      |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])

      |> Pretty.enum "," "[" "]"

      |> pwriteln

fun pretty_tyenv ctxt tyenv =

let

  fun get_typs (v, (s, T)) = (TVar (v, s), T)

  val print = pairself (pretty_typ ctxt)

in

  pretty_helper (print o get_typs) tyenv

end

fun pretty_env ctxt env =

let

   fun get_trms (v, (T, t)) = (Var (v, T), t)

   val print = pairself (pretty_term ctxt)

in

   pretty_helper (print o get_trms) env

end

fun prep_trm thy (x, (T, t)) =

  (cterm_of thy (Var (x, T)), cterm_of thy t)

fun prep_ty thy (x, (S, ty)) =

  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)

fun matcher_inst thy pat trm i =

  let

     val univ = Unify.matchers thy [(pat, trm)]

     val env = nth (Seq.list_of univ) i

     val tenv = Vartab.dest (Envir.term_env env)

     val tyenv = Vartab.dest (Envir.type_env env)

  in

     (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

  end

*}

ML {*

  let

     val pat = Logic.strip_imp_concl (prop_of @{thm spec})

     val trm = @{term "Trueprop (Q True)"}

     val inst = matcher_inst @{theory} pat trm 1

  in

     Drule.instantiate_normalize inst @{thm spec}

  end

*}

ML {*

let

   val c = Const (@{const_name "plus"}, dummyT)

   val o = @{term "1::nat"}

   val v = Free ("x", dummyT)

in

   Syntax.check_term @{context} (c $ o $ v)

end

*}

ML {*

   val my_thm =

   let

      val assm1 = @{cprop "\<And> (x::nat). P x ==> Q x"}

      val assm2 = @{cprop "(P::nat => bool) t"}

      val Pt_implies_Qt =

        Thm.assume assm1

        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

        |> Thm.forall_elim @{cterm "t::nat"}

        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

      val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)

               |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

   in

      Qt

      |> Thm.implies_intr assm2

      |> Thm.implies_intr assm1

   end

*}

local_setup {*

  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd  

*}

local_setup {*

  Local_Theory.note ((@{binding "my_thm_simp"},

        [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd

*}

(* pp 62 *)

ML {*

   Thm.reflexive @{cterm "True"}

    |> Simplifier.rewrite_rule [@{thm True_def}]

    |> pretty_thm @{context}

    |> pwriteln

*}

ML {*

  val thm = @{thm list.induct} |> forall_intr_vars;

  thm |> forall_intr_vars |> cprop_of |> Object_Logic.atomize

  |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)

*}

ML {*

fun atomize_thm thm =

let

  val thm' = forall_intr_vars thm

  val thm'' = Object_Logic.atomize (cprop_of thm')

in

  Raw_Simplifier.rewrite_rule [thm''] thm'

end

*}

ML {*

  @{thm list.induct} |> atomize_thm

*}

ML {*

   Skip_Proof.make_thm @{theory} @{prop "True = False"}

*}

ML {*

fun pthms_of (PBody {thms, ...}) = map #2 thms

val get_names = map #1 o pthms_of

val get_pbodies = map (Future.join o #3) o pthms_of

*}

lemma my_conjIa:

shows "A \<and> B \<Longrightarrow> A \<and> B"

apply(rule conjI)

apply(drule conjunct1)

apply(assumption)

apply(drule conjunct2)

apply(assumption)

done

lemma my_conjIb:

shows "A \<and> B \<Longrightarrow> A \<and> B"

apply(assumption)

done

lemma my_conjIc:

shows "A \<and> B \<Longrightarrow> A \<and> B"

apply(auto)

done

ML {*

@{thm my_conjIa}

  |> Thm.proof_body_of

  |> get_names

*}

ML {*

@{thm my_conjIa}

  |> Thm.proof_body_of

  |> get_pbodies

  |> map get_names

  |> List.concat

*}

ML {*

@{thm my_conjIb}

 |> Thm.proof_body_of

 |> get_pbodies

 |> map get_names

 |> List.concat

*}

ML {*

@{thm my_conjIc}

  |> Thm.proof_body_of

  |> get_pbodies

  |> map get_names

  |> List.concat

*}

ML {*

@{thm my_conjIa}

  |> Thm.proof_body_of

  |> get_pbodies

  |> map get_pbodies

  |> (map o map) get_names

  |> List.concat

  |> List.concat

  |> duplicates (op=)

*}

end