src/CTT/ex/Equality.thy
author blanchet
Mon, 20 Dec 2010 14:17:49 +0100
changeset 41317 fc48faccd77b
parent 35762 af3ff2ba4c54
child 58889 5b7a9633cfa8
permissions -rw-r--r--
disable feature that was enabled by mistake
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     1
(*  Title:      CTT/ex/Equality.thy
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     6
header "Equality reasoning by rewriting"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
theory Equality
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     9
imports CTT
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
begin
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
apply (rule EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    14
apply (rule elim_rls, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    18
lemma when_eq: "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
apply (rule EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
apply (rule elim_rls, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
(*in the "rec" formulation of addition, 0+n=n *)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    25
lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
apply (rule EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
apply (rule elim_rls, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    28
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
(*the harder version, n+0=n: recursive, uses induction hypothesis*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
apply (rule EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
apply (rule elim_rls, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
apply (tactic "hyp_rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    36
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    37
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
(*Associativity of addition*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
lemma "[| a:N;  b:N;  c:N |]
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
      ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    41
          rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 19761
diff changeset
    42
apply (tactic {* NE_tac @{context} "a" 1 *})
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
apply (tactic "hyp_rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    44
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    45
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
(*Martin-Lof (1984) page 62: pairing is surjective*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    48
apply (rule EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    49
apply (rule elim_rls, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
lemma "[| a : A;  b : B |] ==>
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    54
     (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    58
(*a contrived, complicated simplication, requires sum-elimination also*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
      lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
apply (rule reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
apply (rule_tac [3] intrL_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    63
apply (rule_tac [4] EqE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    64
apply (rule_tac [4] SumE, tactic "assume_tac 4")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
(*order of unifiers is essential here*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    68
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
end