Mercurial Mercurial > hg > nominal2 / comparison
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_dt_alpha.ML
changeset 2314 1a14c4171a51
parent 2313 25d2cdf7d7e4
child 2316 08bbde090a17
equal deleted inserted replaced
2313:25d2cdf7d7e4 2314:1a14c4171a51 
   399 
   399 
   400 
   400 
   401 
   401 
   402 (** transitivity proof for alphas **)
 
   402 (** transitivity proof for alphas **)
 
   403 
   403 
       
   404 (* applies cases rules and resolves them with the last premise *)
 
   404 fun ecases_tac cases = 
   405 fun ecases_tac cases = 
   405   Subgoal.FOCUS (fn {prems, ...} =>
 
   406   Subgoal.FOCUS (fn {prems, ...} =>
 
   406     HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
 
   407     HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
 
   407 
   408 
   408 fun aatac pred_names = 
   409 fun aatac pred_names = 
   409   SUBPROOF (fn {prems, context, ...} =>
 
   410   SUBPROOF (fn {prems, context, ...} =>
 
   410     HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
 
   411     HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
 
   411   
   412   
       
   413 (* instantiates exI with the permutation p + q *)
 
   412 val perm_inst_tac =
 
   414 val perm_inst_tac =
 
   413   Subgoal.FOCUS (fn {params, ...} => 
   415   Subgoal.FOCUS (fn {params, ...} => 
   414     let
 
   416     let
 
   415       val (p, q) = pairself snd (last2 params)
 
   417       val (p, q) = pairself snd (last2 params)
 
   416       val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
 
   418       val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
 
   423 let
 
   425 let
 
   424   val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
 
   426   val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
 
   425 in
 
   427 in
 
   426   resolve_tac intros
 
   428   resolve_tac intros
 
   427   THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
   429   THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
   428     TRY o EVERY' 
   430     TRY o EVERY'   (* if binders are present *)
 
   429       [ etac @{thm exE},
 
   431       [ etac @{thm exE},
 
   430         etac @{thm exE},
 
   432         etac @{thm exE},
 
   431         perm_inst_tac ctxt, 
   433         perm_inst_tac ctxt, 
   432         resolve_tac @{thms alpha_trans_eqvt}, 
   434         resolve_tac @{thms alpha_trans_eqvt}, 
   433         atac,
 
   435         atac,
 
   445   HEADGOAL (rtac induct THEN_ALL_NEW  
   447   HEADGOAL (rtac induct THEN_ALL_NEW  
   446     EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
   448     EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
   447              ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
 
   449              ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
 
   448 end
 
   450 end
 
   449 
   451 
   450 xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
 
   452 fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
 
   451 let
 
   453 let
 
   452   val lhs = alpha_trm $ arg1 $ arg2
 
   454   val lhs = alpha_trm $ arg1 $ arg2
 
   453   val mid = alpha_trm $ arg2 $ (Bound 0)
 
   455   val mid = alpha_trm $ arg2 $ (Bound 0)
 
   454   val rhs = alpha_trm $ arg1 $ (Bound 0) 
   456   val rhs = alpha_trm $ arg1 $ (Bound 0) 
   455 in
 
   457 in
nominal2