1 theory Essential

     2 imports FirstStep

     3 begin

     4 

     5 ML {*

     6 fun pretty_helper aux env =

     7   env |> Vartab.dest

     8       |> map aux

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

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

    11       |> pwriteln

    12 

    13 fun pretty_tyenv ctxt tyenv =

    14 let

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

    16   val print = pairself (pretty_typ ctxt)

    17 in

    18   pretty_helper (print o get_typs) tyenv

    19 end

    20 

    21 fun pretty_env ctxt env =

    22 let

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

    24    val print = pairself (pretty_term ctxt)

    25 in

    26    pretty_helper (print o get_trms) env

    27 end

    28 

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

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

    31 

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

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

    34 

    35 fun matcher_inst thy pat trm i =

    36   let

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

    38      val env = nth (Seq.list_of univ) i

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

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

    41   in

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

    43   end

    44 *}

    45 

    46 ML {*

    47   let

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

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

    50      val inst = matcher_inst @{theory} pat trm 1

    51   in

    52      Drule.instantiate_normalize inst @{thm spec}

    53   end

    54 *}

    55 

    56 ML {*

    57 let

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

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

    60    val v = Free ("x", dummyT)

    61 in

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

    63 end

    64 *}

    65 

    66 ML {*

    67    val my_thm =

    68    let

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

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

    71 

    72       val Pt_implies_Qt =

    73         Thm.assume assm1

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

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

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

    77 

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

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

    80    in

    81       Qt

    82       |> Thm.implies_intr assm2

    83       |> Thm.implies_intr assm1

    84    end

    85 *}

    86 

    87 local_setup {*

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

    89 *}

    90 

    91 local_setup {*

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

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

    94 *}

    95 

    96 (* pp 62 *)

    97 

    98 ML {*

    99    Thm.reflexive @{cterm "True"}

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

   101     |> pretty_thm @{context}

   102     |> pwriteln

   103 *}

   104 

   105 

   106 ML {*

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

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

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

   110 *}

   111 

   112 ML {*

   113 fun atomize_thm thm =

   114 let

   115   val thm' = forall_intr_vars thm

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

   117 in

   118   Raw_Simplifier.rewrite_rule [thm''] thm'

   119 end

   120 *}

   121 

   122 ML {*

   123   @{thm list.induct} |> atomize_thm

   124 *}

   125 

   126 ML {*

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

   128 *}

   129 

   130 ML {*

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

   132 val get_names = map #1 o pthms_of

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

   134 *}

   135 

   136 lemma my_conjIa:

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

   138 apply(rule conjI)

   139 apply(drule conjunct1)

   140 apply(assumption)

   141 apply(drule conjunct2)

   142 apply(assumption)

   143 done

   144 

   145 lemma my_conjIb:

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

   147 apply(assumption)

   148 done

   149 

   150 lemma my_conjIc:

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

   152 apply(auto)

   153 done

   154 

   155 

   156 ML {*

   157 @{thm my_conjIa}

   158   |> Thm.proof_body_of

   159   |> get_names

   160 *}

   161 

   162 ML {*

   163 @{thm my_conjIa}

   164   |> Thm.proof_body_of

   165   |> get_pbodies

   166   |> map get_names

   167   |> List.concat

   168 *}

   169 

   170 ML {*

   171 @{thm my_conjIb}

   172  |> Thm.proof_body_of

   173  |> get_pbodies

   174  |> map get_names

   175  |> List.concat

   176 *}

   177 

   178 ML {*

   179 @{thm my_conjIc}

   180   |> Thm.proof_body_of

   181   |> get_pbodies

   182   |> map get_names

   183   |> List.concat

   184 *}

   185 

   186 ML {*

   187 @{thm my_conjIa}

   188   |> Thm.proof_body_of

   189   |> get_pbodies

   190   |> map get_pbodies

   191   |> (map o map) get_names

   192   |> List.concat

   193   |> List.concat

   194   |> duplicates (op=)

   195 *}

   196 

   197 end