CookBook/Package/Ind_Code.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 13 Mar 2009 16:57:16 +0100
changeset 176 3da5f3f07d8b
parent 173 d820cb5873ea
child 177 4e2341f6599d
permissions -rw-r--r--
updated to new read_specification
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory Ind_Code
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
     2
imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
     5
section {* Code *}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
     6
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
     7
subsection {* Definitions *}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
     8
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
     9
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    10
  If we give it a term and a constant name, it will define the 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    11
  constant as the term. 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    12
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    13
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    14
ML{*fun make_defs ((binding, syn), trm) lthy =
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    15
let 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    16
  val arg = ((binding, syn), (Attrib.empty_binding, trm))
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    17
  val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    18
in 
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    19
  (thm, lthy') 
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    20
end*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    21
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    22
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    23
  Returns the definition and the local theory in which this definition has 
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    24
  been made. The @{ML internalK in Thm} is just a flag attached to the 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    25
  theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    26
  These flags just classify theorems and have no significant meaning, except 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    27
  for tools such as finding theorems in the theorem database.
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    28
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    29
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    30
local_setup {*
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    31
  fn lthy =>
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    32
  let
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    33
    val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    34
    val _ = warning (str_of_thm lthy' def)
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    35
  in
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    36
    lthy'
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    37
  end
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    38
*}
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    39
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    40
text {*
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    41
  Prints out the theorem @{prop "MyTrue \<equiv> True"}.
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    42
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    43
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    44
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    45
  Constructs the term for the definition: the main arguments are a predicate
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    46
  and the types of the arguments, it also expects orules which are the 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    47
  intro rules in the object logic; preds which are all predicates. returns the
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    48
  term.
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    49
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    50
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    51
ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    52
let 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    53
  fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    54
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    55
  val fresh_args = 
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    56
        arg_tys 
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    57
        |> map (pair "z")
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    58
        |> Variable.variant_frees lthy orules 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    59
        |> map Free
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    60
in
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    61
  list_comb (pred, fresh_args)
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    62
  |> fold_rev (curry HOLogic.mk_imp) orules
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    63
  |> fold_rev mk_all preds
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    64
  |> fold_rev lambda fresh_args 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    65
end*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    66
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    67
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    68
  The lines 5-9 produce fresh arguments with which the predicate can be applied.
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    69
  For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    70
  generates variants for all these strings (names) so that they are unique w.r.t.~to 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    71
  the intro rules; in Line 9 it generates the corresponding variable terms for these 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    72
  unique names.
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    73
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    74
  The unique free variables are applied to the predicate (Line 11); then
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    75
  the intro rules are attached as preconditions (Line 12); in Line 13 we
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    76
  quantify over all predicates; and in line 14 we just abstract over all
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    77
  the (fresh) arguments of the predicate.
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    78
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    79
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    80
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    81
local_setup {*
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    82
fn lthy =>
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    83
let
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    84
  val orules = [@{prop "even 0"},
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    85
                @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    86
                @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
    87
  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    88
  val pred = @{term "even::nat\<Rightarrow>bool"}
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    89
  val arg_tys = [@{typ "nat"}]
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    90
  val def = defs_aux lthy orules preds (pred, arg_tys)
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
    91
in
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    92
  warning (Syntax.string_of_term lthy def); 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
    93
  lthy
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
    94
end*}
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
    95
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
text {*
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    97
  The arguments of the main function for the definitions are 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    98
  the intro rules; the predicates and their names, their syntax 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
    99
  annotations and the argument types of each predicate. It  
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   100
  returns a theorem list (the definitions) and a local
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   101
  theory where the definitions are made
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   102
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   103
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   104
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   105
let
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   106
  val thy = ProofContext.theory_of lthy
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   107
  val orules = map (ObjectLogic.atomize_term thy) rules
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   108
  val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   109
in
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   110
  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   111
end*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   112
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   113
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   114
  In line 4 we generate the intro rules in the object logic; for this we have to 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   115
  obtain the theory behind the local theory (Line 3); with this we can
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   116
  call @{ML defs_aux} to generate the terms for the left-hand sides.
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   117
  The actual definitions are made in Line 7.  
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   118
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   119
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   120
subsection {* Induction Principles *}
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   121
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   122
text {* Recall the proof for the induction principle for @{term "even"}: *}
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   123
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   124
lemma 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   125
  assumes prems: "even n"
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   126
  shows "P 0 \<Longrightarrow> 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   127
             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   128
apply(atomize (full))
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   129
apply(cut_tac prems)
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   130
apply(unfold even_def)
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   131
apply(drule spec[where x=P])
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   132
apply(drule spec[where x=Q])
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   133
apply(assumption)
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   134
done
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   135
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   136
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   137
text {* We need to be able to instantiate universal quantifiers. *}
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   138
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   139
ML{*fun inst_spec ct = 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   140
 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   141
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   142
text {*
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   143
  Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   144
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   145
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   146
text {*
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   147
  Instantiates universal qantifications in the premises
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   148
*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   149
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   150
lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True"
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   151
apply (tactic {* 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   152
  let 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   153
    val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   154
  in 
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   155
    EVERY1 (map (dtac o inst_spec) ctrms)
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   156
  end *})
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   157
txt {* \begin{minipage}{\textwidth}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   158
       @{subgoals} 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   159
       \end{minipage}*}
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   160
(*<*)oops(*>*)
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   161
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   162
text {*
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   163
  Now the tactic for proving the induction rules: 
163
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   164
*}
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   165
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   166
ML{*fun induction_tac defs prems insts =
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   167
  EVERY1 [ObjectLogic.full_atomize_tac,
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   168
          cut_facts_tac prems,
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   169
          K (rewrite_goals_tac defs),
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   170
          EVERY' (map (dtac o inst_spec) insts),
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   171
          assume_tac]*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   172
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   173
lemma 
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   174
  assumes prems: "even n"
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   175
  shows "P 0 \<Longrightarrow> 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   176
           (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   177
apply(tactic {* 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   178
  let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   179
     val defs = [@{thm even_def}, @{thm odd_def}]
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   180
     val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   181
  in 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   182
    induction_tac defs @{thms prems} insts 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   183
  end *})
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   184
done
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   185
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   186
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   187
text {*
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   188
  While the generic proof is relatively simple, it is a bit harder to
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   189
  set up the goals for the induction principles. 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   190
*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   191
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   192
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   193
ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   194
let
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   195
  val Ps = replicate (length preds) "P"
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   196
  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   197
  
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   198
  val thy = ProofContext.theory_of lthy2
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   199
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   200
  val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   201
  val newpreds = map Free (newprednames ~~ tyss')
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   202
  val cnewpreds = map (cterm_of thy) newpreds
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   203
  val rules' = map (subst_free (preds ~~ newpreds)) rules
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   204
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   205
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   206
  fun prove_induction ((pred, newpred), tys)  =
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   207
  let
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   208
    val zs = replicate (length tys) "z"
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   209
    val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   210
    val newargs = map Free (newargnames ~~ tys)
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   211
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   212
    val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   213
    val goal = Logic.list_implies 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   214
         (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   215
  in
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   216
    Goal.prove lthy3 [] [prem] goal
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   217
      (fn {prems, ...} => induction_tac defs prems cnewpreds)
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   218
       |> singleton (ProofContext.export lthy3 lthy1)
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   219
  end 
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   220
in
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   221
  map prove_induction (preds ~~ newpreds ~~ tyss)
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   222
end*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   223
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   224
ML {*
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   225
  let 
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   226
    val rules = [@{prop "even (0::nat)"},
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   227
                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   228
                 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   229
    val defs = [@{thm even_def}, @{thm odd_def}]
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   230
    val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   231
    val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   232
  in
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   233
    inductions rules defs preds tyss @{context}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   234
  end
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   235
*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   236
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   237
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   238
subsection {* Introduction Rules *}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   239
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   240
ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   241
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   242
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   243
ML{*fun subproof2 prem params2 prems2 =  
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   244
 SUBPROOF (fn {prems, ...} =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   245
   let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   246
     val prem' = prems MRS prem;
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   247
     val prem'' = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   248
       case prop_of prem' of
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   249
           _ $ (Const (@{const_name All}, _) $ _) =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   250
             prem' |> all_elims params2 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   251
                   |> imp_elims prems2
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   252
         | _ => prem';
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   253
   in 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   254
     rtac prem'' 1 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   255
   end)*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   256
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   257
ML{*fun subproof1 rules preds i = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   258
 SUBPROOF (fn {params, prems, context = ctxt', ...} =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   259
   let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   260
     val (prems1, prems2) = chop (length prems - length rules) prems;
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   261
     val (params1, params2) = chop (length params - length preds) params;
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   262
   in
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   263
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   264
     THEN
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   265
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   266
   end)*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   267
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   268
ML{*
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   269
fun introductions_tac defs rules preds i ctxt =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   270
  EVERY1 [ObjectLogic.rulify_tac,
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   271
          K (rewrite_goals_tac defs),
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   272
          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   273
          subproof1 rules preds i ctxt]*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   274
173
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   275
lemma evenS: 
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   276
  shows "odd m \<Longrightarrow> even (Suc m)"
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   277
apply(tactic {* 
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   278
let
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   279
  val rules = [@{prop "even (0::nat)"},
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   280
                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   281
                 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   282
  val defs = [@{thm even_def}, @{thm odd_def}]
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   283
  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   284
in
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   285
  introductions_tac defs rules preds 1 @{context}
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   286
end *})
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   287
done
d820cb5873ea used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents: 165
diff changeset
   288
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   289
ML{*fun introductions rules preds defs lthy = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   290
let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   291
  fun prove_intro (i, goal) =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   292
    Goal.prove lthy [] [] goal
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   293
      (fn {context, ...} => introductions_tac defs rules preds i context)
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   294
in
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   295
  map_index prove_intro rules
164
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   296
end*}
3f617d7a2691 more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 163
diff changeset
   297
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   298
text {* main internal function *}
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   299
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   300
ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   301
let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   302
  val syns = map snd pred_specs
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   303
  val pred_specs' = map fst pred_specs
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   304
  val prednames = map fst pred_specs'
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   305
  val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
163
2319cff107f0 removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   306
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   307
  val tyss = map (binder_types o fastype_of) preds   
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   308
  val (attrs, rules) = split_list rule_specs    
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   309
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   310
  val (defs, lthy') = definitions rules preds prednames syns tyss lthy      
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   311
  val ind_rules = inductions rules defs preds tyss lthy' 	
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   312
  val intro_rules = introductions rules preds defs lthy'
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   314
  val mut_name = space_implode "_" (map Binding.name_of prednames)
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   315
  val case_names = map (Binding.name_of o fst) attrs
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   316
in
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   317
    lthy' 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   318
    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   319
        ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   320
    |-> (fn intross => LocalTheory.note Thm.theoremK
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   321
         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   322
    |>> snd 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   323
    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   324
         ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   325
          [Attrib.internal (K (RuleCases.case_names case_names)),
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   326
           Attrib.internal (K (RuleCases.consumes 1)),
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   327
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   328
          (pred_specs ~~ ind_rules)) #>> maps snd) 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   329
    |> snd
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   330
end*}
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   332
ML{*fun read_specification' vars specs lthy =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   333
let 
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 173
diff changeset
   334
  val specs' = map (fn (a, s) => (a, [s])) specs
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   335
  val ((varst, specst), _) = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   336
                   Specification.read_specification vars specs' lthy
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   337
  val specst' = map (apsnd the_single) specst
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   338
in   
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   339
  (varst, specst')
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   340
end*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   341
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   342
ML{*fun add_inductive pred_specs rule_specs lthy =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   343
let
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   344
  val (pred_specs', rule_specs') = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   345
    read_specification' pred_specs rule_specs lthy
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   346
in
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   347
  add_inductive_i pred_specs' rule_specs' lthy
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   348
end*} 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   349
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   350
ML{*val spec_parser = 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   351
   OuterParse.opt_target --
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   352
   OuterParse.fixes -- 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   353
   Scan.optional 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   354
     (OuterParse.$$$ "where" |--
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   355
        OuterParse.!!! 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   356
          (OuterParse.enum1 "|" 
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   357
             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   358
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   359
ML{*val specification =
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   360
  spec_parser >>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   361
    (fn ((loc, pred_specs), rule_specs) =>
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   362
      Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   363
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   364
ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   365
          OuterKeyword.thy_decl specification*}
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   367
text {*
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   368
  Things to include at the end:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   369
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   370
  \begin{itemize}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   371
  \item say something about add-inductive-i to return
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   372
  the rules
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   373
  \item say that the induction principle is weaker (weaker than
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   374
  what the standard inductive package generates)
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   375
  \end{itemize}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   376
  
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   377
*}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   378
165
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   379
simple_inductive
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   380
  Even and Odd
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   381
where
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   382
  Even0: "Even 0"
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   383
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
890fbfef6d6b partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 164
diff changeset
   384
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   385
91
667a0943c40b added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
end