Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_mutual.ML
changeset 3239 67370521c09c
parent 3231 188826f1ccdb
child 3243 c4f31f1564b7 
--- a/Nominal/nominal_mutual.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_mutual.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -138,7 +138,7 @@
         val ((f, (_, f_defthm)), lthy') =
           Local_Theory.define
             ((Binding.name fname, mixfix),
-              ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+              ((Binding.concealed (Binding.name (fname ^ "_def")), []),
               Term.subst_bound (fsum, f_def))) lthy
       in
         (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
@@ -156,8 +156,6 @@
 
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   let
-    val thy = Proof_Context.theory_of ctxt
-
     val oqnames = map fst pre_qs
     val (qs, _) = Variable.variant_fixes oqnames ctxt
       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
@@ -167,13 +165,13 @@
     val args = map inst pre_args
     val rhs = inst pre_rhs
 
-    val cqs = map (cterm_of thy) qs
-    val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt
+    val cqs = map (Thm.cterm_of ctxt) qs
+    val (ags, ctxt') = fold_map Thm.assume_hyps (map (Thm.cterm_of ctxt) gs) ctxt
 
     val import = fold Thm.forall_elim cqs
       #> fold Thm.elim_implies ags
 
-    val export = fold_rev (Thm.implies_intr o cprop_of) ags
+    val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags
       #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   in
     F ctxt' (f, qs, gs, args, rhs) import export
@@ -242,8 +240,7 @@
 
 fun mk_applied_form ctxt caTs thm =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
+    val xs = map_index (fn (i,T) => Thm.cterm_of ctxt (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
     fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
     |> Conv.fconv_rule (Thm.beta_conversion true)
@@ -253,7 +250,7 @@
 
 fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
   let
-    val cert = cterm_of (Proof_Context.theory_of ctxt)
+    val cert = Thm.cterm_of ctxt
     val newPs =
       map2 (fn Pname => fn MutualPart {cargTs, ...} =>
           Free (Pname, cargTs ---> HOLogic.boolT))
@@ -314,7 +311,7 @@
 
     (* extracting the acc-premises from the induction theorems *)
     val acc_prems = 
-     map prop_of induct_thms
+     map Thm.prop_of induct_thms
      |> map2 forall_elim_list argss 
      |> map (strip_qnt_body @{const_name Pure.all})
      |> map (curry Logic.nth_prem 1)
@@ -333,19 +330,21 @@
 
     val induct_thm = case induct_thms of
         [thm] => thm
-          |> Drule.gen_all 
+          |> Drule.gen_all (Variable.maxidx_of ctxt')
           |> Thm.permute_prems 0 1
-          |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
+          |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm)
       | thms => thms
-          |> map Drule.gen_all 
+          |> map (Drule.gen_all (Variable.maxidx_of ctxt'))
           |> map (Rule_Cases.add_consumes 1)
           |> snd o Rule_Cases.strict_mutual_rule ctxt'
           |> atomize_concl ctxt'
 
-    fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
+    fun tac ctxt thm =
+      rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt
   in
     Goal.prove ctxt' (flat arg_namess) [] goal
-      (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
+      (fn {context = ctxt'', ...} =>
+        HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms)))
     |> singleton (Proof_Context.export ctxt' ctxt)
     |> split_conj_thm
     |> map (fn th => th RS mp)
@@ -435,7 +434,7 @@
     val G_name_aux = G_name ^ "_aux"
     val subst = [(G, Free (G_name_aux, G_type))]
     val GIntros_aux = GIntro_thms
-      |> map prop_of
+      |> map Thm.prop_of
       |> map (Term.subst_free subst)
       |> map (subst_all case_sum_exp)
 
@@ -478,15 +477,16 @@
       (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1)))
 
     fun aux_tac thm = 
-      rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (simpset1 addsimps [inj_thm]))
+      rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW
+      asm_full_simp_tac (simpset1 addsimps [inj_thm])
     
     val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 
       (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
-      |> Drule.gen_all
+      |> Drule.gen_all (Variable.maxidx_of lthy''')
     val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 
       (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE
         (map (aux_tac o simplify simpset0) GIntro_aux_thms))))
-      |> Drule.gen_all
+      |> Drule.gen_all (Variable.maxidx_of lthy''')
 
     val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
       (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
nominal2