17456

1 
(* Title: CCL/Hered.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen

0

4 
Copyright 1993 University of Cambridge


5 
*)


6 

17456

7 
header {* Hereditary Termination  cf. Martin Lo\"f *}


8 


9 
theory Hered


10 
imports Type


11 
begin


12 


13 
text {*


14 
Note that this is based on an untyped equality and so @{text "lam


15 
x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"}


16 
is. Not so useful for functions!


17 
*}

0

18 


19 
consts


20 
(*** Predicates ***)


21 
HTTgen :: "i set => i set"


22 
HTT :: "i set"


23 

17456

24 
axioms

0

25 
(*** Definitions of Hereditary Termination ***)


26 

17456

27 
HTTgen_def:


28 
"HTTgen(R) == {t. t=true  t=false  (EX a b. t=<a,b> & a : R & b : R) 

3837

29 
(EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"

17456

30 
HTT_def: "HTT == gfp(HTTgen)"


31 

20140

32 


33 
subsection {* Hereditary Termination *}


34 


35 
lemma HTTgen_mono: "mono(%X. HTTgen(X))"


36 
apply (unfold HTTgen_def)


37 
apply (rule monoI)


38 
apply blast


39 
done


40 


41 
lemma HTTgenXH:


42 
"t : HTTgen(A) <> t=true  t=false  (EX a b. t=<a,b> & a : A & b : A) 


43 
(EX f. t=lam x. f(x) & (ALL x. f(x) : A))"


44 
apply (unfold HTTgen_def)


45 
apply blast


46 
done


47 


48 
lemma HTTXH:


49 
"t : HTT <> t=true  t=false  (EX a b. t=<a,b> & a : HTT & b : HTT) 


50 
(EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"


51 
apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def])


52 
apply blast


53 
done


54 


55 


56 
subsection {* Introduction Rules for HTT *}


57 


58 
lemma HTT_bot: "~ bot : HTT"


59 
by (blast dest: HTTXH [THEN iffD1])


60 


61 
lemma HTT_true: "true : HTT"


62 
by (blast intro: HTTXH [THEN iffD2])


63 


64 
lemma HTT_false: "false : HTT"


65 
by (blast intro: HTTXH [THEN iffD2])


66 


67 
lemma HTT_pair: "<a,b> : HTT <> a : HTT & b : HTT"


68 
apply (rule HTTXH [THEN iff_trans])


69 
apply blast


70 
done


71 


72 
lemma HTT_lam: "lam x. f(x) : HTT <> (ALL x. f(x) : HTT)"


73 
apply (rule HTTXH [THEN iff_trans])


74 
apply auto


75 
done


76 


77 
lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam


78 


79 
lemma HTT_rews2:


80 
"one : HTT"


81 
"inl(a) : HTT <> a : HTT"


82 
"inr(b) : HTT <> b : HTT"


83 
"zero : HTT"


84 
"succ(n) : HTT <> n : HTT"


85 
"[] : HTT"


86 
"x$xs : HTT <> x : HTT & xs : HTT"


87 
by (simp_all add: data_defs HTT_rews1)


88 


89 
lemmas HTT_rews = HTT_rews1 HTT_rews2


90 


91 


92 
subsection {* Coinduction for HTT *}


93 


94 
lemma HTT_coinduct: "[ t : R; R <= HTTgen(R) ] ==> t : HTT"


95 
apply (erule HTT_def [THEN def_coinduct])


96 
apply assumption


97 
done


98 


99 
ML {*


100 
local val HTT_coinduct = thm "HTT_coinduct"


101 
in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end


102 
*}


103 


104 
lemma HTT_coinduct3:


105 
"[ t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) ] ==> t : HTT"


106 
apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]])


107 
apply assumption


108 
done


109 


110 
ML {*


111 
local


112 
val HTT_coinduct3 = thm "HTT_coinduct3"


113 
val HTTgen_def = thm "HTTgen_def"


114 
in


115 


116 
val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3


117 


118 
fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i


119 


120 
val HTTgenIs =


121 
map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono"))


122 
["true : HTTgen(R)",


123 
"false : HTTgen(R)",


124 
"[ a : R; b : R ] ==> <a,b> : HTTgen(R)",


125 
"[ !!x. b(x) : R ] ==> lam x. b(x) : HTTgen(R)",


126 
"one : HTTgen(R)",


127 
"a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",


128 
"b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",


129 
"zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",


130 
"n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",


131 
"[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",


132 
"[ h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) ] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]

0

133 


134 
end

20140

135 
*}


136 


137 
ML {* bind_thms ("HTTgenIs", HTTgenIs) *}


138 


139 


140 
subsection {* Formation Rules for Types *}


141 


142 
lemma UnitF: "Unit <= HTT"


143 
by (simp add: subsetXH UnitXH HTT_rews)


144 


145 
lemma BoolF: "Bool <= HTT"


146 
by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)


147 


148 
lemma PlusF: "[ A <= HTT; B <= HTT ] ==> A + B <= HTT"


149 
by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)


150 


151 
lemma SigmaF: "[ A <= HTT; !!x. x:A ==> B(x) <= HTT ] ==> SUM x:A. B(x) <= HTT"


152 
by (fastsimp simp: subsetXH SgXH HTT_rews)


153 


154 


155 
(*** Formation Rules for Recursive types  using coinduction these only need ***)


156 
(*** exhaution rule for typeformer ***)


157 


158 
(*Proof by induction  needs induction rule for type*)


159 
lemma "Nat <= HTT"


160 
apply (simp add: subsetXH)


161 
apply clarify


162 
apply (erule Nat_ind)


163 
apply (fastsimp iff: HTT_rews)+


164 
done


165 


166 
lemma NatF: "Nat <= HTT"


167 
apply clarify


168 
apply (erule HTT_coinduct3)


169 
apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1])


170 
done


171 


172 
lemma ListF: "A <= HTT ==> List(A) <= HTT"


173 
apply clarify


174 
apply (erule HTT_coinduct3)


175 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]


176 
subsetD [THEN HTTgen_mono [THEN ci3_AI]]


177 
dest: ListXH [THEN iffD1])


178 
done


179 


180 
lemma ListsF: "A <= HTT ==> Lists(A) <= HTT"


181 
apply clarify


182 
apply (erule HTT_coinduct3)


183 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]


184 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1])


185 
done


186 


187 
lemma IListsF: "A <= HTT ==> ILists(A) <= HTT"


188 
apply clarify


189 
apply (erule HTT_coinduct3)


190 
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]


191 
subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1])


192 
done


193 


194 
end
