Nominal/nominal_dt_rawfuns.ML
changeset 3045 d0ad264f8c4f
parent 2957 01ff621599bc
child 3061 cfc795473656
equal deleted inserted replaced
3044:a609eea06119 3045:d0ad264f8c4f
   259 
   259 
   260     val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
   260     val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
   261  
   261  
   262     val {fs, simps, inducts, ...} = info; 
   262     val {fs, simps, inducts, ...} = info; 
   263 
   263 
   264     val morphism = ProofContext.export_morphism lthy'' lthy
   264     val morphism = Proof_Context.export_morphism lthy'' lthy
   265     val simps_exp = map (Morphism.thm morphism) (the simps)
   265     val simps_exp = map (Morphism.thm morphism) (the simps)
   266     val inducts_exp = map (Morphism.thm morphism) (the inducts)
   266     val inducts_exp = map (Morphism.thm morphism) (the inducts)
   267     
   267     
   268     val (fvs', fv_bns') = chop (length fv_frees) fs
   268     val (fvs', fv_bns') = chop (length fv_frees) fs
   269 
   269 
   332     
   332     
   333       val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
   333       val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
   334 
   334 
   335       val {fs, simps, ...} = info;
   335       val {fs, simps, ...} = info;
   336 
   336 
   337       val morphism = ProofContext.export_morphism lthy'' lthy
   337       val morphism = Proof_Context.export_morphism lthy'' lthy
   338       val simps_exp = map (Morphism.thm morphism) (the simps)
   338       val simps_exp = map (Morphism.thm morphism) (the simps)
   339     in
   339     in
   340       (fs, simps_exp, lthy'')
   340       (fs, simps_exp, lthy'')
   341     end
   341     end
   342 
   342 
   465        THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
   465        THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
   466 
   466 
   467 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   467 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   468   HEADGOAL
   468   HEADGOAL
   469     (Object_Logic.full_atomize_tac
   469     (Object_Logic.full_atomize_tac
   470      THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
   470      THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))  
   471      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
   471      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
   472 
   472 
   473 fun mk_eqvt_goal pi const arg =
   473 fun mk_eqvt_goal pi const arg =
   474   let
   474   let
   475     val lhs = mk_perm pi (const $ arg)
   475     val lhs = mk_perm pi (const $ arg)
   496       val insts = map (single o SOME) arg_names
   496       val insts = map (single o SOME) arg_names
   497       val const_names = map (fst o dest_Const) consts      
   497       val const_names = map (fst o dest_Const) consts      
   498     in
   498     in
   499       Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
   499       Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
   500         prove_eqvt_tac insts ind_thms const_names simps context)
   500         prove_eqvt_tac insts ind_thms const_names simps context)
   501       |> ProofContext.export ctxt'' ctxt
   501       |> Proof_Context.export ctxt'' ctxt
   502     end
   502     end
   503 
   503 
   504 
   504 
   505 end (* structure *)
   505 end (* structure *)
   506 
   506