Nominal/nominal_dt_quot.ML
author Christian Urban <urbanc@in.tum.de>
Thu, 23 Dec 2010 00:46:06 +0000
changeset 2626 d1bdc281be2b
parent 2598 b136721eedb2
child 2628 16ffbc8442ca
permissions -rw-r--r--
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
(*  Title:      nominal_dt_alpha.ML
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
    Author:     Christian Urban
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
    Author:     Cezary Kaliszyk
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
     5
  Performing quotient constructions, lifting theorems and
2626
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
     6
  deriving support properties for the quotient types.
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
*)
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
signature NOMINAL_DT_QUOT =
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
sig
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    11
  val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    14
  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
    Quotient_Info.qconsts_info list * local_theory
2346
4c5881455923 more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2338
diff changeset
    16
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    17
  val define_qperms: typ list -> string list -> (string * sort) list -> 
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    18
    (string * term * mixfix) list -> thm list -> local_theory -> local_theory
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    19
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    20
  val define_qsizes: typ list -> string list -> (string * sort) list -> 
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    21
    (string * term * mixfix) list -> local_theory -> local_theory
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
    22
2434
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
    23
  val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
2475
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    24
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    25
  val prove_supports: Proof.context -> thm list -> term list -> thm list  
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    26
  val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    27
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    28
  val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    29
    local_theory -> local_theory
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    30
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    31
  val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    32
    thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    33
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    34
  val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    35
 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    36
  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
    37
    thm list -> Proof.context -> thm list
2598
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
    38
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
    39
  val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
    40
    thm list -> Proof.context -> thm list  
