nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:07fb696efa3d
+:7a3d86050e72
 in
 lthy2
 end
 *}
+ML {*
+fun spec_frees_tac [] = []
+| spec_frees_tac (x::xs) =
+let
+val spec' =  Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec}
+in
+(rtac spec')::(spec_frees_tac xs)
+end
+*}
+ML {*
+val prepare_tac = CSUBGOAL (fn (concl, i) =>
+let
+val vrs = Thm.add_cterm_frees concl []
+in
+EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i
+end)
+*}
 lemma procedure:
 assumes a: "A"
 and     b: "A \<Longrightarrow> B"
 and     c: "B = C"
 and     d: "C = D"
 [SOME (cterm_of thy rtrm'),
 SOME (cterm_of thy reg_goal),
 SOME (cterm_of thy inj_goal)]
 @{thm procedure}
 end
+*}
-fun procedure_tac rthm =
+ML {*
+fun procedure_tac rthm ctxt =
+prepare_tac THEN'
 Subgoal.FOCUS (fn {context, concl, ...} =>
 let
 val rthm' = atomize_thm rthm
 val rule = procedure_inst context (prop_of rthm') (term_of concl)
 in
 EVERY1 [rtac rule, rtac rthm']
-end)
+end) ctxt
 *}
+ML {*
 (* FIXME: allex_prs and lambda_prs can be one function *)
-ML {*
 fun allex_prs_tac lthy quot =
 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
 THEN' (quotient_tac quot);
 *}