1(* Title: HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML 2 Author: Jasmin Blanchette, Inria, LORIA, MPII 3 Copyright 2016 4 5Proof method for proving uniqueness of corecursive equations ("corec_unique"). 6*) 7 8signature BNF_GFP_GREC_UNIQUE_SUGAR = 9sig 10 val corec_unique_tac: Proof.context -> int -> tactic 11end; 12 13structure BNF_GFP_Grec_Unique_Sugar : BNF_GFP_GREC_UNIQUE_SUGAR = 14struct 15 16open BNF_Util 17open BNF_GFP_Grec 18open BNF_GFP_Grec_Sugar_Util 19open BNF_GFP_Grec_Sugar 20 21fun corec_unique_tac ctxt = 22 Subgoal.FOCUS (fn {context = ctxt, prems, concl, ...} => 23 let 24 (* Workaround for odd name clash for goals with "x" in their context *) 25 val (_, ctxt) = ctxt 26 |> yield_singleton (mk_Frees "x") \<^typ>\<open>unit\<close>; 27 28 val code_thm = (if null prems then error "No premise" else hd prems) 29 |> Object_Logic.rulify ctxt; 30 val code_goal = Thm.prop_of code_thm; 31 32 val (fun_t, args) = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop code_goal))) 33 handle TERM _ => error "Wrong format for first premise"; 34 35 val _ = is_Free fun_t orelse 36 error ("Expected free variable as function in premise, found " ^ 37 Syntax.string_of_term ctxt fun_t); 38 val _ = 39 (case filter_out is_Var args of 40 [] => () 41 | arg :: _ => 42 error ("Expected universal variable as argument to function in premise, found " ^ 43 Syntax.string_of_term ctxt arg)); 44 45 val fun_T = fastype_of fun_t; 46 val (arg_Ts, res_T) = strip_type fun_T; 47 48 val num_args_in_concl = length (snd (strip_comb (fst (HOLogic.dest_eq 49 (HOLogic.dest_Trueprop (Thm.term_of concl)))))) 50 handle TERM _ => error "Wrong format for conclusion"; 51 52 val (corec_info, corec_parse_info) = 53 (case maybe_corec_info_of ctxt res_T of 54 SOME (info as {buffer, ...}) => (info, corec_parse_info_of ctxt arg_Ts res_T buffer) 55 | NONE => error ("No corecursor for " ^ quote (Syntax.string_of_typ ctxt res_T) ^ 56 " (use " ^ quote (#1 \<^command_keyword>\<open>coinduction_upto\<close>) ^ " to derive it)")); 57 58 val Type (fpT_name, _) = res_T; 59 60 val parsed_eq = parse_corec_equation ctxt [fun_t] code_goal; 61 val explored_eq = 62 explore_corec_equation ctxt false false "" fun_t corec_parse_info res_T parsed_eq; 63 64 val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_t explored_eq ctxt; 65 val eq_corecUU = derive_eq_corecUU ctxt corec_info fun_t corecUU_arg code_thm; 66 67 val unique' = derive_unique ctxt Morphism.identity code_goal corec_info fpT_name eq_corecUU 68 |> funpow num_args_in_concl (fn thm => thm RS fun_cong); 69 in 70 HEADGOAL ((K all_tac APPEND' rtac ctxt sym) THEN' rtac ctxt unique' THEN' 71 REPEAT_DETERM_N num_args_in_concl o rtac ctxt ext) 72 end) ctxt THEN' 73 etac ctxt thin_rl; 74 75end; 76