src/HOL/HOLCF/Tools/Domain/domain_induction.ML
author paulson
Thu, 16 Dec 2010 20:14:04 +0000
changeset 41214 8a341cf54a85
parent 40832 4352ca878c41
child 41296 6aaf80ea9715
permissions -rw-r--r--
made sml/nj happy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40040
3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents: 40029
diff changeset
     1
(*  Title:      HOLCF/Tools/Domain/domain_induction.ML
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    Author:     David von Oheimb
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32172
diff changeset
     3
    Author:     Brian Huffman
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
40040
3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents: 40029
diff changeset
     5
Proofs of high-level (co)induction rules for domain command.
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
40040
3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents: 40029
diff changeset
     8
signature DOMAIN_INDUCTION =
31005
e55eed7d9b55 add module signature for domain_theorems.ML
huffman
parents: 31004
diff changeset
     9
sig
35657
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
    10
  val comp_theorems :
40097
429cd74f795f remove legacy comp_dbind option from domain package
huffman
parents: 40040
diff changeset
    11
      binding list ->
35657
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
    12
      Domain_Take_Proofs.take_induct_info ->
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    13
      Domain_Constructors.constr_info list ->
35657
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
    14
      theory -> thm list * theory
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
    15
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    16
  val quiet_mode: bool Unsynchronized.ref
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    17
  val trace_domain: bool Unsynchronized.ref
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    18
end
31005
e55eed7d9b55 add module signature for domain_theorems.ML
huffman
parents: 31004
diff changeset
    19
40040
3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents: 40029
diff changeset
    20
structure Domain_Induction :> DOMAIN_INDUCTION =
31005
e55eed7d9b55 add module signature for domain_theorems.ML
huffman
parents: 31004
diff changeset
    21
struct
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    23
val quiet_mode = Unsynchronized.ref false
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    24
val trace_domain = Unsynchronized.ref false
29402
9610f3870d64 add tracing for domain package proofs
huffman
parents: 29064
diff changeset
    25
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    26
fun message s = if !quiet_mode then () else writeln s
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    27
fun trace s = if !trace_domain then tracing s else ()
29402
9610f3870d64 add tracing for domain package proofs
huffman
parents: 29064
diff changeset
    28
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    29
open HOLCF_Library
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
40013
9db8fb58fddc add function take_theorems
huffman
parents: 39557
diff changeset
    31
(******************************************************************************)
9db8fb58fddc add function take_theorems
huffman
parents: 39557
diff changeset
    32
(***************************** proofs about take ******************************)
9db8fb58fddc add function take_theorems
huffman
parents: 39557
diff changeset
    33
(******************************************************************************)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
40013
9db8fb58fddc add function take_theorems
huffman
parents: 39557
diff changeset
    35
fun take_theorems
40019
05cda34d36e7 put constructor argument specs in constr_info type
huffman
parents: 40018
diff changeset
    36
    (dbinds : binding list)
35775
9b7e2e17be69 pass take_info as argument to Domain_Theorems.theorems
huffman
parents: 35774
diff changeset
    37
    (take_info : Domain_Take_Proofs.take_induct_info)
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    38
    (constr_infos : Domain_Constructors.constr_info list)
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    39
    (thy : theory) : thm list list * theory =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    41
  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    42
  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    44
  val n = Free ("n", @{typ nat})
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    45
  val n' = @{const Suc} $ n
35559
119653afcd6e remove copy_of_dtyp from domain_axioms.ML
huffman
parents: 35558
diff changeset
    46
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    47
  local
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    48
    val newTs = map (#absT o #iso_info) constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    49
    val subs = newTs ~~ map (fn t => t $ n) take_consts
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    50
    fun is_ID (Const (c, _)) = (c = @{const_name ID})
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    51
      | is_ID _              = false
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    52
  in
40488
c67253b83dc8 avoid using stale theory
huffman
parents: 40327
diff changeset
    53
    fun map_of_arg thy v T =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    54
      let val m = Domain_Take_Proofs.map_of_typ thy subs T
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    55
      in if is_ID m then v else mk_capply (m, v) end
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    56
  end
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    57
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    58
  fun prove_take_apps
40019
05cda34d36e7 put constructor argument specs in constr_info type
huffman
parents: 40018
diff changeset
    59
      ((dbind, take_const), constr_info) thy =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
    let
41214
8a341cf54a85 made sml/nj happy
paulson
parents: 40832
diff changeset
    61
      val {iso_info, con_specs, con_betas, ...} : Domain_Constructors.constr_info = constr_info
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    62
      val {abs_inverse, ...} = iso_info
40019
05cda34d36e7 put constructor argument specs in constr_info type
huffman
parents: 40018
diff changeset
    63
      fun prove_take_app (con_const, args) =
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    64
        let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    65
          val Ts = map snd args
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    66
          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    67
          val vs = map Free (ns ~~ Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    68
          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    69
          val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    70
          val goal = mk_trp (mk_eq (lhs, rhs))
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    71
          val rules =
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    72
              [abs_inverse] @ con_betas @ @{thms take_con_rules}
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    73
              @ take_Suc_thms @ deflation_thms @ deflation_take_thms
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    74
          val tac = simp_tac (HOL_basic_ss addsimps rules) 1
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    75
        in
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    76
          Goal.prove_global thy [] [] goal (K tac)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    77
        end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    78
      val take_apps = map prove_take_app con_specs
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    79
    in
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    80
      yield_singleton Global_Theory.add_thmss
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    81
        ((Binding.qualified true "take_rews" dbind, take_apps),
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    82
        [Simplifier.simp_add]) thy
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    83
    end
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
in
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
    85
  fold_map prove_take_apps
40019
05cda34d36e7 put constructor argument specs in constr_info type
huffman
parents: 40018
diff changeset
    86
    (dbinds ~~ take_consts ~~ constr_infos) thy
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    87
end
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
40029
57e7f651fc70 remove dead code
huffman
parents: 40026
diff changeset
    89
(******************************************************************************)
57e7f651fc70 remove dead code
huffman
parents: 40026
diff changeset
    90
(****************************** induction rules *******************************)
57e7f651fc70 remove dead code
huffman
parents: 40026
diff changeset
    91
(******************************************************************************)
40013
9db8fb58fddc add function take_theorems
huffman
parents: 39557
diff changeset
    92
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
    93
val case_UU_allI =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    94
    @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
    95
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
    96
fun prove_induction
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
    97
    (comp_dbind : binding)
40018
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
    98
    (constr_infos : Domain_Constructors.constr_info list)
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
    99
    (take_info : Domain_Take_Proofs.take_induct_info)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   100
    (take_rews : thm list)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   101
    (thy : theory) =
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   102
let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   103
  val comp_dname = Binding.name_of comp_dbind
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   104
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   105
  val iso_infos = map #iso_info constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   106
  val exhausts = map #exhaust constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   107
  val con_rews = maps #con_rews constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   108
  val {take_consts, take_induct_thms, ...} = take_info
35658
3d8da9fac424 pass take_info as an argument to comp_theorems
huffman
parents: 35657
diff changeset
   109
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   110
  val newTs = map #absT iso_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   111
  val P_names = Datatype_Prop.indexify_names (map (K "P") newTs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   112
  val x_names = Datatype_Prop.indexify_names (map (K "x") newTs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   113
  val P_types = map (fn T => T --> HOLogic.boolT) newTs
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   114
  val Ps = map Free (P_names ~~ P_types)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   115
  val xs = map Free (x_names ~~ newTs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   116
  val n = Free ("n", HOLogic.natT)
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   117
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   118
  fun con_assm defined p (con, args) =
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   119
    let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   120
      val Ts = map snd args
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   121
      val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   122
      val vs = map Free (ns ~~ Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   123
      val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   124
      fun ind_hyp (v, T) t =
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   125
          case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   126
          | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   127
      val t1 = mk_trp (p $ list_ccomb (con, vs))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   128
      val t2 = fold_rev ind_hyp (vs ~~ Ts) t1
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   129
      val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   130
    in fold_rev Logic.all vs (if defined then t3 else t2) end
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   131
  fun eq_assms ((p, T), cons) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   132
      mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   133
  val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   134
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   135
  val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   136
  fun quant_tac ctxt i = EVERY
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   137
    (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   138
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   139
  (* FIXME: move this message to domain_take_proofs.ML *)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   140
  val is_finite = #is_finite take_info
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   141
  val _ = if is_finite
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   142
          then message ("Proving finiteness rule for domain "^comp_dname^" ...")
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   143
          else ()
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   144
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   145
  val _ = trace " Proving finite_ind..."
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   146
  val finite_ind =
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   147
    let
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   148
      val concls =
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   149
          map (fn ((P, t), x) => P $ mk_capply (t $ n, x))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   150
              (Ps ~~ take_consts ~~ xs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   151
      val goal = mk_trp (foldr1 mk_conj concls)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   152
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   153
      fun tacf {prems, context} =
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   154
        let
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   155
          (* Prove stronger prems, without definedness side conditions *)
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   156
          fun con_thm p (con, args) =
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   157
            let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   158
              val subgoal = con_assm false p (con, args)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   159
              val rules = prems @ con_rews @ simp_thms
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   160
              val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   161
              fun arg_tac (lazy, _) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   162
                  rtac (if lazy then allI else case_UU_allI) 1
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   163
              val tacs =
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   164
                  rewrite_goals_tac @{thms atomize_all atomize_imp} ::
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   165
                  map arg_tac args @
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   166
                  [REPEAT (rtac impI 1), ALLGOALS simplify]
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   167
            in
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   168
              Goal.prove context [] [] subgoal (K (EVERY tacs))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   169
            end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   170
          fun eq_thms (p, cons) = map (con_thm p) cons
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   171
          val conss = map #con_specs constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   172
          val prems' = maps eq_thms (Ps ~~ conss)
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   173
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   174
          val tacs1 = [
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   175
            quant_tac context 1,
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   176
            simp_tac HOL_ss 1,
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   177
            InductTacs.induct_tac context [[SOME "n"]] 1,
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   178
            simp_tac (take_ss addsimps prems) 1,
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   179
            TRY (safe_tac HOL_cs)]
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   180
          fun con_tac _ = 
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   181
            asm_simp_tac take_ss 1 THEN
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   182
            (resolve_tac prems' THEN_ALL_NEW etac spec) 1
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35777
diff changeset
   183
          fun cases_tacs (cons, exhaust) =
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35777
diff changeset
   184
            res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   185
            asm_simp_tac (take_ss addsimps prems) 1 ::
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   186
            map con_tac cons
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   187
          val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   188
        in
40020
0cbb08bf18df rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents: 40019
diff changeset
   189
          EVERY (map DETERM tacs)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   190
        end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   191
    in Goal.prove_global thy [] assms goal tacf end
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   192
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   193
  val _ = trace " Proving ind..."
35661
ede27eb8e94b don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
huffman
parents: 35660
diff changeset
   194
  val ind =
40022
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   195
    let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   196
      val concls = map (op $) (Ps ~~ xs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   197
      val goal = mk_trp (foldr1 mk_conj concls)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   198
      val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
40022
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   199
      fun tacf {prems, context} =
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   200
        let
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   201
          fun finite_tac (take_induct, fin_ind) =
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   202
              rtac take_induct 1 THEN
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   203
              (if is_finite then all_tac else resolve_tac prems 1) THEN
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   204
              (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   205
          val fin_inds = Project_Rule.projections context finite_ind
40022
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   206
        in
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   207
          TRY (safe_tac HOL_cs) THEN
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   208
          EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   209
        end
40022
3a4a24b714f3 simplify automation of induct proof
huffman
parents: 40020
diff changeset
   210
    in Goal.prove_global thy [] (adms @ assms) goal tacf end
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   211
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   212
  (* case names for induction rules *)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   213
  val dnames = map (fst o dest_Type) newTs
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   214
  val case_ns =
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   215
    let
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   216
      val adms =
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   217
          if is_finite then [] else
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   218
          if length dnames = 1 then ["adm"] else
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   219
          map (fn s => "adm_" ^ Long_Name.base_name s) dnames
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   220
      val bottoms =
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   221
          if length dnames = 1 then ["bottom"] else
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   222
          map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
41214
8a341cf54a85 made sml/nj happy
paulson
parents: 40832
diff changeset
   223
      fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   224
        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   225
        in bot :: map name_of (#con_specs constr_info) end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   226
    in adms @ flat (map2 one_eq bottoms constr_infos) end
35630
8e562d56d404 add case_names attribute to casedist and ind rules
huffman
parents: 35601
diff changeset
   227
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   228
  val inducts = Project_Rule.projections (ProofContext.init_global thy) ind
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   229
  fun ind_rule (dname, rule) =
40026
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   230
      ((Binding.empty, rule),
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   231
       [Rule_Cases.case_names case_ns, Induct.induct_type dname])
35630
8e562d56d404 add case_names attribute to casedist and ind rules
huffman
parents: 35601
diff changeset
   232
35774
218e9766a848 replace some string arguments with bindings
huffman
parents: 35663
diff changeset
   233
in
218e9766a848 replace some string arguments with bindings
huffman
parents: 35663
diff changeset
   234
  thy
40026
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   235
  |> snd o Global_Theory.add_thms [
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   236
     ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []),
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   237
     ((Binding.qualified true "induct"        comp_dbind, ind       ), [])]
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   238
  |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts)))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   239
end (* prove_induction *)
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   240
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   241
(******************************************************************************)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   242
(************************ bisimulation and coinduction ************************)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   243
(******************************************************************************)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   244
35574
ee5df989b7c4 move coinduction-related stuff into function prove_coindunction
huffman
parents: 35560
diff changeset
   245
fun prove_coinduction
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   246
    (comp_dbind : binding, dbinds : binding list)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   247
    (constr_infos : Domain_Constructors.constr_info list)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   248
    (take_info : Domain_Take_Proofs.take_induct_info)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   249
    (take_rews : thm list list)
35599
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   250
    (thy : theory) : theory =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   251
let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   252
  val iso_infos = map #iso_info constr_infos
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   253
  val newTs = map #absT iso_infos
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   254
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   255
  val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   256
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   257
  val R_names = Datatype_Prop.indexify_names (map (K "R") newTs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   258
  val R_types = map (fn T => T --> T --> boolT) newTs
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   259
  val Rs = map Free (R_names ~~ R_types)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   260
  val n = Free ("n", natT)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   261
  val reserved = "x" :: "y" :: R_names
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   262
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   263
  (* declare bisimulation predicate *)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   264
  val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   265
  val bisim_type = R_types ---> boolT
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   266
  val (bisim_const, thy) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   267
      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   268
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   269
  (* define bisimulation predicate *)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   270
  local
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   271
    fun one_con T (con, args) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   272
      let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   273
        val Ts = map snd args
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   274
        val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   275
        val ns2 = map (fn n => n^"'") ns1
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   276
        val vs1 = map Free (ns1 ~~ Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   277
        val vs2 = map Free (ns2 ~~ Ts)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   278
        val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   279
        val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2))
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   280
        fun rel ((v1, v2), T) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   281
            case AList.lookup (op =) (newTs ~~ Rs) T of
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   282
              NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   283
        val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2])
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   284
      in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   285
        Library.foldr mk_ex (vs1 @ vs2, eqs)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   286
      end
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   287
    fun one_eq ((T, R), cons) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   288
      let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   289
        val x = Free ("x", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   290
        val y = Free ("y", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   291
        val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   292
        val disjs = disj1 :: map (one_con T) cons
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   293
      in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   294
        mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs)))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   295
      end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   296
    val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   297
    val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   298
    val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs)
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   299
  in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   300
    val (bisim_def_thm, thy) = thy |>
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   301
        yield_singleton (Global_Theory.add_defs false)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   302
         ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), [])
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   303
  end (* local *)
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   304
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   305
  (* prove coinduction lemma *)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   306
  val coind_lemma =
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   307
    let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   308
      val assm = mk_trp (list_comb (bisim_const, Rs))
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   309
      fun one ((T, R), take_const) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   310
        let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   311
          val x = Free ("x", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   312
          val y = Free ("y", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   313
          val lhs = mk_capply (take_const $ n, x)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   314
          val rhs = mk_capply (take_const $ n, y)
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   315
        in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   316
          mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs))))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   317
        end
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   318
      val goal =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   319
          mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   320
      val rules = @{thm Rep_cfun_strict1} :: take_0_thms
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   321
      fun tacf {prems, context} =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   322
        let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   323
          val prem' = rewrite_rule [bisim_def_thm] (hd prems)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   324
          val prems' = Project_Rule.projections context prem'
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   325
          val dests = map (fn th => th RS spec RS spec RS mp) prems'
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   326
          fun one_tac (dest, rews) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   327
              dtac dest 1 THEN safe_tac HOL_cs THEN
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   328
              ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   329
        in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   330
          rtac @{thm nat.induct} 1 THEN
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   331
          simp_tac (HOL_ss addsimps rules) 1 THEN
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   332
          safe_tac HOL_cs THEN
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   333
          EVERY (map one_tac (dests ~~ take_rews))
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   334
        end
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   335
    in
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   336
      Goal.prove_global thy [] [assm] goal tacf
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   337
    end
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   338
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   339
  (* prove individual coinduction rules *)
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   340
  fun prove_coind ((T, R), take_lemma) =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   341
    let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   342
      val x = Free ("x", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   343
      val y = Free ("y", T)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   344
      val assm1 = mk_trp (list_comb (bisim_const, Rs))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   345
      val assm2 = mk_trp (R $ x $ y)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   346
      val goal = mk_trp (mk_eq (x, y))
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   347
      fun tacf {prems, context} =
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   348
        let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   349
          val rule = hd prems RS coind_lemma
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   350
        in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   351
          rtac take_lemma 1 THEN
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   352
          asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   353
        end
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   354
    in
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   355
      Goal.prove_global thy [] [assm1, assm2] goal tacf
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   356
    end
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   357
  val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   358
  val coind_binds = map (Binding.qualified true "coinduct") dbinds
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   359
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   360
in
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   361
  thy |> snd o Global_Theory.add_thms
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40023
diff changeset
   362
    (map Thm.no_attributes (coind_binds ~~ coinds))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   363
end (* let *)
35574
ee5df989b7c4 move coinduction-related stuff into function prove_coindunction
huffman
parents: 35560
diff changeset
   364
40018
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
   365
(******************************************************************************)
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
   366
(******************************* main function ********************************)
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
   367
(******************************************************************************)
bf85fef3cce4 avoid using Global_Theory.get_thm
huffman
parents: 40017
diff changeset
   368
35657
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
   369
fun comp_theorems
40019
05cda34d36e7 put constructor argument specs in constr_info type
huffman
parents: 40018
diff changeset
   370
    (dbinds : binding list)
35659
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35658
diff changeset
   371
    (take_info : Domain_Take_Proofs.take_induct_info)
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
   372
    (constr_infos : Domain_Constructors.constr_info list)
35657
0537c34c6067 pass take_induct_info as an argument to comp_theorems
huffman
parents: 35654
diff changeset
   373
    (thy : theory) =
35574
ee5df989b7c4 move coinduction-related stuff into function prove_coindunction
huffman
parents: 35560
diff changeset
   374
let
40097
429cd74f795f remove legacy comp_dbind option from domain package
huffman
parents: 40040
diff changeset
   375
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   376
val comp_dname = space_implode "_" (map Binding.name_of dbinds)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   377
val comp_dbind = Binding.name comp_dname
35574
ee5df989b7c4 move coinduction-related stuff into function prove_coindunction
huffman
parents: 35560
diff changeset
   378
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   379
(* Test for emptiness *)
40026
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   380
(* FIXME: reimplement emptiness test
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   381
local
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   382
  open Domain_Library
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   383
  val dnames = map (fst o fst) eqs
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   384
  val conss = map snd eqs
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   385
  fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   386
        is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   387
        ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   388
          rec_of arg <> n andalso rec_to (rec_of arg::ns) 
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   389
            (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   390
        ) o snd) cons
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   391
  fun warn (n,cons) =
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   392
    if rec_to [] false (n,cons)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   393
    then (warning ("domain "^List.nth(dnames,n)^" is empty!") true)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   394
    else false
40023
a868e9d73031 move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents: 40022
diff changeset
   395
in
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   396
  val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   397
  val is_emptys = map warn n__eqs
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   398
end
40026
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   399
*)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   400
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   401
(* Test for indirect recursion *)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   402
local
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   403
  val newTs = map (#absT o #iso_info) constr_infos
40026
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   404
  fun indirect_typ (Type (_, Ts)) =
8f8f18a88685 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents: 40025
diff changeset
   405
      exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   406
    | indirect_typ _ = false
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   407
  fun indirect_arg (_, T) = indirect_typ T
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   408
  fun indirect_con (_, args) = exists indirect_arg args
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   409
  fun indirect_eq cons = exists indirect_con cons
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   410
in
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   411
  val is_indirect = exists indirect_eq (map #con_specs constr_infos)
35599
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   412
  val _ =
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   413
      if is_indirect
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   414
      then message "Indirect recursion detected, skipping proofs of (co)induction rules"
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   415
      else message ("Proving induction properties of domain "^comp_dname^" ...")
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   416
end
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   417
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   418
(* theorems about take *)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   419
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
   420
val (take_rewss, thy) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   421
    take_theorems dbinds take_info constr_infos thy
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   422
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   423
val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
40016
2eff1cbc1ccb remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents: 40014
diff changeset
   424
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   425
val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   426
35585
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   427
(* prove induction rules, unless definition is indirect recursive *)
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   428
val thy =
555f26f00e47 skip proof of induction rule for indirect-recursive domain definitions
huffman
parents: 35574
diff changeset
   429
    if is_indirect then thy else
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   430
    prove_induction comp_dbind constr_infos take_info take_rews thy
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   431
35599
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   432
val thy =
20670f5564e9 skip coinduction proofs for indirect-recursive domain definitions
huffman
parents: 35597
diff changeset
   433
    if is_indirect then thy else
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   434
    prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   435
35642
f478d5a9d238 generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents: 35630
diff changeset
   436
in
f478d5a9d238 generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents: 35630
diff changeset
   437
  (take_rews, thy)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   438
end (* let *)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   439
end (* struct *)