2626
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
    41
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
    42
  val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
    43
    thm list -> thm list -> thm list -> thm list -> thm list
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
    44
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
end
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
struct
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
2475
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
    50
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
(* defines the quotient types *)
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    52
fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    53
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    54
    val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    55
    val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    56
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    57
    fold_map Quotient_Type.add_quotient_type qty_args2 lthy
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    58
  end 
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
2338
e1764a73c292 slight cleaning
Christian Urban <urbanc@in.tum.de>
parents: 2337
diff changeset
    60
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
(* defines quotient constants *)
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    62
fun define_qconsts qtys consts_specs lthy =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    63
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    64
    val (qconst_infos, lthy') = 
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    65
      fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    66
    val phi = ProofContext.export_morphism lthy' lthy
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    67
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    68
    (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    69
  end
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    72
(* defines the quotient permutations and proves pt-class *)
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    73
fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    74
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    75
    val lthy1 = 
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    76
      lthy
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    77
      |> Local_Theory.exit_global
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    78
      |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2396
diff changeset
    79
  
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    80
    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    81
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    82
    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2396
diff changeset
    83
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    84
    val lifted_perm_laws = 
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    85
      map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    86
      |> Variable.exportT lthy3 lthy2
2398
1e6160690546 improved code
Christian Urban <urbanc@in.tum.de>
parents: 2396
diff changeset
    87
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    88
    fun tac _ =
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    89
      Class.intro_classes_tac [] THEN
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    90
        (ALLGOALS (resolve_tac lifted_perm_laws))
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    91
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    92
    lthy2
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    93
    |> Class.prove_instantiation_exit tac 
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    94
    |> Named_Target.theory_init
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
    95
  end
2346
4c5881455923 more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 2338
diff changeset
    96
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
    98
(* defines the size functions and proves size-class *)
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
    99
fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   100
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   101
    val tac = K (Class.intro_classes_tac [])
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   102
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   103
    lthy
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   104
    |> Local_Theory.exit_global
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   105
    |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   106
    |> snd o (define_qconsts qtys size_specs)
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   107
    |> Class.prove_instantiation_exit tac
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   108
    |> Named_Target.theory_init
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   109
  end
2400
c6d30d5f5ba1 defined qperms and qsizes
Christian Urban <urbanc@in.tum.de>
parents: 2398
diff changeset
   110
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   111
2475
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
parents: 2434
diff changeset
   112
(* lifts a theorem and cleans all "_raw" parts
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   113
   from variable names *)
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   114
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   115
local
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   116
  val any = Scan.one (Symbol.not_eof)
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   117
  val raw = Scan.this_string "_raw"
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   118
  val exclude =
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   119
    Scan.repeat (Scan.unless raw any) --| raw >> implode
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   120
  val parser = Scan.repeat (exclude || any)
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   121
in
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   122
  fun unraw_str s =
2574
50da1be9a7e5 current isabelle
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2476
diff changeset
   123
    s |> raw_explode
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   124
      |> Scan.finite Symbol.stopper parser >> implode 
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   125
      |> fst
2431
331873ebc5cd can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents: 2430
diff changeset
   126
end
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   127
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   128
fun unraw_vars_thm thm =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   129
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   130
    fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   131
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   132
    val vars = Term.add_vars (prop_of thm) []
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   133
    val vars' = map (Var o unraw_var_str) vars
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   134
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   135
    Thm.certify_instantiate ([], (vars ~~ vars')) thm
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   136
  end
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   137
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   138
fun unraw_bounds_thm th =
2476
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   139
  let
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   140
    val trm = Thm.prop_of th
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   141
    val trm' = Term.map_abs_vars unraw_str trm
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   142
  in
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   143
    Thm.rename_boundvars trm trm' th
8f8652a8107f tuned (to conform with indentation policy of Markus)
Christian Urban <urbanc@in.tum.de>
parents: 2475
diff changeset
   144
  end
2426
deb5be0115a7 moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents: 2401
diff changeset
   145
2434
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   146
fun lift_thms qtys simps thms ctxt =
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   147
  (map (Quotient_Tacs.lifted ctxt qtys simps
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   148
        #> unraw_bounds_thm
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   149
        #> unraw_vars_thm
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   150
        #> Drule.zero_var_indexes) thms, ctxt)
92dc6cfa3a95 automatic lifting
Christian Urban <urbanc@in.tum.de>
parents: 2433
diff changeset
   151
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   152
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   153
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   154
fun mk_supports_goal ctxt qtrm =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   155
  let  
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   156
    val vs = fresh_args ctxt qtrm
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   157
    val rhs = list_comb (qtrm, vs)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   158
    val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   159
      |> mk_supp
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   160
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   161
    mk_supports lhs rhs
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   162
    |> HOLogic.mk_Trueprop
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   163
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   164
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   165
fun supports_tac ctxt perm_simps =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   166
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   167
    val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   168
    val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   169
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   170
    EVERY' [ simp_tac ss1,
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   171
             Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   172
             simp_tac ss2 ]
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   173
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   174
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   175
fun prove_supports_single ctxt perm_simps qtrm =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   176
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   177
    val goal = mk_supports_goal ctxt qtrm 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   178
    val ctxt' = Variable.auto_fixes goal ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   179
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   180
    Goal.prove ctxt' [] [] goal
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   181
      (K (HEADGOAL (supports_tac ctxt perm_simps)))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   182
    |> singleton (ProofContext.export ctxt' ctxt)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   183
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   184
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   185
fun prove_supports ctxt perm_simps qtrms =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   186
  map (prove_supports_single ctxt perm_simps) qtrms
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   187
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   188
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   189
(* finite supp lemmas for qtypes *)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   190
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   191
fun prove_fsupp ctxt qtys qinduct qsupports_thms =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   192
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   193
    val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   194
    val goals = vs ~~ qtys
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   195
      |> map Free
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   196
      |> map (mk_finite o mk_supp)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   197
      |> foldr1 (HOLogic.mk_conj)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   198
      |> HOLogic.mk_Trueprop
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   199
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   200
    val tac = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   201
      EVERY' [ rtac @{thm supports_finite},
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   202
               resolve_tac qsupports_thms,
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   203
               asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   204
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   205
    Goal.prove ctxt' [] [] goals
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   206
      (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   207
    |> singleton (ProofContext.export ctxt' ctxt)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   208
    |> Datatype_Aux.split_conj_thm
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   209
    |> map zero_var_indexes
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   210
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   211
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   212
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   213
(* finite supp instances *)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   214
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   215
fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   216
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   217
    val lthy1 = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   218
      lthy
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   219
      |> Local_Theory.exit_global
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   220
      |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   221
  
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   222
    fun tac _ =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   223
      Class.intro_classes_tac [] THEN
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   224
        (ALLGOALS (resolve_tac qfsupp_thms))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   225
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   226
    lthy1
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   227
    |> Class.prove_instantiation_exit tac 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   228
    |> Named_Target.theory_init
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   229
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   230
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   231
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   232
(* proves that fv and fv_bn equals supp *)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   233
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   234
fun gen_mk_goals fv supp =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   235
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   236
    val arg_ty = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   237
      fastype_of fv
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   238
      |> domain_type
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   239
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   240
    (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   241
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   242
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   243
fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   244
fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   245
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   246
fun add_ss thms =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   247
  HOL_basic_ss addsimps thms
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   248
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   249
fun symmetric thms = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   250
  map (fn thm => thm RS @{thm sym}) thms
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   251
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   252
val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   253
val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   254
val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   255
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   256
fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   257
  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   258
  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   259
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   260
fun mk_supp_abs_tac ctxt [] = []
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   261
  | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   262
  | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   263
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   264
fun mk_bn_supp_abs_tac trm =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   265
  trm
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   266
  |> fastype_of
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   267
  |> body_type
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   268
  |> (fn ty => case ty of
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   269
        @{typ "atom set"}  => simp_tac (add_ss supp_Abs_set)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   270
      | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   271
      | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   272
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   273
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   274
val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   275
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   276
val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   277
  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   278
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   279
fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   280
  fv_bn_eqvts qinduct bclausess ctxt =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   281
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   282
    val goals1 = map mk_fvs_goals fvs
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   283
    val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns   
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   284
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   285
    fun tac ctxt =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   286
      SUBGOAL (fn (goal, i) =>
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   287
        let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   288
          val (fv_fun, arg) = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   289
            goal |> Envir.eta_contract
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   290
                 |> Logic.strip_assums_concl
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   291
                 |> HOLogic.dest_Trueprop
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   292
                 |> fst o HOLogic.dest_eq
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   293
                 |> dest_comb
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   294
          val supp_abs_tac = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   295
            case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   296
              SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   297
            | NONE => mk_bn_supp_abs_tac fv_fun
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   298
        in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   299
          EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   300
                   TRY o supp_abs_tac,
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   301
                   TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   302
                   TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   303
                   TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   304
                   TRY o asm_full_simp_tac (add_ss thms3),
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   305
                   TRY o simp_tac (add_ss thms2),
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   306
                   TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   307
        end)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   308
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   309
    induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   310
    |> map atomize
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   311
    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   312
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   313
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   314
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   315
fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   316
  let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   317
    fun mk_goal qbn = 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   318
      let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   319
        val arg_ty = domain_type (fastype_of qbn)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   320
        val finite = @{term "finite :: atom set => bool"}
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   321
      in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   322
        (arg_ty, fn x => finite $ (to_set (qbn $ x)))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   323
      end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   324
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   325
    val props = map mk_goal qbns
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   326
    val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   327
      @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   328
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   329
    induct_prove qtys props qinduct (K ss_tac) ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   330
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   331
2598
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   332
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   333
fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   334
  let 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   335
    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   336
    val p = Free (p, @{typ perm})
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   337
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   338
    fun mk_goal qperm_bn alpha_bn =
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   339
      let
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   340
        val arg_ty = domain_type (fastype_of alpha_bn)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   341
      in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   342
        (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   343
      end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   344
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   345
    val props = map2 mk_goal qperm_bns alpha_bns
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   346
    val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   347
    val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   348
  in
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   349
    induct_prove qtys props qinduct (K ss_tac) ctxt'
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   350
    |> ProofContext.export ctxt' ctxt
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   351
    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   352
  end
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   353
2598
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   354
fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   355
  let 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   356
    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   357
    val p = Free (p, @{typ perm})
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   358
2598
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   359
    fun mk_goal qbn qperm_bn =
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   360
      let
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   361
        val arg_ty = domain_type (fastype_of qbn)
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   362
      in
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   363
        (arg_ty, fn x => 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   364
          (mk_id (Abs ("", arg_ty, 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   365
             HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   366
      end
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   367
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   368
    val props = map2 mk_goal qbns qperm_bns
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   369
    val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   370
    val ss_tac = 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   371
      EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   372
              TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   373
              TRY o asm_full_simp_tac HOL_basic_ss]
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   374
  in
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   375
    induct_prove qtys props qinduct (K ss_tac) ctxt'
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   376
    |> ProofContext.export ctxt' ctxt 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   377
    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
b136721eedb2 automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents: 2595
diff changeset
   378
  end
2595
07f775729e90 moved code from nominal_dt_supp to nominal_dt_quot
Christian Urban <urbanc@in.tum.de>
parents: 2574
diff changeset
   379
2626
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   380
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   381
(** proves strong exhauts theorems **)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   382
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   383
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   384
(* fixme: move into nominal_library *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   385
fun abs_const bmode ty =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   386
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   387
    val (const_name, binder_ty, abs_ty) = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   388
      case bmode of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   389
        Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   390
      | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   391
      | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   392
  in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   393
    Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   394
  end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   395
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   396
fun mk_abs bmode trm1 trm2 =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   397
  abs_const bmode (fastype_of trm2) $ trm1 $ trm2  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   398
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   399
fun is_abs_eq thm =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   400
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   401
    fun is_abs trm =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   402
      case (head_of trm) of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   403
        Const (@{const_name "Abs_set"}, _) => true
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   404
      | Const (@{const_name "Abs_lst"}, _) => true
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   405
      | Const (@{const_name "Abs_res"}, _) => true
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   406
      | _ => false
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   407
  in 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   408
    thm |> prop_of 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   409
        |> HOLogic.dest_Trueprop
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   410
        |> HOLogic.dest_eq
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   411
        |> fst
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   412
        |> is_abs
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   413
  end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   414
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   415
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   416
(* adds a freshness condition to the assumptions *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   417
fun mk_ecase_prems lthy c (params, prems, concl) bclauses =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   418
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   419
    val tys = map snd params
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   420
    val binders = get_all_binders bclauses
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   421
   
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   422
    fun prep_binder (opt, i) = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   423
      let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   424
        val t = Bound (length tys - i - 1)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   425
      in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   426
        case opt of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   427
          NONE => setify_ty lthy (nth tys i) t 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   428
        | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   429
      end 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   430
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   431
    val prems' = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   432
      case binders of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   433
        [] => prems                        (* case: no binders *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   434
      | _ => binders                       (* case: binders *) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   435
          |> map prep_binder
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   436
          |> fold_union_env tys
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   437
          |> (fn t => mk_fresh_star t c)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   438
          |> (fn t => HOLogic.mk_Trueprop t :: prems)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   439
  in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   440
    mk_full_horn params prems' concl
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   441
  end  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   442
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   443
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   444
(* derives the freshness theorem that there exists a p, such that 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   445
   (p o as) #* (c, t1,..., tn) *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   446
fun fresh_thm ctxt c parms binders bn_finite_thms =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   447
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   448
    fun prep_binder (opt, i) = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   449
      case opt of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   450
        NONE => setify ctxt (nth parms i) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   451
      | SOME bn => to_set (bn $ (nth parms i))  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   452
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   453
    fun prep_binder2 (opt, i) = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   454
      case opt of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   455
        NONE => atomify ctxt (nth parms i)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   456
      | SOME bn => bn $ (nth parms i) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   457
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   458
    val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   459
    val lhs = binders
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   460
      |> map prep_binder
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   461
      |> fold_union
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   462
      |> mk_perm (Bound 0)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   463
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   464
    val goal = mk_fresh_star lhs rhs
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   465
      |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   466
      |> HOLogic.mk_Trueprop   
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   467
 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   468
    val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   469
      @ @{thms finite.intros finite_Un finite_set finite_fset}  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   470
  in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   471
    Goal.prove ctxt [] [] goal
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   472
      (K (HEADGOAL (rtac @{thm at_set_avoiding1}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   473
          THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   474
  end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   475
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   476
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   477
(* derives an abs_eq theorem of the form 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   478
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   479
   Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   480
   Exists q. [as].x = [q o as].(q o x)  for recursive binders
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   481
*)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   482
fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   483
  (bclause as (BC (bmode, binders, bodies))) =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   484
  case binders of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   485
    [] => [] 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   486
  | _ =>
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   487
      let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   488
        val rec_flag = is_recursive_binder bclause
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   489
        val binder_trm = comb_binders ctxt bmode parms binders
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   490
        val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   491
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   492
        val abs_lhs = mk_abs bmode binder_trm body_trm
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   493
        val abs_rhs = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   494
          if rec_flag
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   495
          then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   496
          else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   497
        
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   498
        val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   499
        val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   500
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   501
        val goal = HOLogic.mk_conj (abs_eq, peq)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   502
          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   503
          |> HOLogic.mk_Trueprop  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   504
 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   505
        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   506
          @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   507
          fresh_star_set} @ @{thms finite.intros finite_fset}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   508
  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   509
        val tac1 = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   510
          if rec_flag
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   511
          then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   512
          else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   513
        
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   514
        val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   515
     in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   516
       [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   517
         |> (if rec_flag
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   518
             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   519
             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   520
     end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   521
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   522
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   523
val setify = @{lemma "xs = ys ==> set xs = set ys" by simp}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   524
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   525
fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   526
  prems bclausess qexhaust_thm =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   527
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   528
    fun aux_tac prem bclauses =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   529
      case (get_all_binders bclauses) of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   530
        [] => EVERY' [rtac prem, atac]
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   531
      | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   532
          let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   533
            val parms = map (term_of o snd) params
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   534
            val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   535
  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   536
            val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   537
            val (([(_, fperm)], fprops), ctxt') = Obtain.result
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   538
              (K (EVERY1 [etac exE, 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   539
                          full_simp_tac (HOL_basic_ss addsimps ss), 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   540
                          REPEAT o (etac @{thm conjE})])) [fthm] ctxt 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   541
  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   542
            val abs_eq_thms = flat 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   543
             (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   544
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   545
            val ((_, eqs), ctxt'') = Obtain.result
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   546
              (K (EVERY1 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   547
                   [ REPEAT o (etac @{thm exE}), 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   548
                     REPEAT o (etac @{thm conjE}),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   549
                     REPEAT o (dtac setify),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   550
                     full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   551
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   552
            val (abs_eqs, peqs) = split_filter is_abs_eq eqs
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   553
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   554
            val fprops' = 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   555
              map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   556
              @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   557
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   558
            (* for freshness conditions *) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   559
            val tac1 = SOLVED' (EVERY'
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   560
              [ simp_tac (HOL_basic_ss addsimps peqs),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   561
                rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   562
                conj_tac (DETERM o resolve_tac fprops') ]) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   563
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   564
            (* for equalities between constructors *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   565
            val tac2 = SOLVED' (EVERY' 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   566
              [ rtac (@{thm ssubst} OF prems),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   567
                rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   568
                rewrite_goal_tac (map safe_mk_equiv abs_eqs),
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   569
                conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   570
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   571
            (* proves goal "P" *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   572
            val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   573
              (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   574
              |> singleton (ProofContext.export ctxt'' ctxt)  
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   575
          in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   576
            rtac side_thm 1 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   577
          end) ctxt
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   578
  in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   579
    EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   580
  end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   581
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   582
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   583
fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   584
  perm_bn_alphas =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   585
  let
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   586
    val ((_, exhausts'), lthy') = Variable.import true exhausts lthy 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   587
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   588
    val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   589
    val c = Free (c, TFree (a, @{sort fs}))
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   590
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   591
    val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   592
      |> map prop_of
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   593
      |> map Logic.strip_horn
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   594
      |> split_list
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   595
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   596
    val ecases' = (map o map) strip_full_horn ecases
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   597
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   598
    val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   599
   
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   600
    fun tac bclausess exhaust {prems, context} =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   601
      case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   602
        prems bclausess exhaust
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   603
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   604
    fun prove prems bclausess exhaust concl =
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   605
      Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   606
  in
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   607
    map4 prove premss bclausesss exhausts' main_concls
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   608
    |> ProofContext.export lthy'' lthy
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   609
  end
d1bdc281be2b moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2598
diff changeset
   610
2337
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   611
end (* structure *)
b151399bd2c3 fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   612