Nominal/nominal_dt_rawfuns.ML
author Christian Urban <urbanc@in.tum.de>
Wed, 18 Aug 2010 00:19:15 +0800
changeset 2410 2bbdb9c427b5
parent 2409 83990a42a068
child 2431 331873ebc5cd
permissions -rw-r--r--
improved runtime slightly, by constructing an explicit size measure for the function definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2297
Christian Urban <urbanc@in.tum.de>
parents: 2296
diff changeset
     1
(*  Title:      nominal_dt_rawfuns.ML
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
    Author:     Christian Urban
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
2297
Christian Urban <urbanc@in.tum.de>
parents: 2296
diff changeset
     5
  Definitions of the raw fv and fv_bn functions
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
*)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
signature NOMINAL_DT_RAWFUNS =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
sig
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    10
  (* info of binding functions *)
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    11
  type bn_info = (term * int * (int * term option) list list) list
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    13
  (* binding modes and binding clauses *)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  datatype bmode = Lst | Res | Set
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
  datatype bclause = BC of bmode * (term option * int) list * int list
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
2296
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    17
  val is_atom: Proof.context -> typ -> bool
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    18
  val is_atom_set: Proof.context -> typ -> bool
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    19
  val is_atom_fset: Proof.context -> typ -> bool
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    20
  val is_atom_list: Proof.context -> typ -> bool
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    21
  val mk_atom_set: term -> term
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    22
  val mk_atom_fset: term -> term
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
    23
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  val setify: Proof.context -> term -> term
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
  val listify: Proof.context -> term -> term
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
    27
  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
    28
    thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
    29
 
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
    30
  val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
struct
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
2375
e163fd99de44 minor polishing
Christian Urban <urbanc@in.tum.de>
parents: 2321
diff changeset
    37
(* term              - is constant of the bn-function 
e163fd99de44 minor polishing
Christian Urban <urbanc@in.tum.de>
parents: 2321
diff changeset
    38
   int               - is datatype number over which the bn-function is defined
e163fd99de44 minor polishing
Christian Urban <urbanc@in.tum.de>
parents: 2321
diff changeset
    39
   int * term option - is number of the corresponding argument with possibly
e163fd99de44 minor polishing
Christian Urban <urbanc@in.tum.de>
parents: 2321
diff changeset
    40
                       recursive call with bn-function term 
e163fd99de44 minor polishing
Christian Urban <urbanc@in.tum.de>
parents: 2321
diff changeset
    41
*)  
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    42
type bn_info = (term * int * (int * term option) list list) list
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    43
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
datatype bmode = Lst | Res | Set
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
datatype bclause = BC of bmode * (term option * int) list * int list
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    47
(* testing for concrete atom types *)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
fun is_atom ctxt ty =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
  | is_atom_set _ _ = false;
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  | is_atom_fset _ _ = false;
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  | is_atom_list _ _ = false
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    61
(* functions for producing sets, fsets and lists of general atom type
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    62
   out from concrete atom types *)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
fun mk_atom_set t =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
  val ty = fastype_of t;
2290
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
    66
  val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
  val img_ty = atom_ty --> ty --> @{typ "atom set"};
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
in
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    69
  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    70
end
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
2321
e9b0728061a8 cleaned up the FSet (noise was introduced by error)
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    72
e9b0728061a8 cleaned up the FSet (noise was introduced by error)
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    73
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
e9b0728061a8 cleaned up the FSet (noise was introduced by error)
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    74
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
e9b0728061a8 cleaned up the FSet (noise was introduced by error)
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    75
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
fun mk_atom_fset t =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
  val ty = fastype_of t;
2290
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
    79
  val atom_ty = dest_fsetT ty --> @{typ "atom"};
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    84
end
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
fun mk_atom_list t =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
  val ty = fastype_of t;
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
  val atom_ty = dest_listT ty --> @{typ atom};
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
  val map_ty = atom_ty --> ty --> @{typ "atom list"};
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
in
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    92
  Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
    93
end
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    95
(* functions that coerces singletons, sets and fsets of concrete atoms
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
    96
   into sets of general atoms *)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
