117658Sjulian(* Title: HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML 217658Sjulian Author: Jasmin Blanchette, Inria, LORIA, MPII 317658Sjulian Copyright 2016 417658Sjulian 517658SjulianProof method for proving uniqueness of corecursive equations ("corec_unique"). 617658Sjulian*) 717658Sjulian 817658Sjuliansignature BNF_GFP_GREC_UNIQUE_SUGAR = 917658Sjuliansig 1017658Sjulian val corec_unique_tac: Proof.context -> int -> tactic 1117658Sjulianend; 1217658Sjulian 1317658Sjulianstructure BNF_GFP_Grec_Unique_Sugar : BNF_GFP_GREC_UNIQUE_SUGAR = 1417658Sjulianstruct 1517658Sjulian 1617658Sjulianopen BNF_Util 1717658Sjulianopen BNF_GFP_Grec 1817658Sjulianopen BNF_GFP_Grec_Sugar_Util 1917658Sjulianopen BNF_GFP_Grec_Sugar 2017658Sjulian 2117658Sjulianfun corec_unique_tac ctxt = 2217658Sjulian Subgoal.FOCUS (fn {context = ctxt, prems, concl, ...} => 2317658Sjulian let 2417658Sjulian (* Workaround for odd name clash for goals with "x" in their context *) 2517658Sjulian val (_, ctxt) = ctxt 2617658Sjulian |> yield_singleton (mk_Frees "x") \<^typ>\<open>unit\<close>; 2717658Sjulian 2817658Sjulian val code_thm = (if null prems then error "No premise" else hd prems) 2917658Sjulian |> Object_Logic.rulify ctxt; 3017658Sjulian val code_goal = Thm.prop_of code_thm; 3117658Sjulian 3217658Sjulian val (fun_t, args) = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop code_goal))) 3317658Sjulian handle TERM _ => error "Wrong format for first premise"; 3417658Sjulian 3517658Sjulian val _ = is_Free fun_t orelse 3617658Sjulian error ("Expected free variable as function in premise, found " ^ 3717658Sjulian Syntax.string_of_term ctxt fun_t); 3817658Sjulian val _ = 3950477Speter (case filter_out is_Var args of 4017658Sjulian [] => () 4117658Sjulian | arg :: _ => 4217658Sjulian error ("Expected universal variable as argument to function in premise, found " ^ 4333445Seivind Syntax.string_of_term ctxt arg)); 4428976Sbde 4528976Sbde val fun_T = fastype_of fun_t; 4617658Sjulian val (arg_Ts, res_T) = strip_type fun_T; 4717658Sjulian 4817658Sjulian val num_args_in_concl = length (snd (strip_comb (fst (HOLogic.dest_eq 4950107Smsmith (HOLogic.dest_Trueprop (Thm.term_of concl)))))) 5060041Sphk handle TERM _ => error "Wrong format for conclusion"; 5131275Sbde 5217658Sjulian val (corec_info, corec_parse_info) = 5317658Sjulian (case maybe_corec_info_of ctxt res_T of 5441137Smsmith SOME (info as {buffer, ...}) => (info, corec_parse_info_of ctxt arg_Ts res_T buffer) 5517658Sjulian | NONE => error ("No corecursor for " ^ quote (Syntax.string_of_typ ctxt res_T) ^ 5655539Sluoqi " (use " ^ quote (#1 \<^command_keyword>\<open>coinduction_upto\<close>) ^ " to derive it)")); 5721776Sbde 5867365Sjhb val Type (fpT_name, _) = res_T; 5939237Sgibbs 6017658Sjulian val parsed_eq = parse_corec_equation ctxt [fun_t] code_goal; 6117658Sjulian val explored_eq = 6217658Sjulian explore_corec_equation ctxt false false "" fun_t corec_parse_info res_T parsed_eq; 6349558Sphk 6417658Sjulian val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_t explored_eq ctxt; 6517658Sjulian val eq_corecUU = derive_eq_corecUU ctxt corec_info fun_t corecUU_arg code_thm; 6617658Sjulian 6726812Speter val unique' = derive_unique ctxt Morphism.identity code_goal corec_info fpT_name eq_corecUU 6817658Sjulian |> funpow num_args_in_concl (fn thm => thm RS fun_cong); 6917658Sjulian in 7017658Sjulian HEADGOAL ((K all_tac APPEND' rtac ctxt sym) THEN' rtac ctxt unique' THEN' 7117658Sjulian REPEAT_DETERM_N num_args_in_concl o rtac ctxt ext) 7217658Sjulian end) ctxt THEN' 7317658Sjulian etac ctxt thin_rl; 7417658Sjulian 7517658Sjulianend; 7617658Sjulian