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