fun setify ctxt t =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
  val ty = fastype_of t;
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
  if is_atom ctxt ty
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
    then  HOLogic.mk_set @{typ atom} [mk_atom t]
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
  else if is_atom_set ctxt ty
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
    then mk_atom_set t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
  else if is_atom_fset ctxt ty
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
    then mk_atom_fset t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
  else raise TERM ("setify", [t])
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   110
(* functions that coerces singletons and lists of concrete atoms
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   111
   into lists of general atoms  *)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
fun listify ctxt t =
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
  val ty = fastype_of t;
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
  if is_atom ctxt ty
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
    then HOLogic.mk_list @{typ atom} [mk_atom t]
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
  else if is_atom_list ctxt ty
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
    then mk_atom_set t
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
  else raise TERM ("listify", [t])
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
(* coerces a list into a set *)
2290
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
   124
fun to_set t =
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
   125
  if fastype_of t = @{typ "atom list"}
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
   126
  then @{term "set::atom list => atom set"} $ t
Christian Urban <urbanc@in.tum.de>
parents: 2289
diff changeset
   127
  else t
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   130
(** functions that construct the equations for fv and fv_bn **)
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   131
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   132
fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   133
let
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   134
  fun mk_fv_body fv_map args i = 
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   135
  let
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   136
    val arg = nth args i
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   137
    val ty = fastype_of arg
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   138
  in
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   139
    case AList.lookup (op=) fv_map ty of
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   140
      NONE => mk_supp arg
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   141
    | SOME fv => fv $ arg
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   142
  end  
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   143
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   144
  fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   145
  let
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   146
    val arg = nth args i
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   147
  in
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   148
    case bn_option of
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   149
      NONE => (setify lthy arg, @{term "{}::atom set"})
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   150
    | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   151
  end  
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   152
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   153
  val t1 = map (mk_fv_body fv_map args) bodies
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   154
  val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   155
in 
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   156
  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   157
end
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   158
2293
aecebd5ed424 hving a working fv-definition without the export
Christian Urban <urbanc@in.tum.de>
parents: 2292
diff changeset
   159
(* in case of fv_bn we have to treat the case special, where an
aecebd5ed424 hving a working fv-definition without the export
Christian Urban <urbanc@in.tum.de>
parents: 2292
diff changeset
   160
   "empty" binding clause is given *)
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   161
fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   162
let
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   163
  fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   164
  let
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   165
    val arg = nth args i
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   166
    val ty = fastype_of arg
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   167
  in
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   168
    case AList.lookup (op=) bn_args i of
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   169
      NONE => (case (AList.lookup (op=) fv_map ty) of
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   170
                 NONE => mk_supp arg
2296
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
   171
               | SOME fv => fv $ arg)
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   172
    | SOME (NONE) => @{term "{}::atom set"}
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   173
    | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   174
  end  
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   175
in
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
  case bclause of
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   177
    BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
2293
aecebd5ed424 hving a working fv-definition without the export
Christian Urban <urbanc@in.tum.de>
parents: 2292
diff changeset
   178
  | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   179
end
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
2296
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
   181
fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = 
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   182
let
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   183
  val arg_names = Datatype_Prop.make_tnames arg_tys
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   184
  val args = map Free (arg_names ~~ arg_tys)
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   185
  val fv = the (AList.lookup (op=) fv_map ty)
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   186
  val lhs = fv $ list_comb (constr, args)
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   187
  val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   188
  val rhs = fold_union rhs_trms
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   189
in
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   190
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   191
end
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   192
2296
45a69c9cc4cc alpha works now
Christian Urban <urbanc@in.tum.de>
parents: 2295
diff changeset
   193
fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
  val arg_names = Datatype_Prop.make_tnames arg_tys
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
  val args = map Free (arg_names ~~ arg_tys)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
  val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
  val lhs = fv_bn $ list_comb (constr, args)
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   199
  val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
  val rhs = fold_union rhs_trms
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
in
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   205
fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
let
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
  val nth_constrs_info = nth constrs_info bn_n
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
  val nth_bclausess = nth bclausesss bn_n
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
in
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   210
  map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
