src/HOL/Eisbach/eisbach_rule_insts.ML
author haftmann
Thu, 08 Nov 2018 09:11:52 +0100
changeset 69260 0a9688695a1b
parent 62162 dca35981c8fb
child 69593 3dda49e08b9d
permissions -rw-r--r--
removed relics of ASCII syntax for indexed big operators
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60248
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
     1
(*  Title:      HOL/Eisbach/eisbach_rule_insts.ML
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     2
    Author:     Daniel Matichuk, NICTA/UNSW
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     3
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     4
Eisbach-aware variants of the "where" and "of" attributes.
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     5
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     6
Alternate syntax for rule_insts.ML participates in token closures by
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     7
examining the behaviour of Rule_Insts.where_rule and instantiating token
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     8
values accordingly. Instantiations in re-interpretation are done with
60791
e3f2262786ea updated to infer_instantiate;
wenzelm
parents: 60653
diff changeset
     9
infer_instantiate.
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    10
*)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    11
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
    12
structure Eisbach_Rule_Insts: sig end =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    13
struct
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    14
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    15
fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm));
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    16
60909
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    17
val mk_term_type_internal = Logic.protect o Logic.mk_term o Logic.mk_type;
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    18
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    19
fun term_type_cases f g t = 
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    20
  (case (try (Logic.dest_type o Logic.dest_term o Logic.unprotect) t) of
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    21
    SOME T => f T
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    22
  | NONE => 
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    23
    (case (try Logic.dest_term t) of
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    24
      SOME t => g t
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    25
    | NONE => raise Fail "Lost encoded instantiation"))
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    26
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
    27
fun add_thm_insts ctxt thm =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    28
  let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    29
    val tyvars = Thm.fold_terms Term.add_tvars thm [];
