src/CCL/Hered.thy
changeset 47966 b8a94ed1646e
parent 42156 df219e736a5d
child 58889 5b7a9633cfa8
equal deleted inserted replaced
47964:b74655182ed6 47966:b8a94ed1646e
   116 
   116 
   117 lemma UnitF: "Unit <= HTT"
   117 lemma UnitF: "Unit <= HTT"
   118   by (simp add: subsetXH UnitXH HTT_rews)
   118   by (simp add: subsetXH UnitXH HTT_rews)
   119 
   119 
   120 lemma BoolF: "Bool <= HTT"
   120 lemma BoolF: "Bool <= HTT"
   121   by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)
   121   by (fastforce simp: subsetXH BoolXH iff: HTT_rews)
   122 
   122 
   123 lemma PlusF: "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT"
   123 lemma PlusF: "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT"
   124   by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)
   124   by (fastforce simp: subsetXH PlusXH iff: HTT_rews)
   125 
   125 
   126 lemma SigmaF: "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
   126 lemma SigmaF: "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
   127   by (fastsimp simp: subsetXH SgXH HTT_rews)
   127   by (fastforce simp: subsetXH SgXH HTT_rews)
   128 
   128 
   129 
   129 
   130 (*** Formation Rules for Recursive types - using coinduction these only need ***)
   130 (*** Formation Rules for Recursive types - using coinduction these only need ***)
   131 (***                                          exhaution rule for type-former ***)
   131 (***                                          exhaution rule for type-former ***)
   132 
   132 
   133 (*Proof by induction - needs induction rule for type*)
   133 (*Proof by induction - needs induction rule for type*)
   134 lemma "Nat <= HTT"
   134 lemma "Nat <= HTT"
   135   apply (simp add: subsetXH)
   135   apply (simp add: subsetXH)
   136   apply clarify
   136   apply clarify
   137   apply (erule Nat_ind)
   137   apply (erule Nat_ind)
   138    apply (fastsimp iff: HTT_rews)+
   138    apply (fastforce iff: HTT_rews)+
   139   done
   139   done
   140 
   140 
   141 lemma NatF: "Nat <= HTT"
   141 lemma NatF: "Nat <= HTT"
   142   apply clarify
   142   apply clarify
   143   apply (erule HTT_coinduct3)
   143   apply (erule HTT_coinduct3)