author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16062  f8110bd9957f 
child 16842  5979c46853d1 
permissions  rwrr 
16062
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

1 
(* ID: $Id$ 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

2 
Author: Stefan Berghofer, TU Muenchen 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

3 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

4 
Admissibility tactic. 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

5 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

6 
Checks whether adm_subst theorem is applicable to the current proof 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

7 
state: 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

8 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

9 
[ cont t; adm P ] ==> adm (%x. P (t x)) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

10 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

11 
"t" is instantiated with a term of chainfinite type, so that 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

12 
adm_chfin can be applied: 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

13 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

14 
adm (P::'a::{chfin,pcpo} => bool) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

15 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

16 
*) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

17 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

18 
signature ADM = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

19 
sig 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

20 
val adm_tac: (int > tactic) > int > tactic 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

21 
end; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

22 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

23 
structure Adm: ADM = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

24 
struct 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

25 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

26 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

27 
(*** find_subterms t 0 [] 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

28 
returns lists of terms with the following properties: 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

29 
1. all terms in the list are disjoint subterms of t 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

30 
2. all terms contain the variable which is bound at level 0 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

31 
3. all occurences of the variable which is bound at level 0 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

32 
are "covered" by a term in the list 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

33 
a list of integers is associated with every term which describes 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

34 
the "path" leading to the subterm (required for instantiation of 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

35 
the adm_subst theorem (see functions mk_term, inst_adm_subst_thm)) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

36 
***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

37 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

38 
fun find_subterms (Bound i) lev path = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

39 
if i = lev then [[(Bound 0, path)]] 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

40 
else [] 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

41 
 find_subterms (t as (Abs (_, _, t2))) lev path = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

42 
if List.filter (fn x => x<=lev) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

43 
(add_loose_bnos (t, 0, [])) = [lev] then 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

44 
[(incr_bv (~lev, 0, t), path)]:: 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

45 
(find_subterms t2 (lev+1) (0::path)) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

46 
else find_subterms t2 (lev+1) (0::path) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

47 
 find_subterms (t as (t1 $ t2)) lev path = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

48 
let val ts1 = find_subterms t1 lev (0::path); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

49 
val ts2 = find_subterms t2 lev (1::path); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

50 
fun combine [] y = [] 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

51 
 combine (x::xs) ys = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

52 
(map (fn z => x @ z) ys) @ (combine xs ys) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

53 
in 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

54 
(if List.filter (fn x => x<=lev) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

55 
(add_loose_bnos (t, 0, [])) = [lev] then 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

56 
[[(incr_bv (~lev, 0, t), path)]] 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

57 
else []) @ 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

58 
(if ts1 = [] then ts2 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

59 
else if ts2 = [] then ts1 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

60 
else combine ts1 ts2) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

61 
end 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

62 
 find_subterms _ _ _ = []; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

63 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

64 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

65 
(*** make term for instantiation of predicate "P" in adm_subst theorem ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

66 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

67 
fun make_term t path paths lev = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

68 
if path mem paths then Bound lev 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

69 
else case t of 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

70 
(Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1)) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

71 
 (t1 $ t2) => (make_term t1 (0::path) paths lev) $ 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

72 
(make_term t2 (1::path) paths lev) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

73 
 t1 => t1; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

74 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

75 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

76 
(*** check whether all terms in list are equal ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

77 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

78 
fun eq_terms [] = true 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

79 
 eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

80 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

81 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

82 
(*figure out internal names*) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

83 
val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"]; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

84 
val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

85 
val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

86 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

87 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

88 
(*** check whether type of terms in list is chain finite ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

89 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

90 
fun is_chfin sign T params ((t, _)::_) = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

91 
let val parTs = map snd (rev params) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

92 
in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

93 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

94 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

95 
(*** try to prove that terms in list are continuous 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

96 
if successful, add continuity theorem to list l ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

97 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

98 
fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

99 
let val parTs = map snd (rev params); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

100 
val contT = (T > (fastype_of1 (T::parTs, t))) > HOLogic.boolT; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

101 
fun mk_all [] t = t 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

102 
 mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

103 
val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

104 
val t' = mk_all params (Logic.list_implies (prems, t)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

105 
val thm = Tactic.prove sign [] [] t' (K (tac 1)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

106 
in (ts, thm)::l end 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

107 
handle ERROR_MESSAGE _ => l; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

108 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

109 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

110 
(*** instantiation of adm_subst theorem (a bit tricky) ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

111 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

112 
fun inst_adm_subst_thm state i params s T subt t paths = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

113 
let val {sign, maxidx, ...} = rep_thm state; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

114 
val j = maxidx+1; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

115 
val tsig = Sign.tsig_of sign; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

116 
val parTs = map snd (rev params); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

117 
val rule = lift_rule (state, i) adm_subst; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

118 
val types = valOf o (fst (types_sorts rule)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

119 
val tT = types ("t", j); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

120 
val PT = types ("P", j); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

121 
fun mk_abs [] t = t 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

122 
 mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

123 
val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

124 
val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))]) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

125 
(make_term t [] paths 0)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

126 
val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt))); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

127 
val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

128 
val ctye = map (fn (ixn, (S, T)) => 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

129 
(ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye'); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

130 
val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

131 
val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT)); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

132 
val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

133 
in rule' end; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

134 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

135 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

136 
(*** extract subgoal i from proof state ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

137 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

138 
fun nth_subgoal i thm = List.nth (prems_of thm, i1); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

139 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

140 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

141 
(*** the admissibility tactic ***) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

142 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

143 
fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

144 
if name = adm_name then SOME abs else NONE 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

145 
 try_dest_adm _ = NONE; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

146 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

147 
fun adm_tac tac i state = 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

148 
state > 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

149 
let val goali = nth_subgoal i state in 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

150 
(case try_dest_adm (Logic.strip_assums_concl goali) of 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

151 
NONE => no_tac 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

152 
 SOME (s, T, t) => 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

153 
let 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

154 
val sign = sign_of_thm state; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

155 
val prems = Logic.strip_assums_hyp goali; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

156 
val params = Logic.strip_params goali; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

157 
val ts = find_subterms t 0 []; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

158 
val ts' = List.filter eq_terms ts; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

159 
val ts'' = List.filter (is_chfin sign T params) ts'; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

160 
val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts''); 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

161 
in 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

162 
(case thms of 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

163 
((ts as ((t', _)::_), cont_thm)::_) => 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

164 
let 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

165 
val paths = map snd ts; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

166 
val rule = inst_adm_subst_thm state i params s T t' t paths; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

167 
in 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

168 
compose_tac (false, rule, 2) i THEN 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

169 
rtac cont_thm i THEN 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

170 
REPEAT (assume_tac i) THEN 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

171 
rtac adm_chfin i 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

172 
end 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

173 
 [] => no_tac) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

174 
end) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

175 
end; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

176 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

177 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

178 
end; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

179 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

180 

f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
diff
changeset

181 
open Adm; 