60909
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    30
    val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    31
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    32
    val tvars = Thm.fold_terms Term.add_vars thm [];
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    33
    val tvars' = tvars  |> map (Logic.mk_term o Var);
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    34
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    35
    val conj =
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
    36
      Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.cterm_of ctxt |> Drule.mk_term;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    37
  in
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    38
    ((tyvars, tvars), Conjunction.intr thm conj)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    39
  end;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    40
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    41
fun get_thm_insts thm =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    42
  let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    43
    val (thm', insts) = Conjunction.elim thm;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    44
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    45
    val insts' = insts
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    46
      |> Drule.dest_term
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    47
      |> Thm.term_of
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    48
      |> Logic.dest_conjunction_list
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    49
      |> (fn f => fold (fn t => fn (tys, ts) =>
60909
3db3f4154e18 clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents: 60791
diff changeset
    50
          term_type_cases (fn T => (T :: tys, ts)) (fn t => (tys, t :: ts)) t) f ([], []))
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    51
      ||> rev
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    52
      |>> rev;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    53
  in
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    54
    (thm', insts')
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    55
  end;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    56
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
    57
fun instantiate_xis ctxt insts thm =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    58
  let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    59
    val tyvars = Thm.fold_terms Term.add_tvars thm [];
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    60
    val tvars = Thm.fold_terms Term.add_vars thm [];
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    61
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    62
    fun add_inst (xi, t) (Ts, ts) =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    63
      (case AList.lookup (op =) tyvars xi of
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
    64
        SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    65
      | NONE =>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    66
          (case AList.lookup (op =) tvars xi of
60791
e3f2262786ea updated to infer_instantiate;
wenzelm
parents: 60653
diff changeset
    67
            SOME _ => (Ts, (xi, Thm.cterm_of ctxt t) :: ts)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    68
          | NONE => error "indexname not found in thm"));
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    69
60791
e3f2262786ea updated to infer_instantiate;
wenzelm
parents: 60653
diff changeset
    70
    val (instT, inst) = fold add_inst insts ([], []);
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    71
  in
60791
e3f2262786ea updated to infer_instantiate;
wenzelm
parents: 60653
diff changeset
    72
    (Thm.instantiate (instT, []) thm
e3f2262786ea updated to infer_instantiate;
wenzelm
parents: 60653
diff changeset
    73
    |> infer_instantiate ctxt inst
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    74
    COMP_INCR asm_rl)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    75
    |> Thm.adjust_maxidx_thm ~1
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    76
    |> restore_tags thm
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    77
  end;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    78
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    79
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    80
datatype rule_inst =
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    81
  Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    82
| Term_Insts of (indexname * term) list
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    83
| Unchecked_Term_Insts of term option list * term option list;
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    84
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    85
fun mk_pair (t, t') = Logic.mk_conjunction (Logic.mk_term t, Logic.mk_term t');
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    86
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    87
fun dest_pair t = apply2 Logic.dest_term (Logic.dest_conjunction t);
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    88
60248
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    89
fun embed_indexname ((xi, s), f) =
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    90
  let fun wrap_xi xi t = mk_pair (Var (xi, fastype_of t), t);
60248
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    91
  in ((xi, s), f o wrap_xi xi) end;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    92
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    93
fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst);
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    94
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    95
fun read_where_insts (insts, fixes) =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    96
  let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    97
    val insts' =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    98
      if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    99
      then Term_Insts (map (unembed_indexname o Parse_Tools.the_real_val o snd) insts)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   100
      else
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   101
        Named_Insts (map (fn (xi, p) => embed_indexname
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   102
          ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts, fixes);
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   103
  in insts' end;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   104
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   105
fun of_rule thm  (args, concl_args) =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   106
  let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   107
    fun zip_vars _ [] = []
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   108
      | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   109
      | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   110
      | zip_vars [] _ = error "More instantiations than variables in theorem";
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   111
    val insts =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   112
      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   113
      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   114
  in insts end;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   115
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   116
val inst =  Args.maybe Parse_Tools.name_term;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   117
val concl = Args.$$$ "concl" -- Args.colon;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   118
60469
d1ea37df7358 tuned signature;
wenzelm
parents: 60379
diff changeset
   119
fun close_unchecked_insts context ((insts, concl_inst), fixes) =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   120
  let
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   121
    val ctxt = Context.proof_of context;
60469
d1ea37df7358 tuned signature;
wenzelm
parents: 60379
diff changeset
   122
    val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2;
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   123
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   124
    val insts' = insts @ concl_inst;
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   125
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   126
    val term_insts =
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   127
      map (the_list o (Option.map Parse_Tools.the_parse_val)) insts'
60486
17a2dae7d246 redundant: read = check o parse;
wenzelm
parents: 60469
diff changeset
   128
      |> burrow (Syntax.read_terms ctxt1 #> Variable.export_terms ctxt1 ctxt)
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   129
      |> map (try the_single);
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   130
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   131
    val _ =
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   132
      (insts', term_insts)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   133
      |> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ());
60552
742b553d88b2 tuned whitespace;
wenzelm
parents: 60486
diff changeset
   134
    val (insts'', concl_insts'') = chop (length insts) term_insts;
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   135
   in Unchecked_Term_Insts (insts'', concl_insts'') end;
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   136
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   137
fun read_of_insts checked context ((insts, concl_insts), fixes) =
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   138
  if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   139
  then
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   140
    if checked
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   141
    then
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   142
      (fn _ =>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   143
       Term_Insts
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   144
        (map (unembed_indexname o Parse_Tools.the_real_val) (map_filter I (insts @ concl_insts))))
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   145
    else
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   146
      (fn _ =>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   147
        Unchecked_Term_Insts
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   148
          (map (Option.map Parse_Tools.the_real_val) insts,
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   149
            map (Option.map Parse_Tools.the_real_val) concl_insts))
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   150
  else
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   151
    if checked
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   152
    then
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   153
      (fn thm =>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   154
        Named_Insts
60248
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   155
          (apply2
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   156
            (map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   157
            (insts, concl_insts)
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   158
          |> of_rule thm |> map ((fn (xi, (nm, f)) => embed_indexname ((xi, nm), f))), fixes))
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   159
    else
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   160
      let val result = close_unchecked_insts context ((insts, concl_insts), fixes);
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   161
      in fn _ => result end;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   162
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   163
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   164
fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm  =
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   165
      let
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   166
        val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   167
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
   168
        val (thm_insts, thm') = add_thm_insts ctxt thm;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   169
        val (thm'', thm_insts') =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   170
          Rule_Insts.where_rule ctxt insts' fixes thm'
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   171
          |> get_thm_insts;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   172
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   173
        val tyinst =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   174
          ListPair.zip (fst thm_insts, fst thm_insts') |> map (fn ((xi, _), typ) => (xi, typ));
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   175
        val tinst =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   176
          ListPair.zip (snd thm_insts, snd thm_insts') |> map (fn ((xi, _), t) => (xi, t));
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   177
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   178
        val _ =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   179
          map (fn ((xi, _), f) =>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   180
            (case AList.lookup (op =) tyinst xi of
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   181
              SOME typ => f (Logic.mk_type typ)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   182
            | NONE =>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   183
                (case AList.lookup (op =) tinst xi of
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   184
                  SOME t => f t
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   185
                | NONE => error "Lost indexname in instantiated theorem"))) insts;
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   186
      in
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   187
        (thm'' |> restore_tags thm)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   188
      end
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   189
  | read_instantiate_closed ctxt (Unchecked_Term_Insts insts) thm =
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   190
      let
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   191
        val (xis, ts) = ListPair.unzip (of_rule thm insts);
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   192
        val ctxt' = Variable.declare_maxidx (Thm.maxidx_of thm) ctxt;
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   193
        val (ts', ctxt'') = Variable.import_terms false ts ctxt';
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   194
        val ts'' = Variable.export_terms ctxt'' ctxt ts';
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   195
        val insts' = ListPair.zip (xis, ts'');
60653
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
   196
      in instantiate_xis ctxt insts' thm end
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
   197
  | read_instantiate_closed ctxt (Term_Insts insts) thm =
7df8e5b05f5a clarified context;
wenzelm
parents: 60642
diff changeset
   198
      instantiate_xis ctxt insts thm;
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   199
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   200
val _ =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   201
  Theory.setup
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   202
    (Attrib.setup @{binding "where"}
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   203
      (Scan.lift
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   204
        (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
61853
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   205
        >> (fn args =>
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   206
            let val args' = read_where_insts args in
62162
dca35981c8fb Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents: 62135
diff changeset
   207
              fn (context, thm) =>
dca35981c8fb Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents: 62135
diff changeset
   208
                (NONE, SOME (read_instantiate_closed (Context.proof_of context) args' thm))
61853
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   209
            end))
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   210
      "named instantiation of theorem");
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   211
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   212
val _ =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   213
  Theory.setup
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   214
    (Attrib.setup @{binding "of"}
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   215
      (Scan.lift
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   216
        (Args.mode "unchecked" --
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   217
          (Scan.repeat (Scan.unless concl inst) --
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   218
            Scan.optional (concl |-- Scan.repeat inst) [] --
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   219
            Parse.for_fixes)) -- Scan.state >>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   220
      (fn ((unchecked, args), context) =>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   221
        let
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   222
          val read_insts = read_of_insts (not unchecked) context args;
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   223
        in
62162
dca35981c8fb Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents: 62135
diff changeset
   224
          fn (context, thm) =>
61853
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   225
            let val thm' =
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   226
              if Thm.is_free_dummy thm andalso unchecked
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   227
              then Drule.free_dummy_thm
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61852
diff changeset
   228
              else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
62162
dca35981c8fb Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents: 62135
diff changeset
   229
            in (NONE, SOME thm') end
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   230
        end))
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   231
      "positional instantiation of theorem");
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   232
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   233
end;