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