src/Pure/logic.ML
author wenzelm
Sun, 31 Dec 2023 12:40:10 +0100
changeset 79404 cb19148c0b95
parent 79399 11b53e039f6f
child 79407 c6c2e41cac1c
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
     1
(*  Title:      Pure/logic.ML
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 28856
diff changeset
     3
    Author:     Makarius
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
     5
Abstract syntax operations of the Pure meta-logic.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
     8
signature LOGIC =
4345
7e9436ffb813 tuned term order;
wenzelm
parents: 4318
diff changeset
     9
sig
46217
7b19666f0e3d renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents: 46215
diff changeset
    10
  val all_const: typ -> term
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
    11
  val all: term -> term -> term
61655
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
    12
  val dependent_all_name: string * term -> term -> term
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
    13
  val is_all: term -> bool
74525
c960bfcb91db discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents: 74509
diff changeset
    14
  val dest_all_global: term -> (string * typ) * term
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46217
diff changeset
    15
  val list_all: (string * typ) list * term -> term
60454
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
    16
  val all_constraint: (string -> typ option) -> string * string -> term -> term
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
    17
  val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
18181
wenzelm
parents: 18029
diff changeset
    18
  val mk_equals: term * term -> term
wenzelm
parents: 18029
diff changeset
    19
  val dest_equals: term -> term * term
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
    20
  val implies: term
18181
wenzelm
parents: 18029
diff changeset
    21
  val mk_implies: term * term -> term
wenzelm
parents: 18029
diff changeset
    22
  val dest_implies: term -> term * term
wenzelm
parents: 18029
diff changeset
    23
  val list_implies: term list * term -> term
wenzelm
parents: 18029
diff changeset
    24
  val strip_imp_prems: term -> term list
wenzelm
parents: 18029
diff changeset
    25
  val strip_imp_concl: term -> term
wenzelm
parents: 18029
diff changeset
    26
  val strip_prems: int * term list * term -> term list * term
21576
8c11b1ce2f05 simplified Logic.count_prems;
wenzelm
parents: 21520
diff changeset
    27
  val count_prems: term -> int
74509
f24ade4ff3cc clarified signature;
wenzelm
parents: 74281
diff changeset
    28
  val no_prems: term -> bool
18181
wenzelm
parents: 18029
diff changeset
    29
  val nth_prem: int * term -> term
63056
9b95ae9ec671 defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents: 61655
diff changeset
    30
  val close_term: (string * term) list -> term -> term
9b95ae9ec671 defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents: 61655
diff changeset
    31
  val close_prop: (string * term) list -> term list -> term -> term
63063
wenzelm
parents: 63056
diff changeset
    32
  val close_prop_constraint: (string -> typ option) ->
wenzelm
parents: 63056
diff changeset
    33
    (string * string) list -> term list -> term -> term
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
    34
  val true_prop: term
19125
59b26248547b simplified Pure conjunction, based on actual const;
wenzelm
parents: 19103
diff changeset
    35
  val conjunction: term
18181
wenzelm
parents: 18029
diff changeset
    36
  val mk_conjunction: term * term -> term
12757
b76a4376cfcb added mk_conjunction_list;
wenzelm
parents: 12137
diff changeset
    37
  val mk_conjunction_list: term list -> term
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
    38
  val mk_conjunction_balanced: term list -> term
18469
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
    39
  val dest_conjunction: term -> term * term
19425
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
    40
  val dest_conjunction_list: term -> term list
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
    41
  val dest_conjunction_balanced: int -> term -> term list
18469
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
    42
  val dest_conjunctions: term -> term list
18181
wenzelm
parents: 18029
diff changeset
    43
  val strip_horn: term -> term list * term
21520
63c73f461eec added type_map;
wenzelm
parents: 21016
diff changeset
    44
  val mk_type: typ -> term
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
    45
  val dest_type: term -> typ
21520
63c73f461eec added type_map;
wenzelm
parents: 21016
diff changeset
    46
  val type_map: (term -> term) -> typ -> typ
76785
9e5a27486ca2 tuned signature;
wenzelm
parents: 74525
diff changeset
    47
  val class_suffix: string
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
    48
  val const_of_class: class -> string
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
    49
  val class_of_const: string -> class
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
    50
  val mk_of_class: typ * class -> term
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
    51
  val dest_of_class: term -> typ * class
35854
d452abc96459 Logic.mk_of_sort convenience;
wenzelm
parents: 35845
diff changeset
    52
  val mk_of_sort: typ * sort -> term list
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
    53
  val name_classrel: string * string -> string
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
    54
  val mk_classrel: class * class -> term
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
    55
  val dest_classrel: term -> class * class
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
    56
  val name_arities: arity -> string list
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
    57
  val name_arity: string * sort list * class -> string
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
    58
  val mk_arities: arity -> term list
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69023
diff changeset
    59
  val mk_arity: string * sort list * class -> term
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
    60
  val dest_arity: term -> string * sort list * class
79397
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
    61
  val present_sorts: sort Ord_List.T -> Types.set ->
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
    62
    {present: (typ * sort) list, extra: sort Ord_List.T}
70811
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
    63
  val dummy_tfree: sort -> typ
70436
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
    64
  type unconstrain_context =
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
    65
   {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
70435
52fbcf7a61f8 tuned signature;
wenzelm
parents: 70384
diff changeset
    66
    constraints: ((typ * class) * term) list,
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
    67
    outer_constraints: (typ * class) list}
77869
1156aa9db7f5 backout 4a174bea55e2;
wenzelm
parents: 77730
diff changeset
    68
  val unconstrainT: sort list -> term -> unconstrain_context * term
18181
wenzelm
parents: 18029
diff changeset
    69
  val protectC: term
wenzelm
parents: 18029
diff changeset
    70
  val protect: term -> term
wenzelm
parents: 18029
diff changeset
    71
  val unprotect: term -> term
19775
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
    72
  val mk_term: term -> term
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
    73
  val dest_term: term -> term
18181
wenzelm
parents: 18029
diff changeset
    74
  val occs: term * term -> bool
wenzelm
parents: 18029
diff changeset
    75
  val close_form: term -> term
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
    76
  val combound: term * int * int -> term
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
    77
  val rlist_abs: (string * typ) list * term -> term
32023
2d071ac5032f export incr_tvar_same;
wenzelm
parents: 32020
diff changeset
    78
  val incr_tvar_same: int -> typ Same.operation
2d071ac5032f export incr_tvar_same;
wenzelm
parents: 32020
diff changeset
    79
  val incr_tvar: int -> typ -> typ
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
    80
  val incr_indexes_operation: {fixed: string list, Ts: typ list, inc: int, level: int} ->
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
    81
    term Same.operation
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
    82
  val incr_indexes: typ list * int -> term -> term
18181
wenzelm
parents: 18029
diff changeset
    83
  val lift_abs: int -> term -> term -> term
wenzelm
parents: 18029
diff changeset
    84
  val lift_all: int -> term -> term -> term
wenzelm
parents: 18029
diff changeset
    85
  val strip_assums_hyp: term -> term list
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
    86
  val strip_assums_concl: term -> term
18181
wenzelm
parents: 18029
diff changeset
    87
  val strip_params: term -> (string * typ) list
23597
ab67175ca8a5 simplified has_meta_prems;
wenzelm
parents: 23418
diff changeset
    88
  val has_meta_prems: term -> bool
18181
wenzelm
parents: 18029
diff changeset
    89
  val flatten_params: int -> term -> term
45328
e5b33eecbf6e tuned signature;
wenzelm
parents: 43329
diff changeset
    90
  val list_rename_params: string list -> term -> term
e5b33eecbf6e tuned signature;
wenzelm
parents: 43329
diff changeset
    91
  val assum_pairs: int * term -> (term * term) list
30554
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
    92
  val assum_problems: int * term -> (term -> term) * term list * term
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 67721
diff changeset
    93
  val bad_schematic: indexname -> string
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 67721
diff changeset
    94
  val bad_fixed: string -> string
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
    95
  val varifyT_global: typ -> typ
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
    96
  val unvarifyT_global: typ -> typ
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
    97
  val varify_types_global: term -> term
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
    98
  val unvarify_types_global: term -> term
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
    99
  val varify_global: term -> term
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   100
  val unvarify_global: term -> term
18181
wenzelm
parents: 18029
diff changeset
   101
  val get_goal: term -> int -> term
wenzelm
parents: 18029
diff changeset
   102
  val goal_params: term -> int -> term * term list
wenzelm
parents: 18029
diff changeset
   103
  val prems_of_goal: term -> int -> term list
wenzelm
parents: 18029
diff changeset
   104
  val concl_of_goal: term -> int -> term
4345
7e9436ffb813 tuned term order;
wenzelm
parents: 4318
diff changeset
   105
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   107
structure Logic : LOGIC =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
struct
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   109
4345
7e9436ffb813 tuned term order;
wenzelm
parents: 4318
diff changeset
   110
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
(*** Abstract syntax operations on the meta-connectives ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
23238
3de6e253efc4 added is_atomic;
wenzelm
parents: 22893
diff changeset
   113
(** all **)
5041
a1d0a6d555cd Goals may now contain assumptions, which are not returned.
nipkow
parents: 4822
diff changeset
   114
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   115
fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
46217
7b19666f0e3d renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents: 46215
diff changeset
   116
7b19666f0e3d renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents: 46215
diff changeset
   117
fun all v t = all_const (Term.fastype_of v) $ lambda v t;
61655
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   118
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   119
fun dependent_all_name (x, v) t =
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   120
  let
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   121
    val x' = if x = "" then Term.term_name v else x;
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   122
    val T = Term.fastype_of v;
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   123
    val t' = Term.abstract_over (v, t);
f217bbe4e93e avoid vacuous quantification, as usual for shared variable scope;
wenzelm
parents: 61654
diff changeset
   124
  in if Term.is_dependent t' then all_const T $ Abs (x', T, t') else t end;
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   125
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   126
fun is_all (Const ("Pure.all", _) $ Abs _) = true
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   127
  | is_all _ = false;
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   128
74525
c960bfcb91db discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents: 74509
diff changeset
   129
fun dest_all_global t =
c960bfcb91db discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents: 74509
diff changeset
   130
  (case t of
c960bfcb91db discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents: 74509
diff changeset
   131
    Const ("Pure.all", _) $ (u as Abs _) => Term.dest_abs_global u
c960bfcb91db discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents: 74509
diff changeset
   132
  | _ => raise TERM ("dest_all", [t]));
18762
9098c92a945f added dest_all;
wenzelm
parents: 18499
diff changeset
   133
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46217
diff changeset
   134
fun list_all ([], t) = t
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46217
diff changeset
   135
  | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46217
diff changeset
   136
18762
9098c92a945f added dest_all;
wenzelm
parents: 18499
diff changeset
   137
60454
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   138
(* operations before type-inference *)
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   139
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   140
local
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   141
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   142
fun abs_body default_type z tm =
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   143
  let
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   144
    fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   145
      | abs lev (t $ u) = abs lev t $ abs lev u
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   146
      | abs lev (a as Free (x, T)) =
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   147
          if x = z then
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   148
            Type.constraint (the_default dummyT (default_type x))
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   149
              (Type.constraint T (Bound lev))
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   150
          else a
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   151
      | abs _ a = a;
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   152
  in abs 0 (Term.incr_boundvars 1 tm) end;
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   153
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   154
in
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   155
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   156
fun all_constraint default_type (y, z) t =
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   157
  all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   158
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   159
fun dependent_all_constraint default_type (y, z) t =
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   160
  let val t' = abs_body default_type z t
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   161
  in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   162
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   163
end;
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   164
a4c6b278f3a7 eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
wenzelm
parents: 59787
diff changeset
   165
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(** equality **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   168
fun mk_equals (t, u) =
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   169
  let val T = Term.fastype_of t
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   170
  in Const ("Pure.eq", T --> T --> propT) $ t $ u end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   172
fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
20883
b432f20a47ca removed is_equals, is_implies;
wenzelm
parents: 20630
diff changeset
   173
  | dest_equals t = raise TERM ("dest_equals", [t]);
637
b344bf624143 added is_equals: term -> bool;
wenzelm
parents: 585
diff changeset
   174
b344bf624143 added is_equals: term -> bool;
wenzelm
parents: 585
diff changeset
   175
70811
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
   176
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
(** implies **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   179
val implies = Const ("Pure.imp", propT --> propT --> propT);
27334
3f17273766f2 added all, is_all;
wenzelm
parents: 26424
diff changeset
   180
20883
b432f20a47ca removed is_equals, is_implies;
wenzelm
parents: 20630
diff changeset
   181
fun mk_implies (A, B) = implies $ A $ B;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   183
fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B)
20883
b432f20a47ca removed is_equals, is_implies;
wenzelm
parents: 20630
diff changeset
   184
  | dest_implies A = raise TERM ("dest_implies", [A]);
5041
a1d0a6d555cd Goals may now contain assumptions, which are not returned.
nipkow
parents: 4822
diff changeset
   185
4822
2733e21814fe added mk_cond_defpair, mk_defpair;
wenzelm
parents: 4693
diff changeset
   186
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
(** nested implications **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   189
(* [A1,...,An], B  goes to  A1\<Longrightarrow>...An\<Longrightarrow>B  *)
18181
wenzelm
parents: 18029
diff changeset
   190
fun list_implies ([], B) = B
wenzelm
parents: 18029
diff changeset
   191
  | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   193
(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to  [A1,...,An], where B is not an implication *)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   194
fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
  | strip_imp_prems _ = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   197
(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to B, where B is not an implication *)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   198
fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
  | strip_imp_concl A = A : term;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   201
(*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B)
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   202
    goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
  if  i<0 or else i too big then raises  TERM*)
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   204
fun strip_prems (0, As, B) = (As, B)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   205
  | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) =
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   206
        strip_prems (i-1, A::As, B)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
  | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
16130
38b111451155 added nth_prem;
wenzelm
parents: 15596
diff changeset
   209
(*Count premises -- quicker than (length o strip_prems) *)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   210
fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
21576
8c11b1ce2f05 simplified Logic.count_prems;
wenzelm
parents: 21520
diff changeset
   211
  | count_prems _ = 0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
74509
f24ade4ff3cc clarified signature;
wenzelm
parents: 74281
diff changeset
   213
fun no_prems (Const ("Pure.imp", _) $ _ $ _) = false
f24ade4ff3cc clarified signature;
wenzelm
parents: 74281
diff changeset
   214
  | no_prems _ = true;
f24ade4ff3cc clarified signature;
wenzelm
parents: 74281
diff changeset
   215
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   216
(*Select Ai from A1\<Longrightarrow>...Ai\<Longrightarrow>B*)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   217
fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   218
  | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
16130
38b111451155 added nth_prem;
wenzelm
parents: 15596
diff changeset
   219
  | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
38b111451155 added nth_prem;
wenzelm
parents: 15596
diff changeset
   220
13659
3cf622f6b0b2 Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents: 12902
diff changeset
   221
(*strip a proof state (Horn clause):
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   222
  B1 \<Longrightarrow> ... Bn \<Longrightarrow> C   goes to   ([B1, ..., Bn], C) *)
13659
3cf622f6b0b2 Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents: 12902
diff changeset
   223
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
3cf622f6b0b2 Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents: 12902
diff changeset
   224
4822
2733e21814fe added mk_cond_defpair, mk_defpair;
wenzelm
parents: 4693
diff changeset
   225
63063
wenzelm
parents: 63056
diff changeset
   226
(* close -- omit vacuous quantifiers *)
63056
9b95ae9ec671 defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents: 61655
diff changeset
   227
9b95ae9ec671 defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents: 61655
diff changeset
   228
val close_term = fold_rev Term.dependent_lambda_name;
63063
wenzelm
parents: 63056
diff changeset
   229
wenzelm
parents: 63056
diff changeset
   230
fun close_prop xs As B =
wenzelm
parents: 63056
diff changeset
   231
  fold_rev dependent_all_name xs (list_implies (As, B));
wenzelm
parents: 63056
diff changeset
   232
wenzelm
parents: 63056
diff changeset
   233
fun close_prop_constraint default_type xs As B =
wenzelm
parents: 63056
diff changeset
   234
  fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B));