end
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   213
fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
let
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   215
  val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   216
  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
  val fv_frees = map Free (fv_names ~~ fv_tys);
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   218
  val fv_map = raw_tys ~~ fv_frees
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   220
  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   221
  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   222
  val fv_bn_names = map (prefix "fv_") bn_names
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   223
  val fv_bn_arg_tys = map (nth raw_tys) bn_tys
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   224
  val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   225
  val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   226
  val fv_bn_map = bns ~~ fv_bn_frees
2292
Christian Urban <urbanc@in.tum.de>
parents: 2290
diff changeset
   227
2407
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   228
  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
49ab06c0ca64 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2388
diff changeset
   229
  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
  
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   231
  val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   232
  val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
2295
8aff3f3ce47f started to work on alpha
Christian Urban <urbanc@in.tum.de>
parents: 2294
diff changeset
   234
  val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
2304
8a98171ba1fc all raw definitions are defined using function
Christian Urban <urbanc@in.tum.de>
parents: 2297
diff changeset
   235
    Function_Common.default_config (pat_completeness_simp constr_thms) lthy
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   236
  
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   237
  val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   238
 
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   239
  val {fs, simps, inducts, ...} = info;
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
  val morphism = ProofContext.export_morphism lthy'' lthy
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
  val fs_exp = map (Morphism.term morphism) fs
2409
83990a42a068 more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 2407
diff changeset
   243
  val simps_exp = map (Morphism.thm morphism) (the simps)
83990a42a068 more tuning of the code
Christian Urban <urbanc@in.tum.de>
parents: 2407
diff changeset
   244
  val inducts_exp = map (Morphism.thm morphism) (the inducts)
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   245
  val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   246
in
2410
2bbdb9c427b5 improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
parents: 2409
diff changeset
   247
  (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   248
end
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   249
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   250
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   251
(** equivarance proofs **)
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   252
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   253
val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   254
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   255
fun subproof_tac const_names simps = 
2388
ebf253d80670 equivariance for size
Christian Urban <urbanc@in.tum.de>
parents: 2385
diff changeset
   256
  SUBPROOF (fn {prems, context, ...} => 
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   257
    HEADGOAL 
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   258
      (simp_tac (HOL_basic_ss addsimps simps)
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   259
       THEN' Nominal_Permeq.eqvt_tac context [] const_names
2388
ebf253d80670 equivariance for size
Christian Urban <urbanc@in.tum.de>
parents: 2385
diff changeset
   260
       THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   261
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   262
fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   263
  HEADGOAL
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   264
    (Object_Logic.full_atomize_tac
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   265
     THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   266
     THEN_ALL_NEW  subproof_tac const_names simps ctxt)
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   267
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   268
fun mk_eqvt_goal pi const arg =
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   269
let
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   270
  val lhs = mk_perm pi (const $ arg)
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   271
  val rhs = const $ (mk_perm pi arg)  
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
in
2305
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   273
  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   274
end
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   275
93ab397f5980 smaller code for raw-eqvt proofs
Christian Urban <urbanc@in.tum.de>
parents: 2304
diff changeset
   276
fun raw_prove_eqvt consts ind_thms simps ctxt =
2308
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   277
  if null consts then []
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   278
  else
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   279
    let 
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   280
      val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   281
      val p = Free (p, @{typ perm})
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   282
      val arg_tys = 
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   283
        consts
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   284
        |> map fastype_of
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   285
        |> map domain_type 
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   286
      val (arg_names, ctxt'') = 
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   287
        Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
2308
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   288
      val args = map Free (arg_names ~~ arg_tys)
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   289
      val goals = map2 (mk_eqvt_goal p) consts args
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   290
      val insts = map (single o SOME) arg_names
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   291
      val const_names = map (fst o dest_Const) consts      
2308
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   292
    in
2311
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   293
      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
4da5c5c29009 work on transitivity proof
Christian Urban <urbanc@in.tum.de>
parents: 2309
diff changeset
   294
        prove_eqvt_tac insts ind_thms const_names simps context)
2308
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   295
      |> ProofContext.export ctxt'' ctxt
387fcbd33820 fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents: 2305
diff changeset
   296
    end
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
end (* structure *)
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299