author  paulson 
Mon, 06 Aug 2001 12:42:43 +0200  
changeset 11461  ffeac9aa1967 
parent 9039  20ff649a0fd1 
permissions  rwrr 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

1 
(* Title: Provers/split_paired_all.ML 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

4 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

5 
Derived rule for turning metalevel surjective pairing into split rule: 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

6 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

7 
p == (fst p, snd p) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

8 
 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

9 
!!a b. PROP (a, b) == !! x. PROP P x 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

10 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

11 
*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

12 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

13 
signature SPLIT_PAIRED_ALL = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

14 
sig 
9039  15 
val rule_params: string > string > thm > thm 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

16 
val rule: thm > thm 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

17 
end; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

18 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

19 
structure SplitPairedAll: SPLIT_PAIRED_ALL = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

20 
struct 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

21 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

22 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

23 
fun all x T t = Term.all T $ Abs (x, T, t); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

24 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

25 
infixr ==>; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

26 
val op ==> = Logic.mk_implies; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

27 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

28 

9039  29 
fun rule_params a b raw_surj_pair = 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

30 
let 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

31 
val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

32 

5704  33 
val surj_pair = Drule.unvarify (standard raw_surj_pair); 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

34 
val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

35 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

36 
val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair)); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

37 
val pT as Type (_, [aT, bT]) = fastype_of p; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

38 
val P = Free (variant used "P", pT > propT); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

39 

5704  40 
(*"!!a b. PROP (a, b)"*) 
9039  41 
val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))); 
5704  42 
(*"!!x. PROP P x"*) 
43 
val all_x = all "x" pT (P $ Bound 0); 

5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

44 

5704  45 
(*lemma "P p == P (fst p, snd p)"*) 
46 
val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair; 

47 

7879  48 
(*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*) 
5704  49 
val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

50 
(fn prems => [resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

51 

7879  52 
(*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*) 
5704  53 
val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

54 
(fn prems => [rtac lem2 1, resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

55 

7879  56 
(*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*) 
5704  57 
val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

58 
(fn prems => [resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

59 
in standard (Thm.equal_intr lem4 lem3) end; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

60 

9039  61 
val rule = rule_params "a" "b"; 
62 

5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

63 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

64 
end; 