63056
9b95ae9ec671 defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents: 61655
diff changeset
   235
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   236
12137
6123958975b8 added mk_conjunction;
wenzelm
parents: 10816
diff changeset
   237
(** conjunction **)
6123958975b8 added mk_conjunction;
wenzelm
parents: 10816
diff changeset
   238
46217
7b19666f0e3d renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents: 46215
diff changeset
   239
val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 25939
diff changeset
   240
val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
19125
59b26248547b simplified Pure conjunction, based on actual const;
wenzelm
parents: 19103
diff changeset
   241
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   242
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   243
(*A &&& B*)
19125
59b26248547b simplified Pure conjunction, based on actual const;
wenzelm
parents: 19103
diff changeset
   244
fun mk_conjunction (A, B) = conjunction $ A $ B;
12137
6123958975b8 added mk_conjunction;
wenzelm
parents: 10816
diff changeset
   245
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   246
(*A &&& B &&& C -- improper*)
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   247
fun mk_conjunction_list [] = true_prop
12757
b76a4376cfcb added mk_conjunction_list;
wenzelm
parents: 12137
diff changeset
   248
  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
12137
6123958975b8 added mk_conjunction;
wenzelm
parents: 10816
diff changeset
   249
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   250
(*(A &&& B) &&& (C &&& D) -- balanced*)
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   251
fun mk_conjunction_balanced [] = true_prop
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 32026
diff changeset
   252
  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   253
