src/HOL/Induct/Term.thy
author wenzelm
Wed, 14 Mar 2012 00:34:56 +0100
changeset 46914 c2ca2c3d23a6
parent 37597 a02ea93e88c6
child 58249 180f1b3508ed
permissions -rw-r--r--
misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     1
(*  Title:      HOL/Induct/Term.thy
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
     2
    Author:     Stefan Berghofer,  TU Muenchen
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     5
header {* Terms over a given alphabet *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
     6
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 37597
diff changeset
     7
theory Term
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 37597
diff changeset
     8
imports Main
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 37597
diff changeset
     9
begin
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    11
datatype ('a, 'b) "term" =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    12
    Var 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    13
  | App 'b "('a, 'b) term list"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    15
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    16
text {* \medskip Substitution function on terms *}
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    18
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 37597
diff changeset
    19
  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 37597
diff changeset
    20
where
5738
0d8698c15439 Terms are now defined using the new datatype package.
berghofe
parents: 5717
diff changeset
    21
  "subst_term f (Var a) = f a"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    22
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    23
| "subst_term_list f [] = []"
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    24
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    26
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    27
text {* \medskip A simple theorem about composition of substitutions *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    28
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    29
lemma subst_comp:
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    30
  "subst_term (subst_term f1 \<circ> f2) t =
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    31
    subst_term f1 (subst_term f2 t)"
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    32
and "subst_term_list (subst_term f1 \<circ> f2) ts =
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    33
    subst_term_list f1 (subst_term_list f2 ts)"
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    34
  by (induct t and ts) simp_all
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    35
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    36
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    37
text {* \medskip Alternative induction rule *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    38
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    39
lemma
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12171
diff changeset
    40
  assumes var: "!!v. P (Var v)"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    41
    and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12171
diff changeset
    42
  shows term_induct2: "P t"
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 36862
diff changeset
    43
    and "\<forall>t \<in> set ts. P t"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    44
  apply (induct t and ts)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    45
     apply (rule var)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    46
    apply (rule app)
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    47
    apply assumption
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    48
   apply simp_all
dc87f33db447 tuned inductions;
wenzelm
parents: 11809
diff changeset
    49
  done
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5738
diff changeset
    50
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
end