18499
567370efb6d7 added mk_conjunction_list2;
wenzelm
parents: 18469
diff changeset
   254
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   255
(*A &&& B*)
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 25939
diff changeset
   256
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
18469
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   257
  | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   258
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   259
(*A &&& B &&& C -- improper*)
19425
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
   260
fun dest_conjunction_list t =
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
   261
  (case try dest_conjunction t of
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
   262
    NONE => [t]
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
   263
  | SOME (A, B) => A :: dest_conjunction_list B);
e0d7d9373faf added dest_conjunction_list;
wenzelm
parents: 19406
diff changeset
   264
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   265
(*(A &&& B) &&& (C &&& D) -- balanced*)
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   266
fun dest_conjunction_balanced 0 _ = []
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 32026
diff changeset
   267
  | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 23357
diff changeset
   268
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28448
diff changeset
   269
(*((A &&& B) &&& C) &&& D &&& E -- flat*)
18469
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   270
fun dest_conjunctions t =
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   271
  (case try dest_conjunction t of
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   272
    NONE => [t]
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   273
  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   274
324245a561b5 mk_conjunction: proper treatment of bounds;
wenzelm
parents: 18248
diff changeset
   275
12137
6123958975b8 added mk_conjunction;
wenzelm
parents: 10816
diff changeset
   276
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   277
(** types as terms **)
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   278
56243
2e10a36b8d46 more qualified names;
wenzelm
parents: 49865
diff changeset
   279
fun mk_type ty = Const ("Pure.type", Term.itselfT ty);
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   280
56243
2e10a36b8d46 more qualified names;
wenzelm
parents: 49865
diff changeset
   281
fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   282
  | dest_type t = raise TERM ("dest_type", [t]);
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   283
21520
63c73f461eec added type_map;
wenzelm
parents: 21016
diff changeset
   284
fun type_map f = dest_type o f o mk_type;
63c73f461eec added type_map;
wenzelm
parents: 21016
diff changeset
   285
4822
2733e21814fe added mk_cond_defpair, mk_defpair;
wenzelm
parents: 4693
diff changeset
   286
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   287
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   288
(** type classes **)
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   289
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   290
(* const names *)
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   291
76785
9e5a27486ca2 tuned signature;
wenzelm
parents: 74525
diff changeset
   292
val class_suffix = "_class";
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   293
76785
9e5a27486ca2 tuned signature;
wenzelm
parents: 74525
diff changeset
   294
val const_of_class = suffix class_suffix;
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   295
76785
9e5a27486ca2 tuned signature;
wenzelm
parents: 74525
diff changeset
   296
fun class_of_const c = unsuffix class_suffix c
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   297
  handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   298
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   299
35854
d452abc96459 Logic.mk_of_sort convenience;
wenzelm
parents: 35845
diff changeset
   300
(* class/sort membership *)
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   301
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   302
fun mk_of_class (ty, c) =
19391
4812d28c90a6 Term.itselfT;
wenzelm
parents: 19125
diff changeset
   303
  Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   304
32784
1a5dde5079ac eliminated redundant bindings;
wenzelm
parents: 32765
diff changeset
   305
fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   306
  | dest_of_class t = raise TERM ("dest_of_class", [t]);
398
41f279b477e2 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents: 210
diff changeset
   307
35854
d452abc96459 Logic.mk_of_sort convenience;
wenzelm
parents: 35845
diff changeset
   308
fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
d452abc96459 Logic.mk_of_sort convenience;
wenzelm
parents: 35845
diff changeset
   309
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   311
(* class relations *)
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   312
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   313
fun name_classrel (c1, c2) =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   314
  Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   315
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   316
fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   317
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   318
fun dest_classrel tm =
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   319
  (case dest_of_class tm of
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   320
    (TVar (_, [c1]), c2) => (c1, c2)
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   321
  | _ => raise TERM ("dest_classrel", [tm]));
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   322
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   323
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   324
(* type arities *)
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   325
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   326
fun name_arities (t, _, S) =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   327
  let val b = Long_Name.base_name t
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   328
  in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
20630
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   329
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   330
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
2010cbb1a941 added name_classrel/arities/arity;
wenzelm
parents: 20548
diff changeset
   331
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   332
fun mk_arities (t, Ss, S) =
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 37230
diff changeset
   333
  let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   334
  in map (fn c => mk_of_class (T, c)) S end;
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   335
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69023
diff changeset
   336
fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69023
diff changeset
   337
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   338
fun dest_arity tm =
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   339
  let
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   340
    fun err () = raise TERM ("dest_arity", [tm]);
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   341
31943
5e960a0780a2 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents: 30554
diff changeset
   342
    val (ty, c) = dest_of_class tm;
19406
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   343
    val (t, tvars) =
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   344
      (case ty of
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   345
        Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   346
      | _ => err ());
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   347
    val Ss =
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   348
      if has_duplicates (eq_fst (op =)) tvars then err ()
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   349
      else map snd tvars;
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   350
  in (t, Ss, c) end;
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   351
410b9d9bf9a1 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents: 19391
diff changeset
   352
79404
cb19148c0b95 tuned comments;
wenzelm
parents: 79399
diff changeset
   353
(* sort constraints within the logic *)
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   354
70811
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
   355
fun dummy_tfree S = TFree ("'dummy", S);
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
   356
79397
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   357
fun present_sorts shyps present_set =
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   358
  let
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   359
    val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   360
    val extra = fold (Sorts.remove_sort o #2) present shyps;
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   361
  in {present = present, extra = extra} end;
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   362
70436
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   363
type unconstrain_context =
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   364
 {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
70436
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   365
  constraints: ((typ * class) * term) list,
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   366
  outer_constraints: (typ * class) list};
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   367
36768
46be86127972 just one version of Thm.unconstrainT, which affects all variables;
wenzelm
parents: 36767
diff changeset
   368
fun unconstrainT shyps prop =
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   369
  let
79385
wenzelm
parents: 79384
diff changeset
   370
    val present_set = Types.build (prop |> (fold_types o fold_atyps) Types.add_set);
79397
0596c28860f9 clarified signature;
wenzelm
parents: 79393
diff changeset
   371
    val {present, extra} = present_sorts shyps present_set;
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   372
79385
wenzelm
parents: 79384
diff changeset
   373
    val n = Types.size present_set;
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 37230
diff changeset
   374
    val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   375
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   376
    val present_map =
79385
wenzelm
parents: 79384
diff changeset
   377
      map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
70438
99024c9c83f6 proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
wenzelm
parents: 70437
diff changeset
   378
    val constraints_map =
79393
wenzelm
parents: 79391
diff changeset
   379
      map (fn (_, V) => (Type.sort_of_atyp V, V)) present_map @
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   380
      map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   381
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   382
    fun unconstrain_atyp {strip_sorts} T =
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   383
      (case AList.lookup (op =) present_map T of
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   384
        SOME U => U |> strip_sorts ? Type.strip_sorts
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   385
      | NONE =>
70438
99024c9c83f6 proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
wenzelm
parents: 70437
diff changeset
   386
          (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   387
            SOME U => U |> strip_sorts ? Type.strip_sorts
70811
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
   388
          | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
785a2112f861 clarified signature -- some operations to support fully explicit proof terms;
wenzelm
parents: 70438
diff changeset
   389
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   390
    fun unconstrain_typ strip_sorts =
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   391
      Term_Subst.map_atypsT_same (fn T =>
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   392
        let val T' = unconstrain_atyp strip_sorts T
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   393
        in if T = T' then raise Same.SAME else T' end);
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   394
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   395
    val constraints =
70436
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   396
      constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   397
        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   398
37230
7b548f137276 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents: 36768
diff changeset
   399
    val outer_constraints =
79385
wenzelm
parents: 79384
diff changeset
   400
      maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
37230
7b548f137276 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents: 36768
diff changeset
   401
70437
fdbb0c2e0162 tuned signature;
wenzelm
parents: 70436
diff changeset
   402
    val ucontext =
79391
70c0dbfacf0b clarified signature: prefer Same.operation;
wenzelm
parents: 79385
diff changeset
   403
     {unconstrain_typ = unconstrain_typ,
70436
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   404
      constraints = constraints,
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   405
      outer_constraints = outer_constraints};
251f1fb44ccd clarified signature;
wenzelm
parents: 70435
diff changeset
   406
    val prop' = prop
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   407
      |> Term_Subst.map_types (unconstrain_typ {strip_sorts = true})
70437
fdbb0c2e0162 tuned signature;
wenzelm
parents: 70436
diff changeset
   408
      |> curry list_implies (map #2 constraints);
fdbb0c2e0162 tuned signature;
wenzelm
parents: 70436
diff changeset
   409
  in (ucontext, prop') end;
36767
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   410
d0095729e1f1 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
wenzelm
parents: 35854
diff changeset
   411
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   412
28448
31a59d7d2168 tuned comments;
wenzelm
parents: 27334
diff changeset
   413
(** protected propositions and embedded terms **)
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   414
56244
3298b7a2795a more qualified names;
wenzelm
parents: 56243
diff changeset
   415
val protectC = Const ("Pure.prop", propT --> propT);
18029
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   416
fun protect t = protectC $ t;
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   417
56244
3298b7a2795a more qualified names;
wenzelm
parents: 56243
diff changeset
   418
fun unprotect (Const ("Pure.prop", _) $ t) = t
18029
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   419
  | unprotect t = raise TERM ("unprotect", [t]);
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   420
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   421
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 25939
diff changeset
   422
fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
19775
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
   423
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 25939
diff changeset
   424
fun dest_term (Const ("Pure.term", _) $ t) = t
19775
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
   425
  | dest_term t = raise TERM ("dest_term", [t]);
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
   426
06cb6743adf6 support embedded terms;
wenzelm
parents: 19425
diff changeset
   427
18181
wenzelm
parents: 18029
diff changeset
   428
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
(*** Low-level term operations ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
(*Does t occur in u?  Or is alpha-convertible to u?
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
  The term t must contain no loose bound variables*)
16846
bbebc68a7faf occs no longer infix (structure not open);
wenzelm
parents: 16130
diff changeset
   433
fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
(*Close up a formula over all free variables by quantification*)
74281
7829d6435c60 more scalable operations;
wenzelm
parents: 70821
diff changeset
   436
fun close_form A =
7829d6435c60 more scalable operations;
wenzelm
parents: 70821
diff changeset
   437
  fold_rev (all o Free) (Frees.build (Frees.add_frees A) |> Frees.list_set) A;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   440
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
(*** Specialized operations for resolution... ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   443
(*computes t(Bound(n+k-1),...,Bound(n))  *)
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   444
fun combound (t, n, k) =
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   445
    if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   446
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   447
(* ([xn,...,x1], t)   goes to   \<lambda>x1 ... xn. t *)
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   448
fun rlist_abs ([], body) = body
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   449
  | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   450
32026
9898880061df tuned incr_tvar_same;
wenzelm
parents: 32023
diff changeset
   451
fun incr_tvar_same 0 = Same.same
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   452
  | incr_tvar_same inc = Term_Subst.map_atypsT_same
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   453
      (fn TVar ((a, i), S) => TVar ((a, i + inc), S)
32026
9898880061df tuned incr_tvar_same;
wenzelm
parents: 32023
diff changeset
   454
        | _ => raise Same.SAME);
16879
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   455
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   456
fun incr_tvar inc = Same.commit (incr_tvar_same inc);
32023
2d071ac5032f export incr_tvar_same;
wenzelm
parents: 32020
diff changeset
   457
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
(*For all variables in the term, increment indexnames and lift over the Us
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
    result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   460
fun incr_indexes_operation {fixed, Ts, inc, level} =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   461
  if null fixed andalso null Ts andalso inc = 0 then Same.same
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   462
  else
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   463
    let
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   464
      val n = length Ts;
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   465
      val incrT = incr_tvar_same inc;
16879
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   466
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   467
      fun incr lev (Var ((x, i), T)) =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   468
            combound (Var ((x, i + inc), Ts ---> Same.commit incrT T), lev, n)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   469
        | incr lev (Free (x, T)) =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   470
            if member (op =) fixed x then
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   471
              combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   472
            else Free (x, incrT T)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   473
        | incr lev (Abs (x, T, t)) =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   474
            (Abs (x, incrT T, Same.commit (incr (lev + 1)) t)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   475
              handle Same.SAME => Abs (x, T, incr (lev + 1) t))
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   476
        | incr lev (t $ u) =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   477
            (incr lev t $ Same.commit (incr lev) u
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   478
              handle Same.SAME => t $ incr lev u)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   479
        | incr _ (Const (c, T)) = Const (c, incrT T)
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   480
        | incr _ (Bound _) = raise Same.SAME;
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   481
    in incr level end;
32026
9898880061df tuned incr_tvar_same;
wenzelm
parents: 32023
diff changeset
   482
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   483
fun incr_indexes (Ts, inc) =
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   484
  if null Ts andalso inc = 0 then I
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   485
  else Same.commit (incr_indexes_operation {fixed = [], Ts = Ts, inc = inc, level = 0});
16879
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   486
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
18248
wenzelm
parents: 18181
diff changeset
   488
(* Lifting functions from subgoal and increment:
18029
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   489
    lift_abs operates on terms
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   490
    lift_all operates on propositions *)
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   491
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   492
fun lift_abs inc =
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   493
  let
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   494
    fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   495
      | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   496
      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
18029
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   497
  in lift [] end;
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   498
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   499
fun lift_all inc =
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   500
  let
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   501
    fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   502
      | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
79232
99bc2dd45111 more general Logic.incr_indexes_operation;
wenzelm
parents: 79231
diff changeset
   503
      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
18029
19f1ad18bece renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents: 17120
diff changeset
   504
  in lift [] end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
(*Strips assumptions in goal, yielding list of hypotheses.   *)
21016
430b35c9cd27 Repaired strip_assums_hyp (now also works for goals not
berghofe
parents: 20883
diff changeset
   507
fun strip_assums_hyp B =
430b35c9cd27 Repaired strip_assums_hyp (now also works for goals not
berghofe
parents: 20883
diff changeset
   508
  let
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   509
    fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   510
      | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) =
21016
430b35c9cd27 Repaired strip_assums_hyp (now also works for goals not
berghofe
parents: 20883
diff changeset
   511
          strip (map (incr_boundvars 1) Hs) t
430b35c9cd27 Repaired strip_assums_hyp (now also works for goals not
berghofe
parents: 20883
diff changeset
   512
      | strip Hs B = rev Hs
430b35c9cd27 Repaired strip_assums_hyp (now also works for goals not
berghofe
parents: 20883
diff changeset
   513
  in strip [] B end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
(*Strips assumptions in goal, yielding conclusion.   *)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   516
fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
60705
6cc14cf3acff tuned whitespace;
wenzelm
parents: 60454
diff changeset
   517
  | strip_assums_concl (Const("Pure.all", _) $ Abs (a, T, t)) = strip_assums_concl t
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
  | strip_assums_concl B = B;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
(*Make a list of all the parameters in a subgoal, even if nested*)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   521
fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
60705
6cc14cf3acff tuned whitespace;
wenzelm
parents: 60454
diff changeset
   522
  | strip_params (Const("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_params t
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
  | strip_params B = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   524
23597
ab67175ca8a5 simplified has_meta_prems;
wenzelm
parents: 23418
diff changeset
   525
(*test for nested meta connectives in prems*)
ab67175ca8a5 simplified has_meta_prems;
wenzelm
parents: 23418
diff changeset
   526
val has_meta_prems =
9667
48cefe2daf32 fixed has_meta_prems: strip_assums_hyp;
wenzelm
parents: 9483
diff changeset
   527
  let
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   528
    fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   529
      | is_meta (Const ("Pure.imp", _) $ _ $ _) = true
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   530
      | is_meta (Const ("Pure.all", _) $ _) = true
9667
48cefe2daf32 fixed has_meta_prems: strip_assums_hyp;
wenzelm
parents: 9483
diff changeset
   531
      | is_meta _ = false;
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   532
    fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   533
      | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B
23597
ab67175ca8a5 simplified has_meta_prems;
wenzelm
parents: 23418
diff changeset
   534
      | ex_meta _ = false;
ab67175ca8a5 simplified has_meta_prems;
wenzelm
parents: 23418
diff changeset
   535
  in ex_meta end;
9483
708a8a05497d added has_meta_prems;
wenzelm
parents: 9460
diff changeset
   536
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   537
(*Removes the parameters from a subgoal and renumber bvars in hypotheses,
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   538
    where j is the total number of parameters (precomputed)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
  If n>0 then deletes assumption n. *)
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   540
fun remove_params j n A =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
    if j=0 andalso n<=0 then A  (*nothing left to do...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   542
    else case A of
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   543
        Const("Pure.imp", _) $ H $ B =>
9460
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   544
          if n=1 then                           (remove_params j (n-1) B)
53d7ad5bec39 Logic.goal_const;
wenzelm
parents: 5041
diff changeset
   545
          else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   546
      | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
      | _ => if n>0 then raise TERM("remove_params", [A])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
             else A;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
(*Move all parameters to the front of the subgoal, renaming them apart;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   551
  if n>0 then deletes assumption n. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
fun flatten_params n A =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
    let val params = strip_params A;
25939
ddea202704b4 Removed Logic.auto_rename.
berghofe
parents: 24848
diff changeset
   554
        val vars = ListPair.zip (Name.variant_list [] (map #1 params),
ddea202704b4 Removed Logic.auto_rename.
berghofe
parents: 24848
diff changeset
   555
                                 map #2 params)
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46217
diff changeset
   556
    in list_all (vars, remove_params (length vars) n A) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
(*Makes parameters in a goal have the names supplied by the list cs.*)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   559
fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) =
45328
e5b33eecbf6e tuned signature;
wenzelm
parents: 43329
diff changeset
   560
      implies $ A $ list_rename_params cs B
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   561
  | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) =
45328
e5b33eecbf6e tuned signature;
wenzelm
parents: 43329
diff changeset
   562
      a $ Abs (c, T, list_rename_params cs t)
e5b33eecbf6e tuned signature;
wenzelm
parents: 43329
diff changeset
   563
  | list_rename_params cs B = B;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
32008
fa0cc3c8f73d tuned comment;
wenzelm
parents: 32004
diff changeset
   565
fa0cc3c8f73d tuned comment;
wenzelm
parents: 32004
diff changeset
   566
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   567
(*** Treatment of "assume", "erule", etc. ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
16879
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   569
(*Strips assumptions in goal yielding
15451
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   570
   HS = [Hn,...,H1],   params = [xm,...,x1], and B,
16879
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   571
  where x1...xm are the parameters. This version (21.1.2005) REQUIRES
b81d3f2ee565 incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents: 16862
diff changeset
   572
  the the parameters to be flattened, but it allows erule to work on
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   573
  assumptions of the form \<And>x. phi. Any \<And> after the outermost string
15451
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   574
  will be regarded as belonging to the conclusion, and left untouched.
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   575
  Used ONLY by assum_pairs.
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   576
      Unless nasms<0, it can terminate the recursion early; that allows
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   577
  erule to work on assumptions of the form P\<Longrightarrow>Q.*)
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   578
fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   579
  | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   580
      strip_assums_imp (nasms-1, H::Hs, B)
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   581
  | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   582
32008
fa0cc3c8f73d tuned comment;
wenzelm
parents: 32004
diff changeset
   583
(*Strips OUTER parameters only.*)
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 56244
diff changeset
   584
fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) =
15451
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   585
      strip_assums_all ((a,T)::params, t)
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   586
  | strip_assums_all (params, B) = (params, B);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   587
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
(*Produces disagreement pairs, one for each assumption proof, in order.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   589
  A is the first premise of the lifted rule, and thus has the form
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   590
    H1 \<Longrightarrow> ... Hk \<Longrightarrow> B   and the pairs are (H1,B),...,(Hk,B).
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   591
  nasms is the number of assumptions in the original subgoal, needed when B
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 63063
diff changeset
   592
    has the form B1 \<Longrightarrow> B2: it stops B1 from being taken as an assumption. *)
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   593
fun assum_pairs(nasms,A) =
15451
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   594
  let val (params, A') = strip_assums_all ([],A)
15454
4b339d3907a0 thin_tac now works on P==>Q
paulson
parents: 15451
diff changeset
   595
      val (Hs,B) = strip_assums_imp (nasms,[],A')
18938
b401ee1cda14 added generic dest_def (mostly from theory.ML);
wenzelm
parents: 18762
diff changeset
   596
      fun abspar t = rlist_abs(params, t)
15451
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   597
      val D = abspar B
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   598
      fun pairrev ([], pairs) = pairs
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   599
        | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
c6c8786b9921 fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents: 14137
diff changeset
   600
  in  pairrev (Hs,[])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   601
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   602
30554
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   603
fun assum_problems (nasms, A) =
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   604
  let
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   605
    val (params, A') = strip_assums_all ([], A)
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   606
    val (Hs, B) = strip_assums_imp (nasms, [], A')
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   607
    fun abspar t = rlist_abs (params, t)
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   608
  in (abspar, rev Hs, B) end;
73f8bd5f0af8 substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents: 30364
diff changeset
   609
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   610
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   611
(* global schematic variables *)
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   612
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   613
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   614
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   615
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   616
fun varifyT_global_same ty = ty
32020
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   617
  |> Term_Subst.map_atypsT_same
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   618
    (fn TFree (a, S) => TVar ((a, 0), S)
31981
9c59cbb9c5a2 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents: 31943
diff changeset
   619
      | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   620
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   621
fun unvarifyT_global_same ty = ty
32020
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   622
  |> Term_Subst.map_atypsT_same
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   623
    (fn TVar ((a, 0), S) => TFree (a, S)
31981
9c59cbb9c5a2 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents: 31943
diff changeset
   624
      | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
9c59cbb9c5a2 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents: 31943
diff changeset
   625
      | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   626
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   627
val varifyT_global = Same.commit varifyT_global_same;
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   628
val unvarifyT_global = Same.commit unvarifyT_global_same;
31981
9c59cbb9c5a2 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents: 31943
diff changeset
   629
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   630
fun varify_types_global tm =
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   631
  Term_Subst.map_types varifyT_global_same tm
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   632
    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
   633
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   634
fun unvarify_types_global tm =
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   635
  Term_Subst.map_types unvarifyT_global_same tm
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   636
    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
   637
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   638
fun varify_global tm = tm
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   639
  |> Term_Subst.map_aterms
32020
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   640
    (fn Free (x, T) => Var ((x, 0), T)
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   641
      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   642
      | _ => raise Same.SAME)
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
   643
  |> varify_types_global;
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   644
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 32784
diff changeset
   645
fun unvarify_global tm = tm
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   646
  |> Term_Subst.map_aterms
32020
9abf5d66606e use structure Same;
wenzelm
parents: 32014
diff changeset
   647
    (fn Var ((x, 0), T) => Free (x, T)
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   648
      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   649
      | Free (x, _) => raise TERM (bad_fixed x, [tm])
79399
11b53e039f6f clarified signature: more operations;
wenzelm
parents: 79397
diff changeset
   650
      | _ => raise Same.SAME)
45344
e209da839ff4 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents: 45328
diff changeset
   651
  |> unvarify_types_global;
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19775
diff changeset
   652
13799
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   653
16862
wenzelm
parents: 16846
diff changeset
   654
(* goal states *)
wenzelm
parents: 16846
diff changeset
   655
49865
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46218
diff changeset
   656
fun get_goal st i =
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46218
diff changeset
   657
  nth_prem (i, st) handle TERM _ =>
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46218
diff changeset
   658
    error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^
eeaf1ec7eac2 clarified defer/prefer: more specific errors;
wenzelm
parents: 46218
diff changeset
   659
      string_of_int (count_prems st)  ^ " subgoals)");
13799
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   660
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   661
(*reverses parameters for substitution*)
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   662
fun goal_params st i =
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   663
  let val gi = get_goal st i
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 28856
diff changeset
   664
      val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
13799
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   665
  in (gi, rfrees) end;
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   666
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   667
fun concl_of_goal st i =
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   668
  let val (gi, rfrees) = goal_params st i
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   669
      val B = strip_assums_concl gi
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   670
  in subst_bounds (rfrees, B) end;
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   671
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   672
fun prems_of_goal st i =
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   673
  let val (gi, rfrees) = goal_params st i
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   674
      val As = strip_assums_hyp gi
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   675
  in map (fn A => subst_bounds (rfrees, A)) As end;
77614fe09362 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents: 13659
diff changeset
   676
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   677
end;